mathlib-initiative/mathlib-tactics huggingface dataset:
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

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.Class

Goal state before:
pp: x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ x.IsOrdinal

Tactic:
]

Goal state after:
x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ x.IsOrdinal
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
IsWellFounded.rank_eq

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

Goal state before:
pp: case refine_1
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : ↑y z
⊢ z.IsOrdinal

Tactic:
]

Goal state after:
case refine_1
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : ↑y z
⊢ z.IsOrdinal
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
]

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

Goal state before:
pp: case refine_2
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : ↑z✝ y✝
hzw : ↑w✝ z✝
hwx : w✝.IsOrdinal
⊢ ↑w✝ y✝

Tactic:
]

Goal state after:
case refine_2
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : ↑z✝ y✝
hzw : ↑w✝ z✝
hwx : w✝.IsOrdinal
⊢ ↑w✝ 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 : Ordinal.{u + 1}
⊢ (∃ a' < x.rank, lift.{u + 1, u} a' = h) → h < ⨆ i, succ (lift.{u + 1, u} (↑i).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}
⊢ (∃ a' < x.rank, lift.{u + 1, u} a' = h) → h < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ↔ x ⊆ y

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ y ⊆ x → y ⊆ x

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (a : ↑(Set.Iio o)), (V_ ↑a).powerset ↔ ∃ a < o, x ⊆ V_ a

Tactic:
]

Goal state after:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (a : ↑(Set.Iio o)), (V_ ↑a).powerset ↔ ∃ a < o, x ⊆ V_ a
Module: Mathlib.Tactic.AddGroup

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : AddGroup G
b : G
h : -b = -1 • b
⊢ (-1 + -1) • b = -2 • b
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (⋃ (a : ↑(Set.Iio o)), (V_ ↑a).powerset).IsTransitive

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ (⋃ (a : ↑(Set.Iio o)), (V_ ↑a).powerset).IsTransitive
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
⊢ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)

Tactic:
]

Goal state after:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
⊢ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ ⋃ (a : ↑(Set.Iio b)), (V_ ↑a).powerset

Tactic:
]

Goal state after:
a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ ⋃ (a : ↑(Set.Iio b)), (V_ ↑a).powerset
Module: Mathlib.Tactic.AddGroup

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

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.AddGroup

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

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ x.rank ≤ o

Tactic:
rw [rank_le_iff]

Goal state after:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
a b : G
⊢ a + -2 • b = a + -2 • b

Tactic:
]

Goal state after:
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₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * ↑(n✝ + 1) + a₁.repr - 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₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * ↑(n✝ + 1) + a₁.repr - a₂.repr
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∃ a < o, y ⊆ V_ a

Tactic:
]

Goal state after:
case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∃ a < o, y ⊆ V_ a
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x.rank < y.rank
⊢ ¬y ⊆ x

Tactic:
]

Goal state after:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x.rank < y.rank
⊢ ¬y ⊆ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank ≤ y.rank ↔ x.rank ≤ y.rank

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
⊢ V_ o ⊆ V_ o

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y ∈ V_ o
⊢ x ∈ V_ o

Tactic:
mem_vonNeumann

Goal state after:
o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y.rank < o
⊢ x.rank < o
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∧ y ⊆ x ↔ x ⊆ y ∧ y ⊆ x

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y.rank < o
⊢ x.rank < o

Tactic:
]

Goal state after:
o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y.rank < o
⊢ x.rank < o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr ≤ e₁.repr

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z.rank ≤ o ↔ z.rank ≤ o

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Type = o.ToType

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∃ b, x.Equiv ((PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Func b)) ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∃ b, x.Equiv ((PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Func b)) ↔ ∃ a < o, x.Equiv a.toPSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.a
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)

Tactic:
]

Goal state after:
case neg.a
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ a, Order.succ (↑a.toOrd).toPSet.rank = o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ a, Order.succ (↑a.toOrd).toPSet.rank = o
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u + 1, u} (⋃ (i : ↑(Set.Iio o)), V_ ↑i).card ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)

Tactic:
]

