awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hzx : z ∉ x
⊢ False

Tactic:
hyx (mem_of_subset_of_mem hx hy (IH z x (Sym2.GameAdd.fst_snd hzy) (hy.mem hzy) hx hzx) hzy)

Premises used: Sym2.GameAdd.fst_snd, ZFSet.IsOrdinal.mem_of_subset_of_mem, ZFSet.IsOrdinal.mem
-- 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
hzx : z ∉ x
⊢ False

Tactic:
exact hyx (mem_of_subset_of_mem hx hy (IH z x (Sym2.GameAdd.fst_snd hzy) (hy.mem hzy) hx hzx) hzy)

Premises used: Sym2.GameAdd.fst_snd, ZFSet.IsOrdinal.mem_of_subset_of_mem, ZFSet.IsOrdinal.mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : y ∉ x ↔ x ⊆ y
rw₁ rw₂ : x ⊆ y ↔ x ⊆ y
⊢ ¬x ⊆ y ↔ y ∈ x

Tactic:
rw [not_iff_comm, notMem_iff_subset hy hx]

Premises used: ZFSet.IsOrdinal.notMem_iff_subset, not_iff_comm
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : y ⊆ x → y ⊆ x
⊢ x ∈ y ∨ y ⊆ x

Tactic:
rw [or_iff_not_imp_left, notMem_iff_subset hx hy]

Premises used: ZFSet.IsOrdinal.notMem_iff_subset, Classical.or_iff_not_imp_left
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ y ⊆ x → y ⊆ x

Tactic:
id

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

Tactic:
exact id

Premises used: id
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
inl : ∀ (h : x ∈ y), x ⊆ y ∨ y ⊆ x
inr : ∀ (h : y ⊆ x), x ⊆ y ∨ y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
obtain h | h := mem_or_subset hx hy

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

Tactic:
Or.inl (hy.subset_of_mem h)

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

Tactic:
exact Or.inl (hy.subset_of_mem h)

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

Tactic:
Or.inr h

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

Tactic:
exact Or.inr h

Premises used: Or.inr
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x ∈ y ∨ y ⊆ x
⊢ x ∈ y ∨ x = y ∨ y ∈ x

Tactic:
rw [eq_comm, ← subset_iff_eq_or_mem hy hx]

Premises used: eq_comm, ZFSet.IsOrdinal.subset_iff_eq_or_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x

Tactic:
mem_or_subset hx hy

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

Tactic:
exact mem_or_subset hx hy

Premises used: ZFSet.IsOrdinal.mem_or_subset
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
a : ZFSet.{u}
ha : a ∈ x
this :
  ∀ (b : ZFSet.{u}) (hb : b ∈ x),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb) ∨
      Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha = Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb ∨
        Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
          (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb)
          (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)
⊢ ∀ {b : ↥x},
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha) b ∨
      Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha = b ∨
        Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b
          (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)

Tactic:
⟨b, hb⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
a : ZFSet.{u}
ha : a ∈ x
b : ZFSet.{u}
hb : b ∈ x
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
      (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)
      (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb) ∨
    Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha = Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb ∨
      Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)

Tactic:
simpa using mem_trichotomous (h.mem ha) (h.mem hb)

Premises used: ZFSet.IsOrdinal.mem, ZFSet.IsOrdinal.mem_trichotomous
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
rw : x.IsTransitive ∧ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsOrdinal

Tactic:
rw [isOrdinal_iff_isTrans]

Premises used: ZFSet.isOrdinal_iff_isTrans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsTransitive ∧ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)

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

Premises used: IsTrans.mk, And.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
refine :
  ∀ (y z w : ↥x) (hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z)
    (hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
⊢ x.IsTransitive ∧ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)

Tactic:
refine ⟨h₁, ⟨@fun y z w hyz hzw ↦ ?_⟩⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
inl :
  ∀ (hyw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
inr :
  ∀ (hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z y),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y y
inr₁ :
  ∀ (hwy : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) w y),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w

Tactic:
obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w

Premises used: Membership.mem, Subrel, trichotomous_of, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
hyw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w

Tactic:
hyw
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
hyw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w

Tactic:
exact hyw
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z y
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y y

Tactic:
cases asymm hyz hzw

Premises used: asymm
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
hwy : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) w y
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w

Tactic:
cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy

Premises used: ZFSet.mem_wf, WellFounded.asymmetric₃
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
mpr :
  x.IsTransitive ∧
      IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) →
    x.IsOrdinal
⊢ x.IsOrdinal ↔
    x.IsTransitive ∧
      IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)

Tactic:
use fun h ↦ ⟨h.isTransitive, h.isWellOrder⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsOrdinal

