mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.gt
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (↑n₁).sub ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
·

Goal state after:
case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.gt
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (↑n₁).sub ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ max x.rank y.rank

pp: case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank

Tactic:
·

Goal state after:
case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ max x.rank y.rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank

Tactic:
·

Goal state after:
case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_

pp: case mpr
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o

Tactic:
·

Goal state after:
case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case mpr
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o

Tactic:
·

Goal state after:
case mpr
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mp
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z

pp: case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
·

Goal state after:
case mp
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
·

Goal state after:
case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z

pp: case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
·

Goal state after:
case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
·

Goal state after:
case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ i, succ (f i).rank

pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ i, succ (f i).rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (⋃ (i : α), f i).rank ≤ ⨆ i, (f i).rank

pp: case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ⨆ i, (f i).rank ≤ (⋃ (i : α), f i).rank

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (⋃ (i : α), f i).rank ≤ ⨆ i, (f i).rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case refine_1
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) → x ∈ s

pp: case refine_2
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
xs : x ∈ s
⊢ (Quotient.out x).Equiv
    ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)).Func ((equivShrink ↑s) ⟨x, xs⟩))

Tactic:
·

Goal state after:
case refine_1
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) → x ∈ s
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : Ordering.eq.Compares e₁ e₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ⨆ i, (f i).rank ≤ (⋃ (i : α), f i).rank

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ⨆ i, (f i).rank ≤ (⋃ (i : α), f i).rank
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x

pp: case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
·

Goal state after:
case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case refine_2
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
xs : x ∈ s
⊢ (Quotient.out x).Equiv
    ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)).Func ((equivShrink ↑s) ⟨x, xs⟩))

Tactic:
·

Goal state after:
case refine_2
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
xs : x ∈ s
⊢ (Quotient.out x).Equiv
    ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)).Func ((equivShrink ↑s) ⟨x, xs⟩))
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
Ordinal.sub_eq_zero_iff_le.2

Goal state after:
case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    0

case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
·

Goal state after:
case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x
Module: Mathlib.SetTheory.ZFC.Ordinal

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

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

Tactic:
·

Goal state after:
case mp
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y → x = y ∨ x ∈ y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: 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

pp: 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:
·

Goal state after:
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
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: 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:
·

Goal state after:
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
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    0

pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    0
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case neg.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 \ ↑m
hm' : ∀ x ∈ ↑y \ ↑m, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y

pp: case neg.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 \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y

Tactic:
·

Goal state after:
case neg.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 \ ↑m
hm' : ∀ x ∈ ↑y \ ↑m, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : Ordering.eq.Compares e₁ e₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : Ordering.eq.Compares e₁ e₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

pp: x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
·

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case neg.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 \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y

Tactic:
·

Goal state after:
case neg.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 \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
·

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
·

Goal state after:
case mpr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x = y ∨ x ∈ y → x ⊆ y
Module: Mathlib.SetTheory.ZFC.Ordinal

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

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

Tactic:
·

Goal state after:
case mpr.inl
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
·

Goal state after:
case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case inl
x z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ x
hy : x ∈ z
⊢ x ∈ z

pp: case inr
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx✝ : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z

Tactic:
·

Goal state after:
case inl
x z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ x
hy : x ∈ z
⊢ x ∈ z
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case inr
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx✝ : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z

Tactic:
·

Goal state after:
case inr
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx✝ : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case inl
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y ∨ y ⊆ x

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

Tactic:
·

Goal state after:
case inl
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y ∨ y ⊆ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
·

Goal state after:
case inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ n • b + -b = (n + -1) • b

Tactic:
← neg_one_zsmul b,

Goal state after:
G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ n • b + -1 • b = (n + -1) • b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.zero
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case eq.zero
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ -b + n • b = (-1 + n) • b

Tactic:
← neg_one_zsmul b,

Goal state after:
G : Type u_1
inst✝ : AddGroup G
b : G
n : ℤ
⊢ -1 • b + n • b = (-1 + n) • b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
·

Goal state after:
case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr