awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x y : Class.{u}
H : ∀ z ∈ x, y ∈ z
z : ZFSet.{u}
hz : z ∈ x
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
have obtain : ∀ (y : ZFSet.{u}),
  (↑z : Class.{u}) y →
    ∀ (H : ∀ z ∈ x, (↑y : Class.{u}) ∈ z),
      ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = (↑y : Class.{u}) ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
Tactic: obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)
Cleared hypotheses: y, H
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right : (↑z : Class.{u}) y
H : ∀ z ∈ x, (↑y : Class.{u}) ∈ z
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = (↑y : Class.{u}) ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
have refine : ∀ (w : ZFSet.{u}) (hxw : x w), y ∈ w
Tactic: refine ⟨y, rfl, fun w hxw => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
⊢ ⋃₀ ∅ = ∅
have a : ∀ (z : ZFSet.{u}), (⋃₀ ∅) z ↔ ∅ z
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
A : Class.{u_1}
hA : A.powerset ⊆ A
⊢ ∀ (x : ZFSet.{u_1}), A x
have by_contra! : ∀ (hnA : ∃ (x : ZFSet.{u_1}), ¬A x), False
Tactic: by_contra! hnA
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
h_1 : A.iota y
x' : ZFSet.{u_1}
h : {x : ZFSet.{u_1} | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ (↑x' : Class.{u_1})
⊢ (↑x : Class.{u_1}) y
have rwa : (↑x' : Class.{u_1}) y
Tactic: rwa [← (H x').1 <| (h x').2 rfl]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ Class.ToSet.{u} (fun (x_1 : ZFSet.{u}) ↦ (↑(map f x) : Class.{u}) (x_1.pair z)) (↑y : Class.{u}) ↔ z = f y
have rw : (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y
Tactic: rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (hypothesis)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
⊢ z = f y
have wy : w = y
Tactic: let ⟨wy, fw⟩ := ZFSet.pair_injective pr
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (hypothesis)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
⊢ z = f y
have fw : f w = z
Tactic: let ⟨wy, fw⟩ := ZFSet.pair_injective pr
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
⊢ z = f y
have rw : f w = f y
Tactic: rw [← fw, wy]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
rw : f w = f y
⊢ z = f y
have rw₁ : f y = f y
Tactic: rw [← fw, wy]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
e : z = f y
⊢ ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
have subst : ∃ z ∈ x, z.pair (f z) = y.pair (f y)
Tactic: subst e
Cleared hypotheses: z, e
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (↑(map (fun (y : ZFSet.{u}) ↦ Classical.epsilon fun (z : ZFSet.{u}) ↦ z ∈ y) x) : Class.{u}) ′ (↑y : Class.{u}) ∈
    (↑y : Class.{u})
have rw : (Classical.epsilon fun (z : ZFSet.{u}) ↦ z ∈ y) ∈ y
Tactic: rw [@map_fval _ (Classical.allZFSetDefinable _) x y yx, Class.coe_mem, Class.coe_apply]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ (↑(mk
          (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
            Quotient.out (s := PSet.setoid)
              (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                      (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                    x) :
                ZFSet.{u}))) :
      Set ZFSet.{u}) =
    s
have h : ∀ (x : ZFSet.{u}),
  x ∈
      (↑(mk
            (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
              Quotient.out (s := PSet.setoid)
                (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                        (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                      x) :
                  ZFSet.{u}))) :
        Set ZFSet.{u}) ↔
    x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
⊢ x ∈
      (↑(mk
            (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
              Quotient.out (s := PSet.setoid)
                (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                        (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                      x) :
                  ZFSet.{u}))) :
        Set ZFSet.{u}) ↔
    x ∈ s
have h : (Quotient.out x ∈
    PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
      Quotient.out (s := PSet.setoid)
        (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
              x) :
          ZFSet.{u})) ↔
  x ∈ s
Tactic: rw [SetLike.mem_coe, ← mk_out x, mk_mem_iff, mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
⊢ (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) ↔
    x ∈ s
have h : (Quotient.out x ∈
    PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
      Quotient.out (s := PSet.setoid)
        (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
              x) :
          ZFSet.{u})) →
  x ∈ s
Tactic: refine ⟨?_, fun xs ↦ ⟨equivShrink s (Subtype.mk x xs), ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
h :
  (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) →
    x ∈ s
⊢ (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) ↔
    x ∈ s
have h₁ : ∀ (xs : x ∈ s),
  PSet.Equiv.{u, u} (Quotient.out x)
    ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
          Quotient.out (s := PSet.setoid)
            (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                    (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                  x) :
              ZFSet.{u})).Func
      ((equivShrink (↑s : Type (u + 1)) : (a : (↑s : Type (u + 1))) → Shrink.{u, u + 1} (↑s : Type (u + 1)))
        (Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ s) x xs)))
Tactic: refine ⟨?_, fun xs ↦ ⟨equivShrink s (Subtype.mk x xs), ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (hypothesis)
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
b :
  (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
      Quotient.out (s := PSet.setoid)
        (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
              x) :
          ZFSet.{u})).Type
h2 :
  PSet.Equiv.{u, u} (Quotient.out x)
    ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
          Quotient.out (s := PSet.setoid)
            (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                    (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                  x) :
              ZFSet.{u})).Func
      b)
⊢ x ∈ s
have h2₁ : x =
  mk
    ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
          Quotient.out (s := PSet.setoid)
            (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                    (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                  x) :
              ZFSet.{u})).Func
      b)
Tactic: rw [← ZFSet.eq, ZFSet.mk_out] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
this : x.IsOrdinal
⊢ False
have apply : (↑x : Class.{u}) ∈ (↑x : Class.{u})
Tactic: apply Class.mem_irrefl x
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
this : x.IsOrdinal
⊢ (↑x : Class.{u}) ∈ (↑x : Class.{u})
have rwa : (↑x : Class.{u}) x
Tactic: rwa [Class.coe_mem, hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
⊢ False
have suffices : x.IsOrdinal
Tactic: suffices IsOrdinal x by
    apply Class.mem_irrefl x
    rwa [Class.coe_mem, hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
⊢ x.IsOrdinal
have refine_1 : ∀ (y : ZFSet.{u}) (hy : y ∈ x) (z : ZFSet.{u}) (hz : z ∈ y), z ∈ x
Tactic: refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
refine_1 : ∀ (y : ZFSet.{u}) (hy : y ∈ x) (z : ZFSet.{u}) (hz : z ∈ y), z ∈ x
⊢ x.IsOrdinal
have refine_2 : ∀ {y z w : ZFSet.{u}} (hyz : y ∈ z) (hzw : z ∈ w) (hwx : w ∈ x), y ∈ w
Tactic: refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
y : ZFSet.{u}
hy : y ∈ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x
have refine_1 : ∀ (hx : IsOrdinal = IsOrdinal) (y : ZFSet.{u}) (hy : y.IsOrdinal) (z : ZFSet.{u}) (hz : (↑y : Class.{u}) z), z.IsOrdinal
Tactic: rw [← Class.coe_apply, hx] at *
Cleared hypotheses: hx, y, hy, z, hz
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Class (goal)
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
⊢ y ∈ w
have refine_2 : ∀ (hx : IsOrdinal = IsOrdinal) {y z w : ZFSet.{u}} (hyz : (↑z : Class.{u}) y) (hzw : (↑w : Class.{u}) z)
  (hwx : w.IsOrdinal), (↑w : Class.{u}) y
Tactic: rw [← Class.coe_apply, hx] at *
Cleared hypotheses: hx, y, z, w, hyz, hzw, hwx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∩ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∩ y
have rw : ∀ (hz : z ∈ x ∧ z ∈ y) (w : ZFSet.{u}) (hw : w ∈ z), w ∈ x ∧ w ∈ y
Tactic: rw [mem_inter] at hz ⊢
Cleared hypotheses: hz, w, hw
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x
have rcases : ∀ (w : ZFSet.{u}) (hw : w ∈ x) (hw' : y ∈ w), z ∈ ⋃₀ x
Tactic: rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x
have rcases : ∀ (w : ZFSet.{u}) (hw : w ∈ x) (hw' : y ∈ w), z ∈ ⋃₀ x
Tactic: rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ IsTransitive.{u} (x ∪ y)
have rw : IsTransitive.{u} (⋃₀ {x, y})
Tactic: rw [← sUnion_pair]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ IsTransitive.{u} (⋃₀ {x, y})
have H : ∀ (y_1 : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x, y} y_1 → y_1.IsTransitive
Tactic: apply IsTransitive.sUnion'
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y_1 : ZFSet.{u}
⊢ Membership.mem (γ := ZFSet.{u}) {x, y} y_1 → y_1.IsTransitive
have H : y_1 = x ∨ y_1 = y → y_1.IsTransitive
Tactic: rw [mem_pair]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x.powerset
have rw : ∀ (hy : y ⊆ x) (z : ZFSet.{u}) (hz : z ∈ y), z ⊆ x
Tactic: rw [mem_powerset] at hy ⊢
Cleared hypotheses: hy, z, hz
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x
have mp : x.IsTransitive → ⋃₀ x ⊆ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
mp : x.IsTransitive → ⋃₀ x ⊆ x
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x
have mpr : ⋃₀ x ⊆ x → x.IsTransitive
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x
have mp : ∀ (z : ZFSet.{u}) (hz : z ∈ x) (hz' : y ∈ z), y ∈ x
Tactic: obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : ↥x),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a b →
      Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b c →
        Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a c
⊢ x.IsOrdinal
have refine : ∀ {y z w : ZFSet.{u}} (hyz : y ∈ z) (hzw : z ∈ w) (hwx : w ∈ x), y ∈ w
Tactic: refine ⟨h₁, fun {y z w} hyz hzw hwx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (hypothesis)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : ↥x),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a b →
      Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b c →
        Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
⊢ y ∈ w
have hzx : z ∈ x
Tactic: have hzx := h₁.mem_trans hzw hwx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ↔ x = y ∨ x ∈ y
have mp : x ⊆ y → x = y ∨ x ∈ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
mp : x ⊆ y → x = y ∨ x ∈ y
⊢ x ⊆ y ↔ x = y ∨ x ∈ y
have mpr : x = y ∨ x ∈ y → x ⊆ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y → x = y ∨ x ∈ y
have mp : ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ⊆ y → x = y ∨ x ∈ y
Tactic: revert hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
⊢ ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ⊆ y → x = y ∨ x ∈ y
have mp : ∀ (a₁ b₁ : ZFSet.{u}),
  (∀ (a₂ b₂ : ZFSet.{u}),
      Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) →
        ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂) →
    ∀ (hx : a₁.IsOrdinal) (hy : b₁.IsOrdinal), a₁ ⊆ b₁ → a₁ = b₁ ∨ a₁ ∈ b₁
Tactic: refine Sym2.GameAdd.recursion mem_wf ?_ x y
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
⊢ x = y ∨ x ∈ y
have pos : ∀ (hyx : y ⊆ x), x = y ∨ x ∈ y
Tactic: by_cases hyx : y ⊆ x
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
pos : ∀ (hyx : y ⊆ x), x = y ∨ x ∈ y
⊢ x = y ∨ x ∈ y
have neg : ∀ (hyx : ¬y ⊆ x), x = y ∨ x ∈ y
Tactic: by_cases hyx : y ⊆ x
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
⊢ x = y ∨ x ∈ y
have neg : ∀ (m : ZFSet.{u}) (hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}))
  (hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m), x = y ∨ x ∈ y