Tactic:
isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩

Premises used: Iff.mpr, ZFSet.isOrdinal_iff_isTrans, And.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
mpr : IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsOrdinal

Tactic:
refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩

Premises used: Iff.mpr, ZFSet.isOrdinal_iff_isTrans, And.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank < y.rank ↔ x ∈ y

Tactic:
⟨fun h ↦ ?_, rank_lt_of_mem⟩

Premises used: Iff.intro, ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
refine : ∀ (h : x.rank < y.rank), x ∈ y
⊢ x.rank < y.rank ↔ x ∈ y

Tactic:
refine ⟨fun h ↦ ?_, rank_lt_of_mem⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x.rank < y.rank
rw : ¬y ⊆ x
⊢ x ∈ y

Tactic:
rw [← hy.not_subset_iff_mem hx]

Premises used: ZFSet.IsOrdinal.not_subset_iff_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x.rank < y.rank
⊢ ¬y ⊆ x

Tactic:
fun h' ↦ (rank_mono h').not_gt h

Premises used: ZFSet.rank_mono, LE.le.not_gt, Not
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x.rank < y.rank
⊢ ¬y ⊆ x

Tactic:
exact fun h' ↦ (rank_mono h').not_gt h

Premises used: ZFSet.rank_mono, LE.le.not_gt
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ↔ y ∉ x
rw₁ : x.rank ≤ y.rank ↔ ¬y.rank < x.rank
rw₂ rw₃ : x.rank ≤ y.rank ↔ x.rank ≤ y.rank
⊢ x.rank ≤ y.rank ↔ x ⊆ y

Tactic:
rw [← notMem_iff_subset hy hx, ← rank_lt_iff_mem hy hx, not_lt]

Premises used: ZFSet.IsOrdinal.notMem_iff_subset, not_lt, ZFSet.IsOrdinal.rank_lt_iff_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x = y
rw₁ : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
rw₂ : x ⊆ y ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
rw₃ rw₄ : x ⊆ y ∧ y ⊆ x ↔ x ⊆ y ∧ y ⊆ x
⊢ x.rank = y.rank ↔ x = y

Tactic:
rw [le_antisymm_iff, subset_antisymm_iff, rank_le_iff_subset hx hy, rank_le_iff_subset hy hx]

Premises used: ZFSet.IsOrdinal.rank_le_iff_subset, le_antisymm_iff, subset_antisymm_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
⊢ IsOrdinal.{u_1} ∅

Tactic:
⟨isTransitive_empty, fun _ _ H ↦ (notMem_empty _ H).elim⟩

Premises used: ZFSet.notMem_empty, False.elim, ZFSet.isTransitive_empty, ZFSet.IsOrdinal.mk
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
⊢ IsOrdinal.{u_1} (insert x x)

Tactic:
⟨fun y hy ↦ ?_, @fun y z w hyz hzw hw ↦ ?_⟩

Premises used: ZFSet.IsOrdinal.mk
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
refine_1 : ∀ (y : ZFSet.{u_1}) (hy : y ∈ insert x x), y ⊆ insert x x
refine_2 : ∀ (y z w : ZFSet.{u_1}) (hyz : y ∈ z) (hzw : z ∈ w) (hw : w ∈ insert x x), y ∈ w
⊢ IsOrdinal.{u_1} (insert x x)

Tactic:
refine ⟨fun y hy ↦ ?_, @fun y z w hyz hzw hw ↦ ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy : y ∈ insert x x
refine_1 : ∀ (h : y.IsOrdinal) (hy : y ∈ insert y y), y ⊆ insert y y
refine_1₁ : ∀ (hy : y ∈ x), y ⊆ insert x x
⊢ y ⊆ insert x x

Tactic:
obtain rfl | hy := mem_insert_iff.1 hy

Premises used: Iff.mp, ZFSet.mem_insert_iff, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy_1 : y ∈ insert x x
hy : y ∈ x
refine_1 : x ⊆ insert x x
⊢ y ⊆ insert x x

Tactic:
apply (h.subset_of_mem hy).trans

Premises used: HasSubset.Subset.trans, ZFSet.IsOrdinal.subset_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy_1 : y ∈ insert x x
hy : y ∈ x
refine_1 : x ⊆ insert x x
⊢ y ⊆ insert x x

Tactic:
on_goal 2 => apply (h.subset_of_mem hy).trans

Premises used: HasSubset.Subset.trans, ZFSet.IsOrdinal.subset_of_mem
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
y : ZFSet.{u_1}
h : y.IsOrdinal
hy : y ∈ insert y y
⊢ y ⊆ insert y y

