English
range(extendLeft.emb 0) = {0}.
Русский
Диапазон extendLeft.emb 0 = {0}.
LaTeX
$$$\\operatorname{range}(\\mathrm{extendLeft}.\\mathrm{emb}\\,0) = \\{0\\}$$$
Lean4
theorem range_emb_extendMiddle_ne_singleton_zero (c : OrderedFinpartition n) (i j : Fin c.length) :
range ((c.extendMiddle i).emb j) ≠ {0} := by
intro h
rcases eq_or_ne j i with rfl | hij
· have : Fin.succ (c.emb j 0) ∈ ({0} : Set (Fin n.succ)) :=
by
rw [← h]
simp only [Nat.succ_eq_add_one, mem_range]
have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]
refine ⟨Fin.cast A.symm (succ 0), ?_⟩
simp only [extendMiddle, ↓reduceDIte, comp_apply, Fin.cast_cast, cast_eq_self, cases_succ]
simp only [mem_singleton_iff] at this
exact Fin.succ_ne_zero _ this
· have : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j) := mem_range_self 0
rw [h] at this
simp only [extendMiddle, hij, ↓reduceDIte, comp_apply, cast_zero, mem_singleton_iff] at this
exact Fin.succ_ne_zero _ this
