-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem subset_iff_eq_or_mem (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y ↔ x = y ∨ x ∈ y

Proof state:
case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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:
obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y.toSet \ x.toSet) (Set.diff_nonempty.2 hyx)

Result:
case neg.intro.intro
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
⊢ x = y ∨ x ∈ y

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ↔ x = y ∨ x ∈ y

Tactic:
constructor

Result:
case mp
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y → x = y ∨ x ∈ y

case mpr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x = y ∨ x ∈ y → x ⊆ y

Proof state:
x y : ZFSet.{u}
⊢ ∀ (a₁ b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) →
          a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂) →
      a₁.IsOrdinal → b₁.IsOrdinal → a₁ ⊆ b₁ → a₁ = b₁ ∨ a₁ ∈ b₁

Tactic:
intro x y IH hx hy hxy

Result:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
⊢ x = y ∨ x ∈ y

Proof state:
case neg.intro.intro
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
⊢ x = y ∨ x ∈ y

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

Result:
case neg.intro.intro.inl
x y✝ y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(m, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : m.IsOrdinal
hxy : m ⊆ y
hyx : ¬y ⊆ m
hm : m ∈ y.toSet \ m.toSet
hm' : ∀ x ∈ y.toSet \ m.toSet, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y

case neg.intro.intro.inr
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y

Proof state:
case neg.intro.intro
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
⊢ x = y ∨ x ∈ y

Tactic:
have hmy : m ∈ y := show m ∈ y.toSet from Set.mem_of_mem_diff hm

Result:
case neg.intro.intro
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
⊢ x = y ∨ x ∈ y

Proof state:
case mpr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x = y ∨ x ∈ y → x ⊆ y

Tactic:
rintro (rfl | h)

Result:
case mpr.inl
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x

case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y

Proof state:
case mp
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y → x = y ∨ x ∈ y

Tactic:
revert hx hy

Result:
case mp
x y : ZFSet.{u}
⊢ x.IsOrdinal → y.IsOrdinal → x ⊆ y → x = y ∨ x ∈ y

Proof state:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
hzx : z ∉ x
⊢ False

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

Result:
no goals

Proof state:
case neg.intro.intro.inr
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y

Tactic:
cases Set.not_mem_of_mem_diff hm H

Result:
no goals

Proof state:
case pos
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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)

Result:
no goals

Proof state:
case mp
x y : ZFSet.{u}
⊢ x.IsOrdinal → y.IsOrdinal → x ⊆ y → x = y ∨ x ∈ y

Tactic:
apply Sym2.GameAdd.induction mem_wf _ x y

Result:
x y : ZFSet.{u}
⊢ ∀ (a₁ b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) →
          a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂) →
      a₁.IsOrdinal → b₁.IsOrdinal → a₁ ⊆ b₁ → a₁ = b₁ ∨ a₁ ∈ b₁

Proof state:
case mpr.inl
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x

Tactic:
rfl

Result:
no goals

Proof state:
case neg.intro.intro.inl
x y✝ y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(m, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : m.IsOrdinal
hxy : m ⊆ y
hyx : ¬y ⊆ m
hm : m ∈ y.toSet \ m.toSet
hm' : ∀ x ∈ y.toSet \ m.toSet, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y

Tactic:
exact Or.inr hmy

Result:
no goals

Proof state:
case neg.intro.intro
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
⊢ x = y ∨ x ∈ y

Tactic:
have hmx : m ⊆ x := by
  intro z hzm
  by_contra hzx
  exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm

Result:
case neg.intro.intro
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → 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.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
⊢ x = y ∨ x ∈ y