Tactic:
simp_all [subset_def]

Premises used: ZFSet.subset_def
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy_1 : y ∈ insert x x
hy : y ∈ x
⊢ x ⊆ insert x x

Tactic:
simp_all [subset_def]

Premises used: ZFSet.subset_def
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw : w ∈ insert x x
refine_2 : ∀ (h : w.IsOrdinal) (hw : w ∈ insert w w), y ∈ w
refine_2₁ : ∀ (hw : w ∈ x), y ∈ w
⊢ y ∈ w

Tactic:
obtain rfl | hw := mem_insert_iff.1 hw

Premises used: Iff.mp, ZFSet.mem_insert_iff, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
h : w.IsOrdinal
hw : w ∈ insert w w
⊢ y ∈ w

Tactic:
h.mem_trans hyz hzw

Premises used: ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw_1 : w ∈ insert x x
hw : w ∈ x
⊢ y ∈ w

Tactic:
h.mem_trans' hyz hzw hw

Premises used: ZFSet.IsOrdinal.mem_trans'
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
h : w.IsOrdinal
hw : w ∈ insert w w
⊢ y ∈ w

Tactic:
exacts [h.mem_trans hyz hzw, h.mem_trans' hyz hzw hw]

Premises used: ZFSet.IsOrdinal.mem_trans
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u}
a : o.ToType
⊢ (↑a.toOrd : Ordinal.{u}) < o

Tactic:
a.toOrd.prop

Premises used: Ordinal.ToType.toOrd, Set.Mem, setOf, Subtype.prop, Set.Iio
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u}
a : o.ToType
⊢ (↑a.toOrd : Ordinal.{u}) < o

Tactic:
exact a.toOrd.prop

Premises used: Ordinal.ToType.toOrd, Subtype.prop
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u}
a : o.ToType
⊢ (↑a.toOrd : Ordinal.{u}) < o

Tactic:
decreasing_by exact a.toOrd.prop

Premises used: Ordinal.ToType.toOrd, Subtype.prop
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
rw : (PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Type = o.ToType
⊢ o.toPSet.Type = o.ToType

Tactic:
rw [toPSet]

Premises used: Ordinal.toPSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ (PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Type = o.ToType

Tactic:
rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
rw :
  (∃ (b : (PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Type),
      x.Equiv ((PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Func b)) ↔
    ∃ a < o, x.Equiv a.toPSet
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
rw [toPSet, PSet.mem_def]

Premises used: PSet.mem_def, Ordinal.toPSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∃ (b : (PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Type),
      x.Equiv ((PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Func b)) ↔
    ∃ a < o, x.Equiv a.toPSet

Tactic:
simpa using ((@ToType.mk o).exists_congr_left (p := fun y ↦ x.Equiv y.1.toPSet)).symm

Premises used: Equiv.exists_congr_left, Ordinal.ToType.mk, RelIso.toEquiv, Iff.symm
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
rw : ⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank = o
⊢ o.toPSet.rank = o

Tactic:
rw [toPSet, PSet.rank]

Premises used: PSet.rank, Ordinal.toPSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
rw : ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑a : Ordinal.{u_1})
| o

Tactic:
rw [← _root_.iSup_succ o]

Premises used: iSup_succ
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
conv_rhs :
  Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank)
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑a : Ordinal.{u_1}))
⊢ ⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank = o

Tactic:
conv_rhs => rw [← _root_.iSup_succ o]

Premises used: iSup_succ
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1})
    (⨆ (x : o.ToType),
      Order.succ
        (toPSet
            (↑((RelIso.toEquiv (r := fun (x1 x2 : o.ToType) ↦ x1 ≤ x2) (s := fun (x1 x2 : (↑(Iio o) : Type (u_1 + 1))) ↦
                      x1 ≤ x2) (OrderIso.symm ToType.mk) :
                    (a : o.ToType) → (↑(Iio o) : Type (u_1 + 1)))
                  x) :
              Ordinal.{u_1})).rank)
    (⨆ (y : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑y : Ordinal.{u_1}).toPSet.rank)

Tactic:
ToType.mk.symm.iSup_comp (g := fun x ↦ Order.succ x.1.toPSet.rank)

Premises used: Equiv.iSup_comp, OrderIso.symm, Ordinal.ToType.mk, RelIso.toEquiv
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
h : ∀ (x : (↑(Iio o) : Type (u_1 + 1))), (↑x : Ordinal.{u_1}) = (↑x : Ordinal.{u_1}).toPSet.rank
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank)
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑a : Ordinal.{u_1}))

Tactic:
convert! ToType.mk.symm.iSup_comp (g := fun x ↦ Order.succ x.1.toPSet.rank)