Tactic: obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y \ x) (Set.diff_nonempty.2 hyx)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (hypothesis)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u})
hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
⊢ m ∈ y
have hm₁ : m ∈ y ∧ m ∉ x
Tactic: simp only [Set.mem_diff, SetLike.mem_coe] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (hypothesis)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u})
hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
⊢ x = y ∨ x ∈ y
have hmy : m ∈ y
Tactic: have hmy : m ∈ y := by simp only [Set.mem_diff, SetLike.mem_coe] at hm; exact hm.1
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u})
hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
⊢ z ∈ x
have by_contra : ∀ (hzx : z ∉ x), False
Tactic: by_contra hzx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (hypothesis)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u})
hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
hmy : m ∈ y
⊢ x = y ∨ x ∈ y
have hmx : m ⊆ x
Tactic: have hmx : m ⊆ x := by
        intro z hzm
        by_contra hzx
        exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u})
hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
⊢ x = y ∨ x ∈ y
have neg : ∀
  (IH :
    ∀ (a₂ b₂ : ZFSet.{u}),
      Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(m, y) →
        ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂)
  (hx : m.IsOrdinal) (hxy : m ⊆ y) (hyx : ¬y ⊆ m) (hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑m : Set ZFSet.{u}))
  (hm' : ∀ x ∈ (↑y : Set ZFSet.{u}) \ (↑m : Set ZFSet.{u}), x ∉ m) (hmx : m ⊆ m), m = y ∨ m ∈ y
Tactic: obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
Cleared hypotheses: x, IH, hx, hxy, hyx, hm, hm', hmx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u})
hm' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
neg :
  ∀
    (IH :
      ∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(m, y) →
          ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂)
    (hx : m.IsOrdinal) (hxy : m ⊆ y) (hyx : ¬y ⊆ m) (hm : m ∈ (↑y : Set ZFSet.{u}) \ (↑m : Set ZFSet.{u}))
    (hm' : ∀ x ∈ (↑y : Set ZFSet.{u}) \ (↑m : Set ZFSet.{u}), x ∉ m) (hmx : m ⊆ m), m = y ∨ m ∈ y
⊢ x = y ∨ x ∈ y
have neg₁ : ∀ (H : m ∈ x), x = y ∨ x ∈ y
Tactic: obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ y
hy : y ∈ z
⊢ x ∈ z
have inl : ∀ (hx : x ⊆ x) (hy : x ∈ z), x ∈ z
Tactic: obtain rfl | hx := h.eq_or_mem_of_subset (hz.mem hy) hx
Cleared hypotheses: y, hx, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ y
hy : y ∈ z
inl : ∀ (hx : x ⊆ x) (hy : x ∈ z), x ∈ z
⊢ x ∈ z
have inr : ∀ (hx : x ∈ y), x ∈ z
Tactic: obtain rfl | hx := h.eq_or_mem_of_subset (hz.mem hy) hx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y ↔ y ⊆ x
have refine : x ∉ y → y ⊆ x
Tactic: refine ⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y → y ⊆ x
have revert : ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ∉ y → y ⊆ x
Tactic: revert hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
⊢ ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ∉ y → y ⊆ x
have refine : ∀ (x y : ZFSet.{u})
  (IH :
    ∀ (a₂ b₂ : ZFSet.{u}),
      Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
        ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ∉ b₂ → b₂ ⊆ a₂)
  (hx : x.IsOrdinal) (hy : y.IsOrdinal) (hyx : x ∉ y) (z : ZFSet.{u}) (hzy : z ∈ y), z ∈ x
Tactic: refine Sym2.GameAdd.recursion mem_wf (fun x y IH hx hy hyx z hzy ↦ ?_) x y