Theorem: PreHFSet.rank_lt_of_mem (Hfzfa.lean)

State before:
atoms : Type u_1
x y : PreHFSet atoms
h✝ : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h : x ∈ lst b
⊢ rank x < rank (lst b)
Tactic:
simp only [rank, Nat.lt_succ_iff]
State after:
atoms : Type u_1
x y : PreHFSet atoms
h✝ : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h : x ∈ lst b
⊢ rank x ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
atoms : Type u_1
x y : PreHFSet atoms
h✝ : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h : x ∈ lst b
⊢ rank x ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
rcases h with ⟨i, hi⟩
State after:
case intro
atoms : Type u_1
x y : PreHFSet atoms
h : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin n✝
hi : x ≈ b i
⊢ rank x ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
case intro
atoms : Type u_1
x y : PreHFSet atoms
h : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin n✝
hi : x ≈ b i
⊢ rank x ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
rw [rank_eq_of_equiv hi]
State after:
case intro
atoms : Type u_1
x y : PreHFSet atoms
h : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin n✝
hi : x ≈ b i
⊢ rank (b i) ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
case intro
atoms : Type u_1
x y : PreHFSet atoms
h : x ∈ y
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin n✝
hi : x ≈ b i
⊢ rank (b i) ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
exact Finset.le_sup (f := fun i => rank (b i)) (Finset.mem_univ i)
State after:
no goals