Premises used: Equiv.iSup_comp, OrderIso.symm, Ordinal.ToType.mk, RelIso.toEquiv
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
x : (↑(Iio o) : Type (u_1 + 1))
h h₁ : (↑x : Ordinal.{u_1}) = (↑x : Ordinal.{u_1})
⊢ (↑x : Ordinal.{u_1}) = (↑x : Ordinal.{u_1}).toPSet.rank

Tactic:
rw [rank_toPSet]
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
h :
  ∀ (y : Ordinal.{u_1}),
    (invImage (fun (x : Ordinal.{u_1}) ↦ x) wellFoundedRelation : WellFoundedRelation Ordinal.{u_1}).1 y o →
      y.toPSet.rank = y
x : (↑(Iio o) : Type (u_1 + 1))
⊢ (↑x : Ordinal.{u_1}) < o

Tactic:
x.2

Premises used: Set.Mem, setOf, Set.Iio, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
h :
  ∀ (y : Ordinal.{u_1}),
    (invImage (fun (x : Ordinal.{u_1}) ↦ x) wellFoundedRelation : WellFoundedRelation Ordinal.{u_1}).1 y o →
      y.toPSet.rank = y
x : (↑(Iio o) : Type (u_1 + 1))
⊢ (↑x : Ordinal.{u_1}) < o

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
h :
  ∀ (y : Ordinal.{u_1}),
    (invImage (fun (x : Ordinal.{u_1}) ↦ x) wellFoundedRelation : WellFoundedRelation Ordinal.{u_1}).1 y o →
      y.toPSet.rank = y
x : (↑(Iio o) : Type (u_1 + 1))
decreasing_by decreasing_by₁ : (↑x : Ordinal.{u_1}) < o
⊢ (↑x : Ordinal.{u_1}) < o

Tactic:
decreasing_by rename_i x; exact x.2
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ mk o.toPSet = o.toZFSet

Tactic:
rfl

Premises used: Ordinal.toZFSet, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
a : ∀ (a : PSet.{u_1}), ⟦a⟧ ∈ o.toZFSet ↔ ∃ a_1 < o, a_1.toZFSet = ⟦a⟧
⊢ x ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = x

Tactic:
induction x using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
a_1 : PSet.{u_1}
a : (∃ a < o, a_1.Equiv a.toPSet) ↔ ∃ a < o, a.toZFSet = mk a_1
⊢ ⟦a_1⟧ ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = ⟦a_1⟧

Tactic:
rw [toZFSet, mk_eq, ZFSet.mk_mem_iff, mem_toPSet_iff]

Premises used: ZFSet.mk_eq, Ordinal.mem_toPSet_iff, ZFSet.mk_mem_iff, Ordinal.toZFSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
a_1 : PSet.{u_1}
a : ∀ (x : Ordinal.{u_1}), a_1.Equiv x.toPSet ↔ x.toZFSet = mk a_1
⊢ (∃ a < o, a_1.Equiv a.toPSet) ↔ ∃ a < o, a.toZFSet = mk a_1

Tactic:
congr!
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
a_1 : PSet.{u_1}
x : Ordinal.{u_1}
a : a_1.Equiv x.toPSet ↔ mk x.toPSet = mk a_1
a₁ : a_1.Equiv x.toPSet ↔ x.toPSet.Equiv a_1
a₂ a₃ : x.toPSet.Equiv a_1 ↔ x.toPSet.Equiv a_1
⊢ a_1.Equiv x.toPSet ↔ x.toZFSet = mk a_1

Tactic:
rw [toZFSet, eq, PSet.Equiv.comm]

Premises used: PSet.Equiv.comm, ZFSet.eq, Ordinal.toZFSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.toZFSet.rank = o

Tactic:
rank_toPSet o

Premises used: ZFSet.rank, Ordinal.rank_toPSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
h : ∀ (x : ZFSet.{u_1}), x ∈ (↑o.toZFSet : Set ZFSet.{u_1}) ↔ x ∈ toZFSet '' Iio o
⊢ (↑o.toZFSet : Set ZFSet.{u_1}) = toZFSet '' Iio o

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ∈ (↑o.toZFSet : Set ZFSet.{u_1}) ↔ x ∈ toZFSet '' Iio o

Tactic:
simp [mem_toZFSet_iff]

Premises used: Ordinal.mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
h : a < b
rw : ∃ a_1 < b, a_1.toZFSet = a.toZFSet
⊢ a.toZFSet ∈ b.toZFSet

Tactic:
rw [mem_toZFSet_iff]

Premises used: Ordinal.mem_toZFSet_iff