awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
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:
hwx.mem_trans hyz hzw

Premises used: Class.ofSet, setOf, ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : (↑y : Class.{u}) z
⊢ z.IsOrdinal

Tactic:
exacts [hy.mem hz, hwx.mem_trans hyz hzw]

Premises used: ZFSet.IsOrdinal.mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
⊢ IsTransitive.{u_1} ∅

Tactic:
fun y hy => (notMem_empty y hy).elim

Premises used: ZFSet.notMem_empty, False.elim, ZFSet.IsTransitive
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
h : x.IsTransitive
⊢ y ∈ x → y ⊆ x

Tactic:
h y
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
z : ZFSet.{u}
⊢ z.IsTransitive ↔ ∀ {x y : ZFSet.{u}}, x ∈ y → y ∈ z → x ∈ z

Tactic:
⟨fun h _ _ hx hy => h.subset_of_mem hy hx, fun H _ hx _ hy => H hy hx⟩

Premises used: ZFSet.IsTransitive.subset_of_mem, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∩ y
w : ZFSet.{u}
hw : w ∈ z
rw : ∀ (hz : z ∈ x ∧ z ∈ y) (w : ZFSet.{u}) (hw : w ∈ z), w ∈ x ∧ w ∈ y
⊢ w ∈ x ∩ y

Tactic:
rw [mem_inter] at hz ⊢

Premises used: ZFSet.mem_inter
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∧ z ∈ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y

Tactic:
⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

Premises used: And.right, And.left, And.intro, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∧ z ∈ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y

