awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∃ (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)
have mk : ∀ (d : δ) (hd : PSet.Equiv.{u, u} (Γ (Eq.mp sorry c)) (Δ d)),
  ∃ (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)
Tactic: let ⟨d, hd⟩ := γδ (by rwa [ea] at c)
-- 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
d : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
⊢ ∃ (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)
have h : 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
    (Sigma.mk (β := fun (x : (PSet.mk β B).Type) ↦ ((PSet.mk β B).Func x).Type) b (Eq.ndrec (motive := «Type») d sorry)))
Tactic: use ⟨b, Eq.ndrec d (Eq.symm eb)⟩
-- 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
d : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
⊢ 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
      (Sigma.mk (β := fun (x : (PSet.mk β B).Type) ↦ ((PSet.mk β B).Func x).Type) b (Eq.ndrec (motive := «Type») d ⋯)))
have h : PSet.Equiv.{u, u} ((A a).Func c) ((B b).Func (Eq.ndrec (motive := «Type») d sorry))
Tactic: change PSet.Equiv ((A a).Func c) ((B b).Func (Eq.ndrec d eb.symm))
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ y ∈ ZFSet.sep (fun (y : ZFSet.{u_1}) ↦ ∀ z ∈ x, y ∈ z) (⋃₀ x) ↔ ∀ z ∈ x, y ∈ z
have simp : (∀ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
Tactic: simp only [and_iff_right_iff_imp, mem_sep]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋃₀ x
have apply : ∃ z ∈ x, y ∈ z
Tactic: apply mem_sUnion.mpr
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ ∃ z ∈ x, y ∈ z
have replace : ∀ (s : ZFSet.{u_1}) (h : s ∈ (↑x : Set ZFSet.{u_1})), ∃ z ∈ x, y ∈ z
Tactic: replace ⟨s, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
⊢ ⋃₀ ∅ = ∅
have a : ∀ (z : ZFSet.{u}), z ∈ ⋃₀ ∅ ↔ Membership.mem (γ := ZFSet.{u}) ∅ z
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
have inl : ∀ (hy : y ∈ ⋂₀ ∅) (hz : Membership.mem (γ := ZFSet.{u_1}) ∅ z), y ∈ z
Tactic: rcases eq_empty_or_nonempty x with (rfl | hx)
Cleared hypotheses: x, hy, hz
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
inl : ∀ (hy : y ∈ ⋂₀ ∅) (hz : Membership.mem (γ := ZFSet.{u_1}) ∅ z), y ∈ z
⊢ y ∈ z
have inr : ∀ (hx : x.Nonempty), y ∈ z
Tactic: rcases eq_empty_or_nonempty x with (rfl | hx)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x
have simp_rw : (∃ (z : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x} z ∧ y ∈ z) ↔ y ∈ x
Tactic: simp_rw [mem_sUnion, mem_singleton, exists_eq_left]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
simp_rw : (∃ (z : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x} z ∧ y ∈ z) ↔ y ∈ x
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x
have simp_rw₁ : (∃ (z : ZFSet.{u}), z = x ∧ y ∈ z) ↔ y ∈ x
Tactic: simp_rw [mem_sUnion, mem_singleton, exists_eq_left]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x
have simp_rw : (∀ (z : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x} z → y ∈ z) ↔ y ∈ x
Tactic: simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
simp_rw : (∀ (z : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x} z → y ∈ z) ↔ y ∈ x
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x
have simp_rw₁ : (∀ (z : ZFSet.{u}), z = x → y ∈ z) ↔ y ∈ x
Tactic: simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x : ZFSet.{u}
⊢ (↑(⋃₀ x) : Set ZFSet.{u}) = ⋃₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))
have h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(⋃₀ x) : Set ZFSet.{u}) ↔ x_1 ∈ ⋃₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x : ZFSet.{u}
h : x.Nonempty
⊢ (↑(⋂₀ x) : Set ZFSet.{u}) = ⋂₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))
have h₁ : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(⋂₀ x) : Set ZFSet.{u}) ↔ x_1 ∈ ⋂₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
H : Eq (α := ZFSet.{u_1}) {x} {y}
this : ⋃₀ {x} = ⋃₀ {y} := ⋯
⊢ x = y
have rwa : ∀ (this : x = ⋃₀ {y}), x = y
Tactic: rwa [sUnion_singleton, sUnion_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
H : Eq (α := ZFSet.{u_1}) {x} {y}
this : ⋃₀ {x} = ⋃₀ {y} := ⋯
rwa : ∀ (this : x = ⋃₀ {y}), x = y
⊢ x = y
have rwa₁ : ∀ (this : x = y), x = y
Tactic: rwa [sUnion_singleton, sUnion_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
⊢ (↑(x ∪ y) : Set ZFSet.{u}) = (↑x : Set ZFSet.{u}) ∪ (↑y : Set ZFSet.{u})
have h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(x ∪ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) ∪ (↑y : Set ZFSet.{u})
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
⊢ (↑(x ∩ y) : Set ZFSet.{u}) = (↑x : Set ZFSet.{u}) ∩ (↑y : Set ZFSet.{u})
have h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(x ∩ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) ∩ (↑y : Set ZFSet.{u})
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
⊢ (↑(x \ y) : Set ZFSet.{u}) = (↑x : Set ZFSet.{u}) \ (↑y : Set ZFSet.{u})
have h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(x \ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) \ (↑y : Set ZFSet.{u})
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
hxy : x ⊆ y
⊢ x ∩ y = x
have a : ∀ (z : ZFSet.{u}), z ∈ x ∩ y ↔ z ∈ x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u}
hyx : y ⊆ x
⊢ x ∩ y = y
have a : ∀ (z : ZFSet.{u}), z ∈ x ∩ y ↔ z ∈ y
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y : ZFSet.{u_1}
⊢ insert x y = {x} ∪ y
have a : ∀ (z : ZFSet.{u_1}), z ∈ insert x y ↔ z ∈ {x} ∪ y
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
x_1 x_2 : PSet.{u}
α : Type u
A : α → PSet.{u}
h : ⟦x_2⟧ ∈ ⟦PSet.mk α A⟧
a : (PSet.mk α A).Type
ya : x_2.Equiv ((PSet.mk α A).Func a)
⊢ f ⟦x_2⟧ ∈ image f ⟦PSet.mk α A⟧
have simp : ZFSet.mk (Definable₁.out f x_2) ∈ image f (ZFSet.mk (PSet.mk α A))
Tactic: simp only [mk_eq, ← Definable₁.mk_out (f := f)]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst : Definable₁ f
x : ZFSet.{u_1}
⊢ (↑(image f x) : Set ZFSet.{u_1}) = f '' (↑x : Set ZFSet.{u_1})
have h : ∀ (x_1 : ZFSet.{u_1}), x_1 ∈ (↑(image f x) : Set ZFSet.{u_1}) ↔ x_1 ∈ f '' (↑x : Set ZFSet.{u_1})
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f ↔ ∃ (i : α), f i = ⟦y⟧
have mp : ⟦y⟧ ∈ range f → ∃ (i : α), f i = ⟦y⟧
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
mp : ⟦y⟧ ∈ range f → ∃ (i : α), f i = ⟦y⟧
⊢ ⟦y⟧ ∈ range f ↔ ∃ (i : α), f i = ⟦y⟧
have mpr : (∃ (i : α), f i = ⟦y⟧) → ⟦y⟧ ∈ range f
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ ⟦y⟧ ∈ range f
have h : y.Equiv
  ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Func
    ((equivShrink α : (a : α) → Shrink.{u, u_1} α) z))
