English
For a maximal product l, Linear_CC'(C hsC ho) applied to l.val equals tail evaluation of C' ho.
Русский
Для максимального продукта l линейный отображатель равен хвосту по C' ho.
LaTeX
$$$\\mathrm{max\\_eq\\_eval} \\ (l : \\mathrm{MaxProducts} C ho) : \\mathrm{Linear\\_CC'} C hsC ho (l. val) = l.val.tail.eval (C' C ho)$$$
Lean4
theorem max_eq_eval [Inhabited I] (l : Products I) (hl : l.val ≠ []) (hlh : l.val.head! = term I ho) :
Linear_CC' C hsC ho (l.eval C) = l.Tail.eval (C' C ho) :=
by
have hlc : ((term I ho) :: l.Tail.val).IsChain (· > ·) := by rw [← max_eq_o_cons_tail ho l hl hlh]; exact l.prop
rw [max_eq_o_cons_tail' ho l hl hlh hlc, Products.evalCons]
ext x
simp only [Linear_CC', Linear_CC'₁, LocallyConstant.comapₗ, Linear_CC'₀, Subtype.coe_eta, LinearMap.sub_apply,
LinearMap.coe_mk, AddHom.coe_mk, LocallyConstant.sub_apply, LocallyConstant.coe_comap, LocallyConstant.coe_mul,
ContinuousMap.coe_mk, Function.comp_apply, Pi.mul_apply]
rw [CC'₁, CC'₀, Products.eval_eq, Products.eval_eq, Products.eval_eq]
simp only [mul_ite, mul_one, mul_zero]
have hi' : ∀ i, i ∈ l.Tail.val → (x.val i = SwapTrue o x.val i) :=
by
intro i hi
simp only [SwapTrue, @eq_comm _ (x.val i), ite_eq_right_iff, ord_term ho]
rintro rfl
exact ((List.IsChain.rel_cons hlc hi).ne rfl).elim
have H : (∀ i, i ∈ l.Tail.val → (x.val i = true)) = (∀ i, i ∈ l.Tail.val → (SwapTrue o x.val i = true)) := by
apply forall_congr; intro i; apply forall_congr; intro hi; rw [hi' i hi]
simp only [H]
split_ifs with h₁ h₂ h₃ <;> try (dsimp [e])
· rw [if_pos (swapTrue_eq_true _ _), if_neg]
· rfl
· simp [mem_C'_eq_false C ho x x.prop]
· push_neg at h₂; obtain ⟨i, hi⟩ := h₂; exfalso; rw [hi' i hi.1] at hi; exact hi.2 (h₁ i hi.1)
· push_neg at h₁; obtain ⟨i, hi⟩ := h₁; exfalso; rw [← hi' i hi.1] at hi; exact hi.2 (h₃ i hi.1)