Tactic:
exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
rcases : ∀ (w : ZFSet.{u}) (hw : w ∈ x) (hw' : y ∈ w), z ∈ ⋃₀ x
⊢ z ∈ ⋃₀ x

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩

Premises used: ZFSet.mem_sUnion, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
mem_sUnion_of_mem hz (h.mem_trans hw' hw)

Premises used: ZFSet.mem_sUnion_of_mem, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)

Premises used: ZFSet.mem_sUnion_of_mem, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
rcases : ∀ (w : ZFSet.{u}) (hw : w ∈ x) (hw' : y ∈ w), z ∈ ⋃₀ x
⊢ z ∈ ⋃₀ x

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩

Premises used: ZFSet.mem_sUnion, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw

Premises used: ZFSet.mem_sUnion_of_mem, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw

Premises used: ZFSet.mem_sUnion_of_mem, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
hf : ∀ (i : α), IsTransitive.{u} (f i)
⊢ ∀ y ∈ range fun (i : α) ↦ f i, y.IsTransitive

Tactic:
simpa
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
rw : IsTransitive.{u} (⋃₀ {x, y})
⊢ IsTransitive.{u} (x ∪ y)

Tactic:
rw [← sUnion_pair]

Premises used: ZFSet.sUnion_pair
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
H : ∀ (y_1 : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x, y} y_1 → y_1.IsTransitive
⊢ IsTransitive.{u} (⋃₀ {x, y})

Tactic:
apply IsTransitive.sUnion'

Premises used: ZFSet.IsTransitive.sUnion'
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y_1 : ZFSet.{u}
H : y_1 = x ∨ y_1 = y → y_1.IsTransitive
⊢ Membership.mem (γ := ZFSet.{u}) {x, y} y_1 → y_1.IsTransitive

Tactic:
rw [mem_pair]

Premises used: ZFSet.mem_pair
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
rw : ∀ (hy : y ⊆ x) (z : ZFSet.{u}) (hz : z ∈ y), z ⊆ x
⊢ z ∈ x.powerset

Tactic:
rw [mem_powerset] at hy ⊢

Premises used: ZFSet.mem_powerset
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ⊆ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ⊆ x

Tactic:
h.subset_of_mem (hy hz)

Premises used: ZFSet.IsTransitive.subset_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ⊆ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ⊆ x

Tactic:
exact h.subset_of_mem (hy hz)

Premises used: ZFSet.IsTransitive.subset_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
mp : x.IsTransitive → ⋃₀ x ⊆ x
mpr : ⋃₀ x ⊆ x → x.IsTransitive
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x

Tactic:
constructor
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
mp : ∀ (z : ZFSet.{u}) (hz : z ∈ x) (hz' : y ∈ z), y ∈ x
⊢ y ∈ x

Tactic:
obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy

Premises used: ZFSet.mem_sUnion, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x

Tactic:
h.mem_trans hz' hz

Premises used: ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x

Tactic:
exact h.mem_trans hz' hz

Premises used: ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
fun z hz ↦ h <| mem_sUnion_of_mem hz hy

Premises used: ZFSet.mem_sUnion_of_mem, ZFSet.Subset
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
exact fun z hz ↦ h <| mem_sUnion_of_mem hz hy

Premises used: ZFSet.mem_sUnion_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
⊢ x.IsTransitive ↔ x ⊆ x.powerset

Tactic:
⟨fun h _ hy => mem_powerset.2 <| h.subset_of_mem hy, fun H _ hy _ hz => mem_powerset.1 (H hy) hz⟩

Premises used: Iff.mpr, ZFSet.IsTransitive.subset_of_mem, ZFSet.mem_powerset, Iff.intro, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
h : x.IsOrdinal
⊢ y ∈ x → y ⊆ x

Tactic:
h.isTransitive.subset_of_mem

Premises used: ZFSet.IsTransitive.subset_of_mem, ZFSet.IsOrdinal.isTransitive
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y z : ZFSet.{u}
h : z.IsOrdinal
⊢ x ∈ y → y ∈ z → x ∈ z

Tactic:
h.isTransitive.mem_trans

Premises used: ZFSet.IsOrdinal.isTransitive, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
⊢ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)

Tactic:
⟨fun _ _ c hab hbc => h.mem_trans' hab hbc c.2⟩

Premises used: IsTrans.mk, ZFSet.IsOrdinal.mem_trans', Subtype.property
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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

Tactic:
⟨h₁, fun {y z w} hyz hzw hwx ↦ ?_⟩

Premises used: ZFSet.IsOrdinal.mk
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
refine : ∀ {y z w : ZFSet.{u}} (hyz : y ∈ z) (hzw : z ∈ w) (hwx : w ∈ x), y ∈ w
⊢ x.IsOrdinal

Tactic:
refine ⟨h₁, fun {y z w} hyz hzw hwx ↦ ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
⊢ z ∈ x

Tactic:
have hzx := h₁.mem_trans hzw hwx
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
hzx : z ∈ x
⊢ y ∈ w

Tactic:
h₂ ⟨y, h₁.mem_trans hyz hzx⟩ ⟨z, hzx⟩ ⟨w, hwx⟩ hyz hzw

Premises used: Set.Mem, Subrel, Subtype.mk, ZFSet.IsTransitive.mem_trans, Order.Preimage
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
hzx : z ∈ x
⊢ y ∈ w

Tactic:
exact h₂ ⟨y, h₁.mem_trans hyz hzx⟩ ⟨z, hzx⟩ ⟨w, hwx⟩ hyz hzw

Premises used: Subtype.mk, ZFSet.IsTransitive.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y ∈ x
⊢ y.IsOrdinal

Tactic:
have := hx.isTrans
  let f : _ ↪r Subrel (· ∈ ·) (· ∈ x) := Subrel.inclusionEmbedding (· ∈ ·) (hx.subset_of_mem hy)
  isOrdinal_iff_isTrans.2 ⟨fun _ hz _ ha ↦ hx.mem_trans' ha hz hy, f.isTrans⟩

Premises used: Iff.mpr, Membership.mem, RelEmbedding.isTrans, ZFSet.IsOrdinal.isTrans, ZFSet.isOrdinal_iff_isTrans, Subrel.inclusionEmbedding, ZFSet.IsOrdinal.subset_of_mem, And.intro, ZFSet.IsOrdinal.mem_trans'
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
mp : x ⊆ y → x = y ∨ x ∈ y
mpr : x = y ∨ x ∈ y → x ⊆ y
⊢ x ⊆ y ↔ x = y ∨ x ∈ y

Tactic:
constructor
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
mp : ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ⊆ y → x = y ∨ x ∈ y
⊢ x ⊆ y → x = y ∨ x ∈ y

Tactic:
revert hx hy
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
⊢ ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ⊆ y → x = y ∨ x ∈ y

Tactic:
Sym2.GameAdd.recursion mem_wf ?_ x y

Premises used: ZFSet.mem_wf, Sym2.GameAdd.recursion
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
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₁
⊢ ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ⊆ y → x = y ∨ x ∈ y

Tactic:
refine Sym2.GameAdd.recursion mem_wf ?_ x y
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
neg : ∀ (hyx : ¬y ⊆ x), x = y ∨ x ∈ y
⊢ x = y ∨ x ∈ y

Tactic:
by_cases hyx : y ⊆ x
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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

Tactic:
Or.inl (subset_antisymm hxy hyx)

Premises used: subset_antisymm, Or.inl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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

Tactic:
exact Or.inl (subset_antisymm hxy hyx)

Premises used: subset_antisymm, Or.inl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
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
⊢ x = y ∨ x ∈ y

Tactic:
obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y \ x) (Set.diff_nonempty.2 hyx)

Premises used: Iff.mpr, ZFSet.mem_wf, SDiff.sdiff, Set.diff_nonempty, SetLike.coe, WellFounded.has_min
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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 ∧ m ∉ x

Tactic:
simp only [Set.mem_diff, SetLike.mem_coe] at hm

Premises used: SetLike.mem_coe, Set.mem_diff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
hm : m ∈ y ∧ m ∉ x
⊢ m ∈ y

Tactic:
hm.1

Premises used: And.left
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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' : ∀ x_2 ∈ (↑y : Set ZFSet.{u}) \ (↑x : Set ZFSet.{u}), x_2 ∉ m
hm : m ∈ y ∧ m ∉ x
⊢ m ∈ y

Tactic:
exact hm.1

Premises used: And.left
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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

Tactic:
have hmy : m ∈ y := by simp only [Set.mem_diff, SetLike.mem_coe] at hm; exact hm.1
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
by_contra : ∀ (hzx : z ∉ x), False
⊢ z ∈ x

Tactic:
by_contra hzx
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
hzx : z ∉ x
⊢ False

Tactic:
hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm

Premises used: And.intro, ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
hzx : z ∉ x
⊢ False

Tactic:
exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm

Premises used: And.intro, ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
⊢ m ⊆ x

Tactic:
have hmx : m ⊆ x := by
        intro z hzm
        by_contra hzx
        exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
neg₁ : ∀ (H : m ∈ x), x = y ∨ x ∈ y
⊢ x = y ∨ x ∈ y

Tactic:
obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx

Premises used: Sym2.GameAdd.fst_snd, ZFSet.IsOrdinal.mem, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y_1 y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
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:
Or.inr hmy

Premises used: Or.inr
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y_1 y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
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:
exact Or.inr hmy

Premises used: Or.inr
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
H : m ∈ x
⊢ x = y ∨ x ∈ y

Tactic:
cases Set.notMem_of_mem_diff hm H

Premises used: Set.notMem_of_mem_diff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x

Tactic:
rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y

Tactic:
hy.subset_of_mem h

Premises used: ZFSet.IsOrdinal.subset_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y

Tactic:
exact hy.subset_of_mem h

Premises used: ZFSet.IsOrdinal.subset_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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
inr : ∀ (hx : x ∈ y), x ∈ z
⊢ x ∈ z

Tactic:
obtain rfl | hx := h.eq_or_mem_of_subset (hz.mem hy) hx

Premises used: ZFSet.IsOrdinal.eq_or_mem_of_subset, ZFSet.IsOrdinal.mem, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ x
hy : x ∈ z
⊢ x ∈ z

Tactic:
hy
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ x
hy : x ∈ z
⊢ x ∈ z

Tactic:
exact hy
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx_1 : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z

Tactic:
hz.mem_trans hx hy

Premises used: ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx_1 : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z

Tactic:
exact hz.mem_trans hx hy

Premises used: ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y ↔ y ⊆ x

Tactic:
⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩

Premises used: ZFSet.mem_irrefl, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
refine : x ∉ y → y ⊆ x
⊢ x ∉ y ↔ y ⊆ x

Tactic:
refine ⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
revert : ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ∉ y → y ⊆ x
⊢ x ∉ y → y ⊆ x

Tactic:
revert hx hy
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
⊢ ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ∉ y → y ⊆ x

Tactic:
Sym2.GameAdd.recursion mem_wf (fun x y IH hx hy hyx z hzy ↦ ?_) x y

Premises used: ZFSet.mem_wf, Sym2.GameAdd.recursion
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
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
⊢ ∀ (hx : x.IsOrdinal) (hy : y.IsOrdinal), x ∉ y → y ⊆ x

Tactic:
refine Sym2.GameAdd.recursion mem_wf (fun x y IH hx hy hyx z hzy ↦ ?_) x y
-- Module: Mathlib.SetTheory.ZFC.Ordinal
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₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
by_contra : ∀ (hzx : z ∉ x), False
⊢ z ∈ x

Tactic:
by_contra hzx