Tactic: use equivShrink α z
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (↑(range f) : Set ZFSet.{u}) = Set.range f
have h : ∀ (x : ZFSet.{u}), x ∈ (↑(range f) : Set ZFSet.{u}) ↔ x ∈ Set.range f
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (↑(⋃ (i : α), f i) : Set ZFSet.{u}) = ⋃ (i : α), (↑(f i) : Set ZFSet.{u})
have h : ∀ (x : ZFSet.{u}),
  x ∈ (↑(⋃ (i : α), f i) : Set ZFSet.{u}) ↔ Membership.mem (γ := Set ZFSet.{u}) (⋃ (i : α), (↑(f i) : Set ZFSet.{u})) x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
have refine : ∀ (e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b), z ∈ (x ∪ y).powerset.powerset
Tactic: refine mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
x x' y y' : ZFSet.{u_1}
H : x.pair y = x'.pair y'
⊢ x = x' ∧ y = y'
have H₁ : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
Tactic: simp_rw [ZFSet.ext_iff, pair, mem_pair] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ y = y'
have obtain : ∀ (H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}), x = x ∧ y = y'
Tactic: obtain rfl : x = x' := And.left <| by simpa [or_and_left] using (H {x}).1 (Or.inl rfl)
Cleared hypotheses: x', H
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = x ∧ y = y'
have he : y = x → y = y'
Tactic: have he : y = x → y = y' := by
    rintro rfl
    simpa [eq_comm] using H {y, y'}
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
⊢ x = x ∧ y = y'
have hx : Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y} ↔
  Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