Goal state after:
case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u + 1, u} (⋃ (i : ↑(Set.Iio o)), V_ ↑i).card ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.a
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ e₁.repr + b₂ ≤ e₁.repr + b₂

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case e'_3
o : Ordinal.{u_1}
x✝ : ↑(Iio o)
⊢ ↑x✝ = ↑x✝

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ Ordinal.omega0 ≤ o

Tactic:
]

Goal state after:
case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ Ordinal.omega0 ≤ o
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ (∃ a < o, a✝.Equiv a.toPSet) ↔ ∃ a < o, a.toZFSet = mk a✝

Tactic:
]

Goal state after:
case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ (∃ a < o, a✝.Equiv a.toPSet) ↔ ∃ a < o, a.toZFSet = mk a✝
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
x✝ : Ordinal.{u_1}
⊢ x✝.toPSet.Equiv a✝ ↔ x✝.toPSet.Equiv a✝

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ o.card ≤ ⨆ i, (V_ ↑i).card

Tactic:
]

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ o.card ≤ ⨆ i, (V_ ↑i).card
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ ∃ a_1 < b, a_1.toZFSet = a.toZFSet

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ a_1 < b, a_1.toZFSet = a.toZFSet
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ (V_ ((⨆ i, (V_ ↑i).card).ord + 1)).card ≤ ⨆ i, (V_ ↑i).card

Tactic:
]

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ (V_ ((⨆ i, (V_ ↑i).card).ord + 1)).card ≤ ⨆ i, (V_ ↑i).card
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊆ x✝.toZFSet ∧ ¬x✝.toZFSet ⊆ x✝¹.toZFSet

Tactic:
]

Goal state after:
x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊆ x✝.toZFSet ∧ ¬x✝.toZFSet ⊆ x✝¹.toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : e₂ = 0
x : ℕ
xe : ↑n₂ = x.succ
⊢ ω ^ e₁.repr * (↑↑n₁ * (↑x + 1)) + a₁.repr = ω ^ e₁.repr * (↑↑n₁ * (↑x + 1)) + a₁.repr

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_1
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x.rank.toZFSet ∈ Set.range toZFSet

Tactic:
]

Goal state after:
case refine_1
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x.rank.toZFSet ∈ Set.range toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * a₂.repr =
    (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ω ^ e₂.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * a₂.repr

Tactic:
]

Goal state after:
case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * a₂.repr =
    (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ω ^ e₂.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * a₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ^ e₁.repr * ω ^ e₂.repr = ω ^ e₁.repr * ω ^ e₂.repr

pp: case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ∣ ω ^ e₂.repr

Tactic:
]

Goal state after:
case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ∣ ω ^ e₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ¬e.repr = repr 0
⊢ ω ^ e.repr = ω ^ e.repr

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.refine_1
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a.repr < ω ^ e.repr

Tactic:
]

Goal state after:
case neg.refine_1
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a.repr < ω ^ e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.refine_2
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ω ^ 1 * ω ^ (e.repr - 1) * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'

Tactic:
]

Goal state after:
case neg.refine_2
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ω ^ 1 * ω ^ (e.repr - 1) * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s t : R
h : r + s = t
⊢ (algebraMap R A) t = (algebraMap R A) t

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
h : r + s = 0
⊢ IsNat 0 0

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
h : r + s = 0
⊢ IsNat 0 0
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
r t : R
h : -r = t
⊢ (algebraMap R A) t = (algebraMap R A) t

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x : ONote
inst✝¹ : x.NF
o : ONote
inst✝ : o.NF
⊢ (x.oadd 1 0 * o).NF

Tactic:
]

Goal state after:
x : ONote
inst✝¹ : x.NF
o : ONote
inst✝ : o.NF
⊢ (x.oadd 1 0 * o).NF
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) s = (algebraMap R A) s

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Semifield A
inst✝ : Algebra R A
r s : R
h : r⁻¹ = s
⊢ (algebraMap R A) s = (algebraMap R A) s

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
]

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Tactic:
]

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
]

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
]

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
]

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)