Theorem: PreHFSet.rank_eq_of_equiv (Hfzfa.lean)

State before:
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ rank (lst a) = rank (lst b)
Tactic:
apply le_antisymm
State after:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ rank (lst a) ≤ rank (lst b)

case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ rank (lst b) ≤ rank (lst a)

State before:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ rank (lst a) ≤ rank (lst b)
Tactic:
simp only [rank, Nat.succ_le_succ_iff, Finset.sup_le_iff]
State after:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (b_1 : Fin n✝¹), b_1 ∈ Finset.univ → rank (a b_1) ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (b_1 : Fin n✝¹), b_1 ∈ Finset.univ → rank (a b_1) ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
intro i _
State after:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
a✝ : i ∈ Finset.univ
⊢ rank (a i) ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
a✝ : i ∈ Finset.univ
⊢ rank (a i) ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
obtain ⟨j, hj⟩ := h₁ i
State after:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
a✝ : i ∈ Finset.univ
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ rank (a i) ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
a✝ : i ∈ Finset.univ
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ rank (a i) ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
rw [rank_eq_of_equiv hj]
State after:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
a✝ : i ∈ Finset.univ
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ rank (b j) ≤ Finset.sup Finset.univ fun i => rank (b i)

State before:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
a✝ : i ∈ Finset.univ
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ rank (b j) ≤ Finset.sup Finset.univ fun i => rank (b i)
Tactic:
exact Finset.le_sup (f := fun i => rank (b i)) (Finset.mem_univ j)
State after:
no goals

State before:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ rank (lst b) ≤ rank (lst a)
Tactic:
simp only [rank, Nat.succ_le_succ_iff, Finset.sup_le_iff]
State after:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (b_1 : Fin n✝), b_1 ∈ Finset.univ → rank (b b_1) ≤ Finset.sup Finset.univ fun i => rank (a i)

State before:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (b_1 : Fin n✝), b_1 ∈ Finset.univ → rank (b b_1) ≤ Finset.sup Finset.univ fun i => rank (a i)
Tactic:
intro i _
State after:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
a✝ : i ∈ Finset.univ
⊢ rank (b i) ≤ Finset.sup Finset.univ fun i => rank (a i)

State before:
case a
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
a✝ : i ∈ Finset.univ
⊢ rank (b i) ≤ Finset.sup Finset.univ fun i => rank (a i)
Tactic:
obtain ⟨j, hj⟩ := h₂ i
State after:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
a✝ : i ∈ Finset.univ
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ rank (b i) ≤ Finset.sup Finset.univ fun i => rank (a i)

State before:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
a✝ : i ∈ Finset.univ
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ rank (b i) ≤ Finset.sup Finset.univ fun i => rank (a i)
Tactic:
rw [← rank_eq_of_equiv hj]
State after:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
a✝ : i ∈ Finset.univ
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ rank (a j) ≤ Finset.sup Finset.univ fun i => rank (a i)

State before:
case a.intro
atoms : Type u_1
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₁ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₂ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
a✝ : i ∈ Finset.univ
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ rank (a j) ≤ Finset.sup Finset.univ fun i => rank (a i)
Tactic:
exact Finset.le_sup (f := fun i => rank (a i)) (Finset.mem_univ j)
State after:
no goals