Theorem: PreHFSet.exists_mem_rank_eq_rank_succ (Hfzfa.lean)

State before:
atoms : Type u_1
y✝ z : PreHFSet atoms
hz : z ∈ y✝
x✝¹ : PreHFSet atoms
n : ℕ
y : Fin (n + 1) → PreHFSet atoms
x✝ : x✝¹ ∈ lst y
hy : ∃ z, z ∈ lst y
⊢ ∃ z, z ∈ lst y ∧ rank (lst y) = rank z + 1
Tactic:
obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_sup' (Finset.univ_nonempty (α := Fin (n + 1))) (fun i => rank (y i))
State after:
case intro.intro
atoms : Type u_1
y✝ z : PreHFSet atoms
hz : z ∈ y✝
x✝¹ : PreHFSet atoms
n : ℕ
y : Fin (n + 1) → PreHFSet atoms
x✝ : x✝¹ ∈ lst y
hy : ∃ z, z ∈ lst y
i : Fin (n + 1)
left✝ : i ∈ Finset.univ
hi : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => rank (y i)) = rank (y i)
⊢ ∃ z, z ∈ lst y ∧ rank (lst y) = rank z + 1

State before:
case intro.intro
atoms : Type u_1
y✝ z : PreHFSet atoms
hz : z ∈ y✝
x✝¹ : PreHFSet atoms
n : ℕ
y : Fin (n + 1) → PreHFSet atoms
x✝ : x✝¹ ∈ lst y
hy : ∃ z, z ∈ lst y
i : Fin (n + 1)
left✝ : i ∈ Finset.univ
hi : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => rank (y i)) = rank (y i)
⊢ ∃ z, z ∈ lst y ∧ rank (lst y) = rank z + 1
Tactic:
refine ⟨y i, ⟨i, Equiv.rfl⟩, ?_⟩
State after:
case intro.intro
atoms : Type u_1
y✝ z : PreHFSet atoms
hz : z ∈ y✝
x✝¹ : PreHFSet atoms
n : ℕ
y : Fin (n + 1) → PreHFSet atoms
x✝ : x✝¹ ∈ lst y
hy : ∃ z, z ∈ lst y
i : Fin (n + 1)
left✝ : i ∈ Finset.univ
hi : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => rank (y i)) = rank (y i)
⊢ rank (lst y) = rank (y i) + 1

State before:
case intro.intro
atoms : Type u_1
y✝ z : PreHFSet atoms
hz : z ∈ y✝
x✝¹ : PreHFSet atoms
n : ℕ
y : Fin (n + 1) → PreHFSet atoms
x✝ : x✝¹ ∈ lst y
hy : ∃ z, z ∈ lst y
i : Fin (n + 1)
left✝ : i ∈ Finset.univ
hi : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => rank (y i)) = rank (y i)
⊢ rank (lst y) = rank (y i) + 1
Tactic:
rw [← hi, rank, Finset.sup'_eq_sup]
State after:
no goals