English
For all i,j, range((c.extendMiddle i).emb j) ≠ {0}.
Русский
Для всех i,j диапазон (c.extendMiddle i).emb j не равен {0}.
LaTeX
$$$\\forall i:\\mathrm{Fin}(c.length),\\forall j:\\mathrm{Fin}(c.partSize i),\\; \\operatorname{range}( (\\mathrm{extendMiddle}\, i).\\mathrm{emb}\\, j) \\neq \\{0\\}$$$
Lean4
/-- Extend an ordered partition of `n` entries, by adding to the `i`-th part a new point to the
left. -/
@[simps -fullyApplied length partSize]
def extendMiddle (c : OrderedFinpartition n) (k : Fin c.length) : OrderedFinpartition (n + 1)
where
length := c.length
partSize := update c.partSize k (c.partSize k + 1)
partSize_pos
m := by
rcases eq_or_ne m k with rfl | hm
· simp
· simpa [hm] using c.partSize_pos m
emb := by
intro m
by_cases h : m = k
· have : update c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := by rw [h]; simp
exact Fin.cases 0 (succ ∘ c.emb k) ∘ Fin.cast this
· have : update c.partSize k (c.partSize k + 1) m = c.partSize m := by simp [h]
exact succ ∘ c.emb m ∘ Fin.cast this
emb_strictMono := by
intro m
rcases eq_or_ne m k with rfl | hm
· suffices
∀ (a' b' : Fin (c.partSize m + 1)),
a' < b' →
(cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) a' <
(cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) b'
by
simp only [↓reduceDIte]
intro a b hab
exact this _ _ hab
intro a' b' h'
induction b' using Fin.induction with
| zero => simp at h'
| succ b =>
induction a' using Fin.induction with
| zero => simp
| succ a' =>
simp only [cases_succ, comp_apply, succ_lt_succ_iff]
exact c.emb_strictMono m (by simpa using h')
· simp only [hm, ↓reduceDIte]
exact strictMono_succ.comp ((c.emb_strictMono m).comp (by exact fun ⦃a b⦄ h ↦ h))
parts_strictMono := by
convert strictMono_succ.comp c.parts_strictMono with m
rcases eq_or_ne m k with rfl | hm
· simp only [↓reduceDIte, update_self, add_tsub_cancel_right, comp_apply, cast_mk]
let a : Fin (c.partSize m + 1) := ⟨c.partSize m, lt_add_one (c.partSize m)⟩
let b : Fin (c.partSize m) := ⟨c.partSize m - 1, Nat.sub_one_lt_of_lt (c.partSize_pos m)⟩
change (cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) a = succ (c.emb m b)
have : a = succ b := by simpa [a, b, succ] using (Nat.sub_eq_iff_eq_add (c.partSize_pos m)).mp rfl
simp [this]
· simp [hm]
disjoint i hi j hj
hij := by
wlog h : i ≠ k generalizing i j
· apply Disjoint.symm (this j (mem_univ j) i (mem_univ i) hij.symm ?_)
simp only [ne_eq, Decidable.not_not] at h
simpa [h] using hij.symm
rcases eq_or_ne j k with rfl | hj
· simp only [onFun, ↓reduceDIte]
suffices
∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
succ (c.emb i a') ≠ cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
by
apply Set.disjoint_iff_forall_ne.2
simp only [hij, ↓reduceDIte, mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff]
intro a b
apply this
intro a' b'
induction b' using Fin.induction with
| zero => simp
| succ b' =>
simp only [cases_succ, comp_apply, ne_eq, succ_inj]
apply c.emb_ne_emb_of_ne hij
· simp only [onFun, h, ↓reduceDIte, hj]
apply Set.disjoint_iff_forall_ne.2
simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, succ_inj]
intro a b
apply c.emb_ne_emb_of_ne hij
cover := by
refine Fin.cases ?_ (fun i ↦ ?_)
· simp only [mem_range]
exact ⟨k, ⟨0, by simp⟩, by simp⟩
· simp only [mem_range]
rcases eq_or_ne (c.index i) k with rfl | hi
· have A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) = c.partSize (c.index i) + 1 :=
by simp
exact ⟨c.index i, (succ (c.invEmbedding i)).cast A.symm, by simp⟩
· have A : update c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i) := by simp [hi]
exact ⟨c.index i, (c.invEmbedding i).cast A.symm, by simp [hi]⟩
