internlm/Lean-Github huggingface dataset:
Theorem: HEq.funext'
Proof state before:
case refl
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (∀ (x : α₁), HEq (f₁ x) (f₂ (cast ⋯ x))) → HEq f₁ f₂
Tactic:
apply HEq.funext
Proof state after:
case refl.type_eq
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (fun x => β₁ x) = fun x => β₂ (cast ⋯ x)
Theorem: HEq.funext'
Proof state before:
case refl.type_eq
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (fun x => β₁ x) = fun x => β₂ (cast ⋯ x)
Tactic:
funext x
Proof state after:
case refl.type_eq.h
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
x : α₁
⊢ β₁ x = β₂ (cast ⋯ x)
Theorem: HEq.funext'
Proof state before:
case refl.type_eq.h
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
x : α₁
⊢ β₁ x = β₂ (cast ⋯ x)
Tactic:
apply type_eq_β
Proof state after:
no goals
Theorem: flatten_atom
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : atoms
⊢ flatten (atom x) = {x}
Tactic:
rw [flatten, dif_pos] <;> simp
Proof state after:
no goals
Theorem: flatten_ofFinset
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
⊢ flatten (ofFinset s) = Finset.biUnion s fun x => flatten x
Tactic:
rw [flatten, dif_neg] <;> simp [Finset.sup_eq_biUnion]
Proof state after:
no goals
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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)
⊢ insert x (lst a) ≈ insert y (lst b)
Tactic:
constructor
Proof state after:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹ + 1)), ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)

case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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)
⊢ ∀ (j : Fin (n✝ + 1)), ∃ i, Equiv (Fin.cons x a i) (Fin.cons y b j)
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹ + 1)), ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)
Tactic:
intro i
Proof state after:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹ + 1)
⊢ ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹ + 1)
⊢ ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)
Tactic:
induction' i using Fin.cases with i
Proof state after:
case left.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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)
⊢ ∃ j, Equiv (Fin.cons x a 0) (Fin.cons y b j)

case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case left.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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)
⊢ ∃ j, Equiv (Fin.cons x a 0) (Fin.cons y b j)
Tactic:
exact ⟨0, h⟩
Proof state after:
no goals
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)
Tactic:
let ⟨j, hj⟩ := h₂ i
Proof state after:
case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝¹
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)
Tactic:
exact ⟨j.succ, hj⟩
Proof state after:
no goals
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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)
⊢ ∀ (j : Fin (n✝ + 1)), ∃ i, Equiv (Fin.cons x a i) (Fin.cons y b j)
Tactic:
intro i
Proof state after:
case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝ + 1)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b i)
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝ + 1)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b i)
Tactic:
induction' i using Fin.cases with i
Proof state after:
case right.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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, Equiv (Fin.cons x a i) (Fin.cons y b 0)

case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case right.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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, Equiv (Fin.cons x a i) (Fin.cons y b 0)
Tactic:
exact ⟨0, h⟩
Proof state after:
no goals
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))
Tactic:
let ⟨j, hj⟩ := h₃ i
Proof state after:
case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))
Theorem: PreHFSet.insert_equiv_of_equiv
Proof state before:
case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
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✝
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))
Tactic:
exact ⟨j.succ, hj⟩
Proof state after:
no goals
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
atoms : Type u_1
x y z : PreHFSet atoms
a : atoms
⊢ x ∈ insert y (atom a) → isAtom (atom a) = false ∧ (x ≈ y ∨ x ∈ atom a)
Tactic:
simp [insert, isAtom, Membership.mem, Mem]
Proof state after:
no goals
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
⊢ x ∈ insert y (lst b) → isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
rintro ⟨i, hi⟩
Proof state after:
case intro
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi : x ≈ Fin.cons y b i
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
case intro
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi : x ≈ Fin.cons y b i
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
induction' i using Fin.cases with i
Proof state after:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)

case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
refine ⟨rfl, Or.inl ?_⟩
Proof state after:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ x ≈ y
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ x ≈ y
Tactic:
simpa using hi
Proof state after:
no goals
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
refine ⟨rfl, Or.inr ⟨i, ?_⟩⟩
Proof state after:
case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ x ≈ b i
Theorem: PreHFSet.eq_or_mem_of_mem_insert
Proof state before:
case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ x ≈ b i
Tactic:
simpa using hi
Proof state after:
no goals
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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]
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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 _
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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]
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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)
Proof state after:
no goals
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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]
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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 _
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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]
Proof 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)
Theorem: PreHFSet.rank_eq_of_equiv
Proof 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)
Proof state after:
no goals
Theorem: PreHFSet.rank_eq_zero_iff
Proof state before:
atoms : Type u_1
a✝ : atoms
⊢ rank (atom a✝) = 0 ↔ isAtom (atom a✝) = true
Tactic:
simp [rank, isAtom]
Proof state after:
no goals
Theorem: PreHFSet.rank_eq_zero_iff
Proof state before:
atoms : Type u_1
n✝ : ℕ
a✝ : Fin n✝ → PreHFSet atoms
⊢ rank (lst a✝) = 0 ↔ isAtom (lst a✝) = true
Tactic:
simp [rank, isAtom]
Proof state after:
no goals
Theorem: PreHFSet.rank_lt_of_mem
Proof 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]
Proof 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)
Theorem: PreHFSet.rank_lt_of_mem
Proof 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⟩
Proof 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)
Theorem: PreHFSet.rank_lt_of_mem
Proof 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]
Proof 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)
Theorem: PreHFSet.rank_lt_of_mem
Proof 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)
Proof state after:
no goals
Theorem: PreHFSet.exists_mem_rank_eq_rank_succ
Proof 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))
Proof 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
Theorem: PreHFSet.exists_mem_rank_eq_rank_succ
Proof 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⟩, ?_⟩
Proof 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
Theorem: PreHFSet.exists_mem_rank_eq_rank_succ
Proof 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]
Proof state after:
no goals
Theorem: PreHFSet.mem_toList_iff
Proof state before:
atoms : Type u_1
x y : PreHFSet atoms
a✝ : atoms
⊢ x ∈ atom a✝ ↔ ∃ x', x' ∈ toList (atom a✝) ∧ x' ≈ x
Tactic:
simp [toList, not_mem_atom]
Proof state after:
no goals
Theorem: PreHFSet.mem_toList_iff
Proof state before:
atoms : Type u_1
x y : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
x✝ : ∃ x', x' ∈ toList (lst b) ∧ x' ≈ x
x' : PreHFSet atoms
h₁ : x' ∈ toList (lst b)
h₂ : x' ≈ x
⊢ x ∈ lst b
Tactic:
obtain ⟨i, rfl⟩ := (List.mem_ofFn _ _).mp h₁
Proof state after:
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