Tactic: have hx := H {x, y}
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx :
  Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y} ↔
    Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
⊢ x = x ∧ y = y'
have hx₁ : y = x ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
Tactic: simp_rw [pair_eq_singleton_iff, true_and, or_true, true_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
⊢ x = x ∧ y = y'
have refine : ∀ (hy : Eq (α := ZFSet.{u_1}) {x, y} {x, y'}), y = x ∨ y = y'
Tactic: refine ⟨rfl, hx.elim he fun hy ↦ Or.elim ?_ he id⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
⊢ y = f z
have let : ∀ w ∈ x, ∀ (we : w.pair (f w) = z.pair y), y = f z
Tactic: let ⟨w, _, we⟩ := mem_image.1 yx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
⊢ y = f z
have wz : w = z
Tactic: let ⟨wz, fy⟩ := pair_injective we
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (hypothesis)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
⊢ y = f z
have fy : f w = y
Tactic: let ⟨wz, fy⟩ := pair_injective we
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
⊢ y = f z
have rw : f w = f z
Tactic: rw [← fy, wz]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
rw : f w = f z
⊢ y = f z
have rw₁ : f z = f z
Tactic: rw [← fy, wz]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y
have rw : Hereditarily p x ↔ Hereditarily p x
Tactic: rw [← Hereditarily]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x → p ∅
have apply : ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅
Tactic: apply @ZFSet.inductionOn _ x
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
have inl : ∀ (IH : ∀ (y : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) ∅ y → Hereditarily p y → p ∅) (h : Hereditarily p ∅), p ∅
Tactic: rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)
Cleared hypotheses: y, IH, h
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Basic (goal)
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
inl :
  ∀ (IH : ∀ (y : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) ∅ y → Hereditarily p y → p ∅) (h : Hereditarily p ∅), p ∅
⊢ p ∅
have inr : ∀ (a : ZFSet.{u}) (ha : a ∈ (↑y : Set ZFSet.{u})), p ∅
Tactic: rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x : ZFSet.{u}
⊢ #↥x = lift.{u + 1, u} x.card
have rw : #↥x = lift.{u + 1, u} #(Shrink.{u, u + 1} ↥x)
Tactic: rw [card, lift_mk_shrink'']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x : ZFSet.{u}
rw : #↥x = lift.{u + 1, u} #(Shrink.{u, u + 1} ↥x)
⊢ #↥x = lift.{u + 1, u} x.card
have rw₁ : #↥x = #↥x
Tactic: rw [card, lift_mk_shrink'']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
⊢ card ∅ = 0
have rw : #↥∅ = lift.{u_1 + 1, u_1} 0
Tactic: rw [← lift_inj, ← cardinalMk_coe_sort]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x y : ZFSet.{u}
⊢ (insert x y).card ≤ y.card + 1
have rw : lift.{u + 1, u} (insert x y).card ≤ lift.{u + 1, u} (y.card + 1)
Tactic: rw [← lift_le.{u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x y : ZFSet.{u}
h : x ∉ y
⊢ (insert x y).card = y.card + 1
have rw : lift.{u + 1, u} (insert x y).card = lift.{u + 1, u} (y.card + 1)
Tactic: rw [← lift_inj.{u, u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x y : ZFSet.{u}
h : x ≠ y
⊢ card {x, y} = 2
have h₁ : 2 = card {y} + 1
Tactic: convert! card_insert (notMem_singleton.2 h)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x y : ZFSet.{u}
h : x ≠ y
⊢ 2 = card {y} + 1
have h₁ : 2 = HAdd.hAdd (α := Cardinal.{u}) 1 1
Tactic: rw [card_singleton, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x y : ZFSet.{u}
h : x ≠ y
h₁ : 2 = HAdd.hAdd (α := Cardinal.{u}) 1 1
⊢ 2 = card {y} + 1
have h₂ : Eq.{u + 2} (α := Cardinal.{u}) 2 2
Tactic: rw [card_singleton, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x y : ZFSet.{u}
⊢ (x ∪ y).card ≤ x.card + y.card
have rw : lift.{u + 1, u} (x ∪ y).card ≤ lift.{u + 1, u} (x.card + y.card)
Tactic: rw [← lift_le.{u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
x : ZFSet.{u}
⊢ x.powerset.card = HPow.hPow (α := Cardinal.{u}) 2 x.card
have rw : lift.{u + 1, u} x.powerset.card = lift.{u + 1, u} (HPow.hPow (α := Cardinal.{u}) 2 x.card)
Tactic: rw [← lift_inj.{u, u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{u, v} (range f).card ≤ lift.{v, u} #α
have rw : lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{v + 1, u} #α
Tactic: rw [← lift_le.{max u (v + 1)}, lift_lift.{v}, lift_umax.{u, v + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Cardinal (goal)
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{u, v} (⋃ (i : α), f i).card ≤ sum.{u, v} fun (i : α) ↦ (f i).card
have rw : lift.{v + 1, max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤ lift.{v + 1, max u v} (sum.{u, v} fun (i : α) ↦ (f i).card)
Tactic: rw [← lift_le.{max u (v + 1)}, lift_umax.{max u v, v + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
⊢ ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
have refine : ∀ (a x : ZFSet.{u}) (IH : ∀ y ∈ x, Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑y : Class.{u})),
  ∀ y ∈ (↑x : Class.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) y
Tactic: refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (hypothesis)
Goal:
⊢ ∀ (a : Class.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) a
have H : ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
Tactic: have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x := by
      refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
      rintro A ⟨z, rfl, hz⟩
      exact IH z hz
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
H : ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
⊢ ∀ (a : Class.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) a
have refine : ∀ (A y : Class.{u}), y ∈ A → Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) y
Tactic: refine fun A => ⟨A, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : ZFSet.{u}
h : (↑x : Class.{u}) = (↑y : Class.{u})
z : ZFSet.{u}
⊢ (↑x : Class.{u}) z ↔ (↑y : Class.{u}) z
have rw : (↑y : Class.{u}) z ↔ (↑y : Class.{u}) z
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
A : Class.{u}
x : ZFSet.{u}
h : A.ToSet (↑x : Class.{u})
y : ZFSet.{u}
yx : (↑y : Class.{u}) = (↑x : Class.{u})
py : A y
⊢ A x
have rwa : ∀ (py : A x), A x
Tactic: rwa [ofSet.inj yx] at py
Cleared hypotheses: py
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z
have mp : (⋃₀ x) y → ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : Class.{u_1}
y : ZFSet.{u_1}
mp : (⋃₀ x) y → ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z
⊢ (⋃₀ x) y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z
have mpr : (∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z) → (⋃₀ x) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : Class.{u}
⊢ y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
have mp : y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : Class.{u}
mp : y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z
⊢ y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
have mpr : (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : Class.{u}
y : ZFSet.{u}
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z
have refine : (∀ (z : ZFSet.{u}), x z → y ∈ z) → (⋂₀ x) y
Tactic: refine ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y z : Class.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
have obtain : ∀ (w : ZFSet.{u_1}) (hw : (⋂₀ x) w), (↑w : Class.{u_1}) ∈ z
Tactic: obtain ⟨w, rfl, hw⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : Class.{u}
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z
have refine : ∀ (H : ∀ z ∈ x, y ∈ z), y ∈ ⋂₀ x
Tactic: refine ⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋂₀ x
have simp_rw : ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
Tactic: simp_rw [mem_def, sInter_apply]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
have obtain : ∀ (z : ZFSet.{u}) (hz : z ∈ x), ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
Tactic: obtain ⟨z, hz⟩ := h
Cleared hypotheses: h