internlm/Lean-Github huggingface dataset:
Theorem: PreHFSet.mem_toList_iff
Proof state before:
case intro
atoms : Type u_1
x y : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
x✝ : ∃ x', x' ∈ toList (lst b) ∧ x' ≈ x
i : Fin n✝
h₁ : b i ∈ toList (lst b)
h₂ : b i ≈ x
⊢ x ∈ lst b
Tactic:
exact ⟨i, h₂.symm⟩
Proof state after:
no goals
Theorem: HFSet.eq_or_mem_of_mem_insert
Proof state before:
atoms : Type u_1
x✝ y✝ z✝ : HFSet atoms
x y z : PreHFSet atoms
h :
  Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
    insert (Quotient.mk PreHFSet.instSetoidPreHFSet y) (Quotient.mk PreHFSet.instSetoidPreHFSet z)
⊢ isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet z) = false ∧
    (Quotient.mk PreHFSet.instSetoidPreHFSet x = Quotient.mk PreHFSet.instSetoidPreHFSet y ∨
      Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet z)
Tactic:
rw [Quotient.eq]
Proof state after:
atoms : Type u_1
x✝ y✝ z✝ : HFSet atoms
x y z : PreHFSet atoms
h :
  Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
    insert (Quotient.mk PreHFSet.instSetoidPreHFSet y) (Quotient.mk PreHFSet.instSetoidPreHFSet z)
⊢ isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet z) = false ∧
    (x ≈ y ∨ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet z)
Theorem: HFSet.eq_or_mem_of_mem_insert
Proof state before:
atoms : Type u_1
x✝ y✝ z✝ : HFSet atoms
x y z : PreHFSet atoms
h :
  Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
    insert (Quotient.mk PreHFSet.instSetoidPreHFSet y) (Quotient.mk PreHFSet.instSetoidPreHFSet z)
⊢ isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet z) = false ∧
    (x ≈ y ∨ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet z)
Tactic:
exact PreHFSet.eq_or_mem_of_mem_insert h
Proof state after:
no goals
Theorem: HFSet.mem_insert_iff
Proof state before:
atoms : Type u_1
x y z : HFSet atoms
⊢ x ∈ insert y z ↔ isAtom z = false ∧ (x = y ∨ x ∈ z)
Tactic:
constructor
Proof state after:
case mp
atoms : Type u_1
x y z : HFSet atoms
⊢ x ∈ insert y z → isAtom z = false ∧ (x = y ∨ x ∈ z)

case mpr
atoms : Type u_1
x y z : HFSet atoms
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z) → x ∈ insert y z
Theorem: HFSet.mem_insert_iff
Proof state before:
case mp
atoms : Type u_1
x y z : HFSet atoms
⊢ x ∈ insert y z → isAtom z = false ∧ (x = y ∨ x ∈ z)
Tactic:
intro h
Proof state after:
case mp
atoms : Type u_1
x y z : HFSet atoms
h : x ∈ insert y z
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z)
Theorem: HFSet.mem_insert_iff
Proof state before:
case mp
atoms : Type u_1
x y z : HFSet atoms
h : x ∈ insert y z
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z)
Tactic:
exact eq_or_mem_of_mem_insert h
Proof state after:
no goals
Theorem: HFSet.mem_insert_iff
Proof state before:
case mpr
atoms : Type u_1
x y z : HFSet atoms
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z) → x ∈ insert y z
Tactic:
rintro ⟨h₁, rfl|h₂⟩
Proof state after:
case mpr.intro.inl
atoms : Type u_1
x z : HFSet atoms
h₁ : isAtom z = false
⊢ x ∈ insert x z

case mpr.intro.inr
atoms : Type u_1
x y z : HFSet atoms
h₁ : isAtom z = false
h₂ : x ∈ z
⊢ x ∈ insert y z
Theorem: HFSet.mem_insert_iff
Proof state before:
case mpr.intro.inl
atoms : Type u_1
x z : HFSet atoms
h₁ : isAtom z = false
⊢ x ∈ insert x z
Tactic:
exact mem_insert_self _ _ h₁
Proof state after:
no goals
Theorem: HFSet.mem_insert_iff
Proof state before:
case mpr.intro.inr
atoms : Type u_1
x y z : HFSet atoms
h₁ : isAtom z = false
h₂ : x ∈ z
⊢ x ∈ insert y z
Tactic:
exact mem_insert_of_mem h₂
Proof state after:
no goals
Theorem: HFSet.ofMultiset_cons
Proof state before:
atoms : Type u_1
s : Multiset (HFSet atoms)
x : HFSet atoms
⊢ ofMultiset (x ::ₘ s) = insert x (ofMultiset s)
Tactic:
simp [ofMultiset]
Proof state after:
no goals
Theorem: HFSet.ofMultiset_isAtom
Proof state before:
atoms : Type u_1
s : Multiset (HFSet atoms)
⊢ isAtom (ofMultiset 0) = false
Tactic:
simp [ofMultiset]
Proof state after:
no goals
Theorem: HFSet.ofMultiset_isAtom
Proof state before:
atoms : Type u_1
s✝ : Multiset (HFSet atoms)
y : HFSet atoms
s : Multiset (HFSet atoms)
ih : isAtom (ofMultiset s) = false
⊢ isAtom (ofMultiset (y ::ₘ s)) = false
Tactic:
simpa
Proof state after:
no goals
Theorem: HFSet.mem_ofMultiset_iff
Proof state before:
atoms : Type u_1
s : Multiset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ ofMultiset 0 ↔ x ∈ 0
Tactic:
simp [ofMultiset]
Proof state after:
no goals
Theorem: HFSet.mem_ofMultiset_iff
Proof state before:
atoms : Type u_1
s✝ : Multiset (HFSet atoms)
x y : HFSet atoms
s : Multiset (HFSet atoms)
ih : x ∈ ofMultiset s ↔ x ∈ s
⊢ x ∈ ofMultiset (y ::ₘ s) ↔ x ∈ y ::ₘ s
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: HFSet.mem_ofFinset_iff
Proof state before:
atoms : Type u_1
s : Finset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ ofFinset s ↔ x ∈ s
Tactic:
simp [ofFinset]
Proof state after:
no goals
Theorem: HFSet.mem_toFinset_iff
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet s) ↔
    Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Tactic:
