awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
⊢ ε_ (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
have rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
Tactic: rw [epsilon_eq_deriv, epsilon_eq_deriv, deriv_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
⊢ ε_ (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
have rw₁ : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) =
  nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o))
Tactic: rw [epsilon_eq_deriv, epsilon_eq_deriv, deriv_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
rw₁ :
  deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) =
    nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o))
⊢ ε_ (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
have rw₂ : nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o)) =
  nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o))
Tactic: rw [epsilon_eq_deriv, epsilon_eq_deriv, deriv_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ ε_ 0 ≤ o
have rw : nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ≤ o
Tactic: rw [epsilon_zero_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
⊢ ω ^ ε_ o = ε_ o
have rw : ω ^ deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o = deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o
Tactic: rw [epsilon_eq_deriv, deriv_fp (isNormal_opow one_lt_omega0)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
rw : ω ^ deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o = deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o
⊢ ω ^ ε_ o = ε_ o
have rw₁ : deriv (fun (x : Ordinal.{u_1}) ↦ ω ^ x) o = deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o
Tactic: rw [epsilon_eq_deriv, deriv_fp (isNormal_opow one_lt_omega0)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
⊢ o < ε_ 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
have rw : o < nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
Tactic: rw [epsilon_zero_eq_nfp, lt_nfp_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
rw : o < nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
⊢ o < ε_ 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
have rw₁ : (∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0) ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
Tactic: rw [epsilon_zero_eq_nfp, lt_nfp_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
n : ℕ
⊢ (fun (a : Ordinal.{u_1}) ↦ ω ^ a)^[n] 0 < ε_ 0
have rw : (fun (a : Ordinal.{u_1}) ↦ ω ^ a)^[n] 0 < nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
Tactic: rw [epsilon_zero_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
n : ℕ
⊢ (fun (a : Ordinal.{u_1}) ↦ ω ^ a)^[n] 0 < nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
have h : 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0
Tactic: apply iterate_lt_nfp (isNormal_opow one_lt_omega0).strictMono
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
⊢ ω < ε_ o
have apply : ω < veblen 1 0
Tactic: apply lt_of_lt_of_le _ <| (veblen_right_strictMono _).monotone zero_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ Γ_ 0 ≤ o
have rw : nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ≤ o
Tactic: rw [gamma_zero_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
⊢ o < Γ_ 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
have rw : o < nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
Tactic: rw [gamma_zero_eq_nfp, lt_nfp_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
rw : o < nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
⊢ o < Γ_ 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
have rw₁ : (∃ (n : ℕ), o < (fun (x : Ordinal.{u}) ↦ veblen x 0)^[n] 0) ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
Tactic: rw [gamma_zero_eq_nfp, lt_nfp_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
n : ℕ
⊢ (fun (a : Ordinal.{u_1}) ↦ veblen a 0)^[n] 0 < Γ_ 0
have rw : (fun (a : Ordinal.{u_1}) ↦ veblen a 0)^[n] 0 < nfp (fun (x : Ordinal.{u_1}) ↦ veblen x 0) 0
Tactic: rw [gamma_zero_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
n : ℕ
⊢ (fun (a : Ordinal.{u_1}) ↦ veblen a 0)^[n] 0 < nfp (fun (x : Ordinal.{u_1}) ↦ veblen x 0) 0
have h : 0 < veblen 0 0
Tactic: apply iterate_lt_nfp veblen_zero_strictMono
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ o
have apply : ε_ 0 < Γ_ 0
Tactic: apply (gamma_le_gamma.2 zero_le).trans_lt'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₁ = Γ_ o
have rw : (veblen (Γ_ o) 0).invVeblen₁ = veblen (Γ_ o) 0
Tactic: rw [← veblen_gamma_zero, invVeblen₁_veblen veblen_pos, veblen_gamma_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
rw : (veblen (Γ_ o) 0).invVeblen₁ = veblen (Γ_ o) 0
⊢ (Γ_ o).invVeblen₁ = Γ_ o
have rw₁ : Γ_ o = veblen (Γ_ o) 0
Tactic: rw [← veblen_gamma_zero, invVeblen₁_veblen veblen_pos, veblen_gamma_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
rw : (veblen (Γ_ o) 0).invVeblen₁ = veblen (Γ_ o) 0
rw₁ : Γ_ o = veblen (Γ_ o) 0
⊢ (Γ_ o).invVeblen₁ = Γ_ o
have rw₂ : Γ_ o = Γ_ o
Tactic: rw [← veblen_gamma_zero, invVeblen₁_veblen veblen_pos, veblen_gamma_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₂ = 0
have rw : (veblen (Γ_ o) 0).invVeblen₂ = 0
Tactic: rw [← veblen_gamma_zero, invVeblen₂_veblen gamma_ne_zero veblen_pos]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u_1}
rw : (veblen (Γ_ o) 0).invVeblen₂ = 0
⊢ (Γ_ o).invVeblen₂ = 0
have rw₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
Tactic: rw [← veblen_gamma_zero, invVeblen₂_veblen gamma_ne_zero veblen_pos]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
⊢ o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ range Γ_
have mp : o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
mp : o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_
⊢ o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ range Γ_
have mpr : o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_
have mp : o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o
Tactic: rw [mem_range_gamma, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o
have mp : ∀ (h : o.invVeblen₁ = o) (ho : ¬o = 0), veblen o 0 ≤ o
Tactic: refine fun h ho ↦ (left_le_veblen ..).antisymm' ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| o
have rw : veblen o o.invVeblen₂
Tactic: rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
⊢ veblen o 0 ≤ o
have mp : veblen o 0 ≤ veblen o o.invVeblen₂
Tactic: conv_rhs => rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_
have rw : o.invVeblen₁ ≠ o ↔ o ≠ 0 ∧ o ∉ range Γ_
Tactic: rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
rw : o.invVeblen₁ ≠ o ↔ o ≠ 0 ∧ o ∉ range Γ_
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_
have rw₁ : ¬o.invVeblen₁ = o ↔ o ≠ 0 ∧ o ∉ range Γ_
Tactic: rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
rw : o.invVeblen₁ ≠ o ↔ o ≠ 0 ∧ o ∉ range Γ_
rw₁ : ¬o.invVeblen₁ = o ↔ o ≠ 0 ∧ o ∉ range Γ_
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_
have rw₂ : ¬(o = 0 ∨ o ∈ range Γ_ ) ↔ o ≠ 0 ∧ o ∉ range Γ_
Tactic: rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
rw : o.invVeblen₁ ≠ o ↔ o ≠ 0 ∧ o ∉ range Γ_
rw₁ : ¬o.invVeblen₁ = o ↔ o ≠ 0 ∧ o ∉ range Γ_
rw₂ : ¬(o = 0 ∨ o ∈ range Γ_ ) ↔ o ≠ 0 ∧ o ∉ range Γ_
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_
have rw₃ : ¬o = 0 ∧ o ∉ range Γ_ ↔ o ≠ 0 ∧ o ∉ range Γ_
Tactic: rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ out f xs ≈ out f ys
have rw : (f fun (x : Fin n) ↦ ZFSet.mk (xs x)) = f fun (x : Fin n) ↦ ZFSet.mk (ys x)
Tactic: rw [← Quotient.eq_iff_equiv, mk_eq, mk_eq, mk_out, mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x_1 y_1 z x y : ZFSet.{u}
hxy : x.toSet = y.toSet
⊢ x = y
have a : ∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet
Tactic: apply ext_aux
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
⊢ Small.{u, u + 1} ↥(⟦a⟧)
have suffices : Function.Surjective f
Tactic: suffices Function.Surjective f by exact small_of_surjective this
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x_1 y_1 z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
y : ZFSet.{u}
hb : y ∈ mk a
⊢ ∃ (a_1 : a.Type), f a_1 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) y hb
have h : ∀ (a_1 : PSet.{u}) (hb : ⟦a_1⟧ ∈ mk a),
  ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ hb
Tactic: induction y using Quotient.inductionOn
Cleared hypotheses: y, hb
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
a_1 : PSet.{u}
hb : ⟦a_1⟧ ∈ mk a
⊢ ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ hb
have h : ∀ (i : a.Type) (h : a_1.Equiv (a.Func i)),
  ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ sorry
Tactic: obtain ⟨i, h⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
⊢ (↑∅ : Set ZFSet.{u}) = ∅
have h : ∀ (x : ZFSet.{u}), x ∈ (↑∅ : Set ZFSet.{u}) ↔ Membership.mem (γ := Set ZFSet.{u}) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x : PSet.{u_1}
⊢ ZFSet.Nonempty.{u_1} (mk x) ↔ x.Nonempty
have refine : ZFSet.Nonempty.{u_1} (mk x) → x.Nonempty
Tactic: refine ⟨?_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x : PSet.{u_1}
a : ZFSet.{u_1}
h : a ∈ (↑(mk x) : Set ZFSet.{u_1})
⊢ x.Nonempty
have h₁ : ∀ (a : PSet.{u_1}) (h : ⟦a⟧ ∈ (↑(mk x) : Set ZFSet.{u_1})), x.Nonempty
Tactic: induction a using Quotient.inductionOn
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
u : ZFSet.{u_1}
⊢ u = ∅ ∨ u.Nonempty
have rw : (¬∃ (x : ZFSet.{u_1}), x ∈ u) ∨ u.Nonempty
Tactic: rw [eq_empty, ← not_exists]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
⊢ (↑(insert x y) : Set ZFSet.{u_1}) = insert x (↑y : Set ZFSet.{u_1})
have h : ∀ (x_1 : ZFSet.{u_1}), x_1 ∈ (↑(insert x y) : Set ZFSet.{u_1}) ↔ x_1 ∈ insert x (↑y : Set ZFSet.{u_1})
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x : ZFSet.{u_1}
⊢ (↑{x} : Set ZFSet.{u_1}) = {x}
have h : ∀ (x_1 : ZFSet.{u_1}), x_1 ∈ (↑{x} : Set ZFSet.{u_1}) ↔ Membership.mem (γ := Set ZFSet.{u_1}) {x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {x, x} {x}
have a : ∀ (z : ZFSet.{u_1}), Membership.mem (γ := ZFSet.{u_1}) {x, x} z ↔ Membership.mem (γ := ZFSet.{u_1}) {x} z
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y z : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {x, y} {z} ↔ x = z ∧ y = z
have refine_1 : ∀ (h : Eq (α := ZFSet.{u_1}) {x, y} {z}), x = z ∧ y = z
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y z : ZFSet.{u_1}
refine_1 : ∀ (h : Eq (α := ZFSet.{u_1}) {x, y} {z}), x = z ∧ y = z
⊢ Eq (α := ZFSet.{u_1}) {x, y} {z} ↔ x = z ∧ y = z
have refine_2 : x = z ∧ y = z → Eq (α := ZFSet.{u_1}) {x, y} {z}
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y z : ZFSet.{u_1}
h : Eq (α := ZFSet.{u_1}) {x, y} {z}
⊢ x = z ∧ y = z
have refine_1 : Membership.mem (γ := ZFSet.{u_1}) {z} x ∧ Membership.mem (γ := ZFSet.{u_1}) {z} y
Tactic: rw [← mem_singleton, ← mem_singleton]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y z : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {x} {y, z} ↔ x = y ∧ x = z
have rw : y = x ∧ z = x ↔ x = y ∧ x = z
Tactic: rw [eq_comm, pair_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
n_1 : ZFSet.{u}
x : PSet.{u}
h_1 : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))
have rw : insert (mk (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })) (mk (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })) =
  insert (mk (ofNat n)) (mk (ofNat n))
Tactic: rw [ZFSet.sound h]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ (↑(ZFSet.sep p a) : Set ZFSet.{u_1}) = {x : ZFSet.{u_1} | x ∈ a ∧ p x}
have h : ∀ (x : ZFSet.{u_1}),
  x ∈ (↑(ZFSet.sep p a) : Set ZFSet.{u_1}) ↔ Membership.mem (γ := Set ZFSet.{u_1}) {x : ZFSet.{u_1} | x ∈ a ∧ p x} x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
have let : ∀ (b : β) (hb : PSet.Equiv.{u, u} (A a) (B b)),
  ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
Tactic: let ⟨b, hb⟩ := αβ a
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : PSet.Equiv.{u, u} (A a) (B b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
have mk : ∀ (γ : Type u) (Γ : γ → PSet.{u}),
  (∀ (a_1 : γ) (ea : A a = Γ a_1),
      ∃ (b : (⋃₀ PSet.mk β B).Type),
        PSet.Equiv.{u, u}
          ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
          ((⋃₀ PSet.mk β B).Func b)) →
    ∀ (ea : A a = PSet.mk γ Γ),
      ∃ (b : (⋃₀ PSet.mk β B).Type),
        PSet.Equiv.{u, u}
          ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
          ((⋃₀ PSet.mk β B).Func b)
Tactic: induction ea : A a with | _ γ Γ
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : PSet.Equiv.{u, u} (A a) (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
have mk : ∀ (δ : Type u) (Δ : δ → PSet.{u}),
  (∀ (a_1 : δ) (eb : B b = Δ a_1),
      ∃ (b : (⋃₀ PSet.mk β B).Type),
        PSet.Equiv.{u, u}
          ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
          ((⋃₀ PSet.mk β B).Func b)) →
    ∀ (eb : B b = PSet.mk δ Δ),
      ∃ (b : (⋃₀ PSet.mk β B).Type),
        PSet.Equiv.{u, u}
          ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
          ((⋃₀ PSet.mk β B).Func b)
Tactic: induction eb : B b with | _ δ Δ
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : PSet.Equiv.{u, u} (A a) (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
have mk : (∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)) →
  ∀ (ea : A a = PSet.mk γ Γ) (δ : Type u) (Δ : δ → PSet.{u}) (hb : PSet.Equiv.{u, u} (PSet.mk γ Γ) (PSet.mk δ Δ)),
    (∀ (a_1 : δ) (eb : B b = Δ a_1),
        ∃ (b : (⋃₀ PSet.mk β B).Type),
          PSet.Equiv.{u, u}
            ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
            ((⋃₀ PSet.mk β B).Func b)) →
      ∀ (eb : B b = PSet.mk δ Δ),
        ∃ (b : (⋃₀ PSet.mk β B).Type),
          PSet.Equiv.{u, u}
            ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
            ((⋃₀ PSet.mk β B).Func b)
Tactic: rw [ea, eb] at hb
Cleared hypotheses: hb, A_ih, ea, δ, Δ, A_ih_1, eb
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
hb : PSet.Equiv.{u, u} (PSet.mk γ Γ) (PSet.mk δ Δ)
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
have γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
Tactic: obtain ⟨γδ, δγ⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
hb : PSet.Equiv.{u, u} (PSet.mk γ Γ) (PSet.mk δ Δ)
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)
have δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
Tactic: obtain ⟨γδ, δγ⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
⊢ γ
have rwa : (c : (PSet.mk γ Γ).Type) → γ
Tactic: rwa [ea] at c
Cleared hypotheses: c