-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
/-- If the left-most part is not `{0}`, then the part containing `0` has at least two elements:
either because it's the left-most part, and then it's not just `0` by assumption, or because it's
not the left-most part and then, by increasingness of maximal elements in parts, it contains
a positive element. -/
lemma one_lt_partSize_index_zero (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) ≠ {0}) :
    1 < c.partSize (c.index 0)

Proof state:
case h.e'_3
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 = {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩}.card

Tactic:
apply (Finset.card_pair ?_).symm

Result:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 0 ≠ c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩

Proof state:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
convert Nat.card_mono Subtype.finite this

Result:
case h.e'_3
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 = Nat.card ↑{0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩}

Proof state:
case h.e'_3
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 = Nat.card ↑{0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩}

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_ofFinset, toFinset_singleton]

Result:
case h.e'_3
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 = {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩}.card

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ {0} ⊂ range (c.emb (c.index 0))

Tactic:
apply ssubset_of_subset_of_ne ?_ hc.symm

Result:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ {0} ⊆ range (c.emb (c.index 0))

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]

Result:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card (Fin (c.partSize (c.index 0)))

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
⊢ 1 < c.partSize (c.index 0)

Tactic:
rw [this]

Result:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card (Fin (c.partSize (c.index 0)))

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
⊢ 1 < c.partSize (c.index 0)

Tactic:
have : c.partSize (c.index 0) = Nat.card (range (c.emb (c.index 0))) := by
  rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]; simp

Result:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
⊢ 1 < c.partSize (c.index 0)

Proof state:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
have : {c.emb (c.index 0) 0,
    c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, Nat.sub_one_lt_of_lt (c.partSize_pos _)⟩}
      ⊆ range (c.emb (c.index 0)) := by simp [insert_subset]

Result:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {c.emb (c.index 0) 0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
apply one_lt_two.trans_le

Result:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
rw [← h] at hc

Result:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {c.emb (c.index 0) 0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
simp only [emb_zero] at this

Result:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ {0} ⊆ range (c.emb (c.index 0))

Tactic:
simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 0 ≠ c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩

Tactic:
exact ((Fin.zero_le _).trans_lt (c.parts_strictMono ((pos_iff_ne_zero' (c.index 0)).mpr h))).ne

Result:
no goals