Theorem: HFSet.rank_def (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ rank x = Finset.sup (toFinset x) rank + 1
Tactic:
apply le_antisymm
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ Finset.sup (toFinset x) rank + 1 ≤ rank x

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ Finset.sup (toFinset x) rank + 1 ≤ rank x
Tactic:
swap
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ Finset.sup (toFinset x) rank + 1 ≤ rank x

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ Finset.sup (toFinset x) rank + 1 ≤ rank x
Tactic:
rw [Nat.succ_le_iff, Finset.sup_lt_iff]
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ ∀ (b : HFSet atoms), b ∈ toFinset x → rank b < rank x

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ ⊥ < rank x

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ ∀ (b : HFSet atoms), b ∈ toFinset x → rank b < rank x
Tactic:
intro
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
b✝ : HFSet atoms
⊢ b✝ ∈ toFinset x → rank b✝ < rank x

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
b✝ : HFSet atoms
⊢ b✝ ∈ toFinset x → rank b✝ < rank x
Tactic:
simpa using rank_lt_of_mem
State after:
no goals

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ ⊥ < rank x
Tactic:
contrapose! h
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : rank x ≤ ⊥
⊢ isAtom x ≠ false

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : rank x ≤ ⊥
⊢ isAtom x ≠ false
Tactic:
simpa using h
State after:
no goals

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
by_cases H : (toFinset x).Nonempty
State after:
case pos
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

case neg
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : ¬Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case pos
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

case neg
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : ¬Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
swap
State after:
case neg
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : ¬Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

case pos
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case neg
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : ¬Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
simp only [Finset.not_nonempty_iff_eq_empty, toFinset_eq_empty_iff, h, false_or] at H
State after:
case neg
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : x = ∅
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case neg
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : x = ∅
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
simp [H]
State after:
no goals

State before:
case pos
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
H : Finset.Nonempty (toFinset x)
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
rcases H with ⟨z, hz⟩
State after:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
z : HFSet atoms
hz : z ∈ toFinset x
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
z : HFSet atoms
hz : z ∈ toFinset x
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
rw [mem_toFinset_iff] at hz
State after:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
z : HFSet atoms
hz : z ∈ x
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
z : HFSet atoms
hz : z ∈ x
⊢ rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
revert h hz
State after:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x z : HFSet atoms
⊢ isAtom x = false → z ∈ x → rank x ≤ Finset.sup (toFinset x) rank + 1

State before:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x z : HFSet atoms
⊢ isAtom x = false → z ∈ x → rank x ≤ Finset.sup (toFinset x) rank + 1
Tactic:
refine Quotient.inductionOn₂ x z fun x z h hz => ?_
State after:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
⊢ rank (Quotient.mk PreHFSet.instSetoidPreHFSet x) ≤
    Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank + 1

State before:
case pos.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
⊢ rank (Quotient.mk PreHFSet.instSetoidPreHFSet x) ≤
    Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank + 1
Tactic:
obtain ⟨y, hy, hr⟩ := PreHFSet.exists_mem_rank_eq_rank_succ ⟨z, hz⟩
State after:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ rank (Quotient.mk PreHFSet.instSetoidPreHFSet x) ≤
    Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank + 1

State before:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ rank (Quotient.mk PreHFSet.instSetoidPreHFSet x) ≤
    Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank + 1
Tactic:
conv_lhs => dsimp only [rank]
State after:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ Quotient.lift (fun x => PreHFSet.rank x) (_ : ∀ (x y : PreHFSet atoms), x ≈ y → PreHFSet.rank x = PreHFSet.rank y)
      (Quotient.mk PreHFSet.instSetoidPreHFSet x) ≤
    Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank + 1

State before:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ Quotient.lift (fun x => PreHFSet.rank x) (_ : ∀ (x y : PreHFSet atoms), x ≈ y → PreHFSet.rank x = PreHFSet.rank y)
      (Quotient.mk PreHFSet.instSetoidPreHFSet x) ≤
    Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank + 1
Tactic:
simp only [Quotient.lift_mk, hr, add_le_add_iff_right, bot_eq_zero']
State after:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ PreHFSet.rank y ≤ Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank

State before:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ PreHFSet.rank y ≤ Finset.sup (toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)) rank
Tactic:
refine Finset.le_sup (f := rank) (b := ⟦y⟧) ?_
State after:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet y ∈ toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)

State before:
case pos.intro.intro.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ z✝ : HFSet atoms
x z : PreHFSet atoms
h : isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet x) = false
hz : Quotient.mk PreHFSet.instSetoidPreHFSet z ∈ Quotient.mk PreHFSet.instSetoidPreHFSet x
y : PreHFSet atoms
hy : y ∈ x
hr : PreHFSet.rank x = PreHFSet.rank y + 1
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet y ∈ toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet x)
Tactic:
simpa using hy
State after:
no goals