English
If an ordered finpartition c of n+1 has its leftmost atom equal to {0}, then eraseLeft c hc is an ordered finpartition of n.
Русский
Если упорядоченная финразби́вка c на n+1 имеет левый атом равный {0}, тогда eraseLeft c hc является упорядоченной финразби́вкой на n.
LaTeX
$$If $c$ is an OrderedFinpartition of $n+1$ and $hc: \mathrm{range}(c.emb\,0) = \{0\}$, then $\mathrm{eraseLeft}(c hc)$ is an OrderedFinpartition of $n$.$$
Lean4
/-- Given an ordered finpartition of `n+1`, with a leftmost atom equal to `{0}`, remove this
atom to form an ordered finpartition of `n`. -/
def eraseLeft (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) = {0}) : OrderedFinpartition n
where
length := c.length - 1
partSize := by
have : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
exact fun i ↦ c.partSize (Fin.cast this (succ i))
partSize_pos i := c.partSize_pos _
emb i
j := by
have : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
refine Fin.pred (c.emb (Fin.cast this (succ i)) j) ?_
have := c.disjoint (mem_univ (Fin.cast this (succ i))) (mem_univ 0) (ne_of_beq_false rfl)
exact Set.disjoint_iff_forall_ne.1 this (by simp) (by simp only [mem_singleton_iff, hc])
emb_strictMono i a b
hab := by
simp only [pred_lt_pred_iff, Nat.succ_eq_add_one]
apply c.emb_strictMono _ hab
parts_strictMono := by
intro i j hij
simp only [pred_lt_pred_iff, Nat.succ_eq_add_one]
apply c.parts_strictMono (cast_strictMono _ (strictMono_succ hij))
disjoint i _ j _
hij := by
apply Set.disjoint_iff_forall_ne.2
simp only [mem_range, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, pred_inj]
intro a b
exact c.emb_ne_emb_of_ne ((cast_injective _).ne (by simpa using hij))
cover
x := by
simp only [mem_range]
obtain ⟨i, j, hij⟩ : ∃ (i : Fin c.length), ∃ (j : Fin (c.partSize i)), c.emb i j = succ x :=
⟨c.index (succ x), c.invEmbedding (succ x), by simp⟩
have A : c.length = c.length - 1 + 1 := (Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))).symm
have i_ne : i ≠ 0 := by
intro h
have : succ x ∈ range (c.emb i) := by rw [← hij]; apply mem_range_self
rw [h, hc, mem_singleton_iff] at this
exact Fin.succ_ne_zero _ this
refine ⟨pred (Fin.cast A i) (by simpa using i_ne), Fin.cast (by simp) j, ?_⟩
have : x = pred (succ x) (succ_ne_zero x) := rfl
rw [this]
congr
rw [← hij]
congr 1
· simp
· simp [Fin.heq_ext_iff]
