-- Mathlib/Combinatorics/Colex.lean
lemma IsInitSeg.exists_initSeg (h𝒜 : IsInitSeg 𝒜 r) (h𝒜₀ : 𝒜.Nonempty) :
    ∃ s : Finset α, #s = r ∧ 𝒜 = initSeg s

Proof state:
case h.refine_2.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ toColex).ofColex = #t
le : { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
p : { ofColex := t } < { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
⊢ t ∈ 𝒜

Tactic:
exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ #(𝒜.sup' h𝒜₀ toColex).ofColex = #t ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }

Tactic:
refine ⟨fun p ↦ ?_, ?_⟩

Result:
case h.refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ #(𝒜.sup' h𝒜₀ toColex).ofColex = #t ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }

case h.refine_2
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ #(𝒜.sup' h𝒜₀ toColex).ofColex = #t ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex } → t ∈ 𝒜

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ t ∈ initSeg (𝒜.sup' h𝒜₀ toColex).ofColex

Tactic:
rw [mem_initSeg]

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ #(𝒜.sup' h𝒜₀ toColex).ofColex = #t ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }

Proof state:
case h.refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ r = r ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }

Tactic:
exact ⟨rfl, le_sup' _ p⟩

Result:
no goals

Proof state:
case h.refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ #(𝒜.sup' h𝒜₀ toColex).ofColex = #t ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }

Tactic:
rw [h𝒜.1 p, h𝒜.1 hs]

Result:
case h.refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ r = r ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
a : Finset α
ha : a ∈ 𝒜
⊢ { ofColex := a } ∈ ofColex ⁻¹' ↑𝒜

Tactic:
simpa using ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex
  (fun a ha ↦ by simpa using ha)

Result:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
⊢ 𝒜 = initSeg (𝒜.sup' h𝒜₀ toColex).ofColex

Tactic:
ext t

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ t ∈ initSeg (𝒜.sup' h𝒜₀ toColex).ofColex

Proof state:
case h.refine_2.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ toColex).ofColex = #t
le : { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
⊢ t ∈ 𝒜

Tactic:
obtain p | p := le.eq_or_lt

Result:
case h.refine_2.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ toColex).ofColex = #t
le : { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
p : { ofColex := t } = { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
⊢ t ∈ 𝒜

case h.refine_2.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ toColex).ofColex = #t
le : { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
p : { ofColex := t } < { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
⊢ t ∈ 𝒜

Proof state:
case h.refine_2.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ toColex).ofColex = #t
le : { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
p : { ofColex := t } = { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
⊢ t ∈ 𝒜

Tactic:
rwa [toColex_inj.1 p]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
refine ⟨_, h𝒜.1 hs, ?_⟩

Result:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
⊢ 𝒜 = initSeg (𝒜.sup' h𝒜₀ toColex).ofColex

Proof state:
case h.refine_2
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ #(𝒜.sup' h𝒜₀ toColex).ofColex = #t ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex } → t ∈ 𝒜

Tactic:
rintro ⟨cards, le⟩

Result:
case h.refine_2.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ toColex).ofColex = #t
le : { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
⊢ t ∈ 𝒜