English
The composition of eval with sum_equiv equals the elimination on the sum, i.e., eval after the equivalence acts like evaluating each branch separately.
Русский
Композиция eval с sum_equiv совпадает с разложением по веткам, т.е. eval после эквивалента действует отдельно на каждую ветвь.
LaTeX
$$$\\mathrm{eval}\\,C \\circ (\\mathrm{sum\\_equiv}\\ C\\ ho) = \\mathrm{Sum.elim}\\ (\\lambda l. \\mathrm{Products.eval}\\ C l.1) (\\lambda l. \\mathrm{Products.eval}\\ C l.1)$$$
Lean4
/-- The equivalence from the sum of `GoodProducts (π C (ord I · < o))` and
`(MaxProducts C ho)` to `GoodProducts C`. -/
noncomputable def sum_equiv (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type (· < · : I → I → Prop)) :
GoodProducts (π C (ord I · < o)) ⊕ (MaxProducts C ho) ≃ GoodProducts C :=
calc
_ ≃ Set.range (sum_to C ho) := Equiv.ofInjective (sum_to C ho) (injective_sum_to C ho)
_ ≃ _ := Equiv.setCongr <| by rw [sum_to_range C ho, union_succ C hsC ho]