rw [toFinset, Quotient.lift_mk, List.mem_toFinset (a := ⟦x⟧)]
Proof state after:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
      List.map (fun z => Quotient.mk PreHFSet.instSetoidPreHFSet z) (PreHFSet.toList s) ↔
    Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Theorem: HFSet.mem_toFinset_iff
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
      List.map (fun z => Quotient.mk PreHFSet.instSetoidPreHFSet z) (PreHFSet.toList s) ↔
    Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Tactic:
simp only [List.mem_map, Quotient.eq, ← PreHFSet.mem_toList_iff]
Proof state after:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ x ∈ s ↔ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Theorem: HFSet.mem_toFinset_iff
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ x ∈ s ↔ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Tactic:
rfl
Proof state after:
no goals
Theorem: HFSet.toFinset_ofFinset
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
s : HFSet atoms
hs : isAtom s = false
⊢ ofFinset (toFinset s) = s
Tactic:
ext x <;> simp [hs]
Proof state after:
no goals
Theorem: HFSet.ofFinset_toFinset
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
⊢ toFinset (ofFinset s) = s
Tactic:
ext x
Proof state after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ toFinset (ofFinset s) ↔ x ∈ s
Theorem: HFSet.ofFinset_toFinset
Proof state before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ toFinset (ofFinset s) ↔ x ∈ s
Tactic:
simp
Proof state after:
no goals
Theorem: HFSet.ofFinset_insert
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
s : Finset (HFSet atoms)
⊢ ofFinset (insert x s) = insert x (ofFinset s)
Tactic:
ext z <;> simp
Proof state after:
no goals
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ x = ∅
Tactic:
ext z
Proof state after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom x = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom x = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Tactic:
simpa using h'
Proof state after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Tactic:
simp
Proof state after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
⊢ isAtom x = true ∨ x = ∅ → toFinset x = ∅
Tactic:
rintro (h'|rfl)
Proof state after:
case inl
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h' : isAtom x = true
⊢ toFinset x = ∅

case inr
atoms : Type u_1
inst✝ : DecidableEq atoms
⊢ toFinset ∅ = ∅
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
case inl
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h' : isAtom x = true
⊢ toFinset x = ∅
Tactic:
obtain ⟨a, rfl⟩ := isAtom_eq_true_iff.mp h'
Proof state after:
case inl.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
a : atoms
h' : isAtom (atom a) = true
⊢ toFinset (atom a) = ∅
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
case inl.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
a : atoms
h' : isAtom (atom a) = true
⊢ toFinset (atom a) = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: HFSet.toFinset_eq_empty_iff
Proof state before:
case inr
atoms : Type u_1
inst✝ : DecidableEq atoms
⊢ toFinset ∅ = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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]
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof state after:
no goals
Theorem: HFSet.rank_def
Proof state before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : isAtom x = false
⊢ ⊥ < rank x
Tactic:
contrapose! h
Proof state after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : rank x ≤ ⊥
⊢ isAtom x ≠ false
Theorem: HFSet.rank_def
Proof state before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : rank x ≤ ⊥
⊢ isAtom x ≠ false
Tactic:
simpa using h
Proof state after:
no goals
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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]
Proof state after:
no goals
Theorem: HFSet.rank_def
Proof 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⟩
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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
Proof 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
Theorem: HFSet.rank_def
Proof 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 => ?_
Proof 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
Theorem: HFSet.rank_def
Proof 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⟩
Proof 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
Theorem: HFSet.rank_def
Proof 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]
Proof 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
Theorem: HFSet.rank_def
Proof 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']
Proof 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
Theorem: HFSet.rank_def
Proof 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⟧) ?_
Proof 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)
Theorem: HFSet.rank_def
Proof 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
Proof state after:
no goals
Theorem: HFSet.rank_ofFinset
Proof state before:
atoms : Type u_1
s : Finset (HFSet atoms)
⊢ rank (ofFinset s) = Finset.sup s rank + 1
Tactic:
classical
rw [rank_def] <;> simp
Proof state after:
no goals
Theorem: HFSet.rank_ofFinset
Proof state before:
atoms : Type u_1
s : Finset (HFSet atoms)
⊢ rank (ofFinset s) = Finset.sup s rank + 1
Tactic:
rw [rank_def] <;> simp
Proof state after:
no goals
Theorem: HFSet.induction'
Proof state before:
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
⊢ motive y
Tactic:
cases H : y.isAtom
Proof state after:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y

case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y
Theorem: HFSet.induction'
Proof state before:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y

case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y
Tactic:
swap
Proof state after:
case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y

case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y