-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma range_emb_extendMiddle_ne_singleton_zero (c : OrderedFinpartition n) (i j : Fin c.length) :
    range ((c.extendMiddle i).emb j) ≠ {0}

Proof state:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ False

Tactic:
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, cast_trans, cast_eq_self, cases_succ]

Result:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ ∈ {0}
⊢ False

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ ∃ y, (c.extendMiddle j).emb j y = (c.emb j 0).succ

Tactic:
refine ⟨Fin.cast A.symm (succ 0), ?_⟩

Result:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ (c.extendMiddle j).emb j (Fin.cast ⋯ (succ 0)) = (c.emb j 0).succ

Proof state:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ {0}
⊢ False

Tactic:
simp only [extendMiddle, hij, ↓reduceDIte, comp_apply, cast_zero, mem_singleton_iff] at this

Result:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.emb j 0).succ = 0
⊢ False

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ ∃ y, (c.extendMiddle j).emb j y = (c.emb j 0).succ

Tactic:
have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]

Result:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ ∃ y, (c.extendMiddle j).emb j y = (c.emb j 0).succ

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ (c.extendMiddle j).emb j (Fin.cast ⋯ (succ 0)) = (c.emb j 0).succ

Tactic:
simp only [extendMiddle, ↓reduceDIte, comp_apply, cast_trans, cast_eq_self, cases_succ]

Result:
no goals

Proof state:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.emb j 0).succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Result:
no goals

Proof state:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)
⊢ False

Tactic:
rw [h] at this

Result:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ {0}
⊢ False

Proof state:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
⊢ range ((c.extendMiddle i).emb j) ≠ {0}

Tactic:
intro h

Result:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
⊢ False

Proof state:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.emb j 0).succ ∈ range ((c.extendMiddle j).emb j)

Tactic:
simp only [Nat.succ_eq_add_one, mem_range]

Result:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ ∃ y, (c.extendMiddle j).emb j y = (c.emb j 0).succ

Proof state:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ ∈ {0}
⊢ False

Tactic:
simp only [mem_singleton_iff] at this

Result:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ = 0
⊢ False

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.emb j 0).succ ∈ {0}

Tactic:
rw [← h]

Result:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.emb j 0).succ ∈ range ((c.extendMiddle j).emb j)

Proof state:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
⊢ False

Tactic:
have : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j) :=
  mem_range_self 0

Result:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)
⊢ False

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.extendMiddle j).partSize j = c.partSize j + 1

Tactic:
simp [extendMiddle]

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
⊢ False

Tactic:
rcases eq_or_ne j i with rfl | hij

Result:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ False

case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
⊢ False