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

Tactic:
by

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
⊢ z = f y

Tactic:
by

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
e : z = f y
⊢ ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z

Tactic:
by

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ Class.ToSet (fun x_1 ↦ ↑(map f x) (x_1.pair z)) ↑y ↔ z = f y

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
n : ¬∃ y_1, y_1 ∈ y
⊢ ∅ ∈ x

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑x.choice ′ ↑y ∈ ↑y

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∩ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∩ y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
hf : ∀ (i : α), (f i).IsTransitive
⊢ ∀ y ∈ range fun i ↦ f i, y.IsTransitive

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ (x ∪ y).IsTransitive

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x.powerset

Tactic:
mem_powerset

Goal state after:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ⊆ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ⊆ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x.powerset

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x.powerset

Tactic:
by
  rw [mem_powerset] at hy ⊢
  exact h.subset_of_mem (hy hz)

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
⊢ Function.Injective fun x ↦ ⟨↑x, ⋯⟩

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ m ∈ y

Tactic:
by

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

Goal state before:
pp: ⊢ IsOrdinal ∉ Class.univ

Tactic:
by

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

Goal state before:
pp: 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
⊢ m ⊆ x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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:
by

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:
by

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:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
h : x.IsOrdinal
⊢ ∀ {a b : ↥x},
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b ∨ a = b ∨ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.AddGroup

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

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (V_ o).IsTransitive

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.AddGroup

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

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ V_ b

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u}
h : a ≤ b
⊢ a = b → V_ a ⊆ V_ b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.AddGroup

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

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.AddGroup

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

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x.IsTransitive ∧ IsWellOrder (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x ⊆ V_ x.rank

Tactic:
by

Goal state after:
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 ∈ y

Tactic:
by

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x.rank < o → ∃ a < o, x.rank ≤ a

Tactic:
by

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

Goal state before:
pp: o : ONote
⊢ 0 * o = 0

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ x.rank < o

Tactic:
by

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

Goal state before:
pp: o : ONote
⊢ o * 0 = 0

Tactic:
by

Goal state after:
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 ⊆ y

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x ∈ V_ (succ x.rank)

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (V_ o).rank ≤ o

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u}
⊢ V_ a ∈ V_ b ↔ a < b

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u}
⊢ V_ a ⊆ V_ b ↔ a ≤ b

Tactic:
by

Goal state after:
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 = y

Tactic:
by

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:
by

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

Goal state before:
pp: ⊢ ∀ (x y : Ordinal.{u_1}), x ≤ y ↔ V_ x ⊆ V_ y

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (y : ZFSet.{u_1}), y ∉ V_ 0

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
h : IsSuccPrelimit o
z : ZFSet.{u}
⊢ z ∈ V_ o ↔ z ∈ ⋃ (a : ↑(Set.Iio o)), V_ ↑a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card ≤ (V_ o).card

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u_1}
h : x.IsOrdinal
⊢ (insert x x).IsOrdinal

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.Type = o.ToType

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.rank = o

Tactic:
by

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

Goal state before:
pp: 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₂
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
by

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

Goal state before:
pp: o : ONote
x✝ : NF 0
h₂ : o.NF
⊢ (0 * o).NF

Tactic:
by

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

Goal state before:
pp: o : ONote
x✝ : NF 0
h₂ : o.NF
⊢ (0 * o).repr = repr 0 * o.repr

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = x

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ↑o.toZFSet = toZFSet '' Iio o

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ a.toZFSet ∈ b.toZFSet

Tactic:
by

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

Goal state before:
pp: ⊢ Monotone toZFSet

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a.toZFSet ∈ b.toZFSet ↔ a < b

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a.toZFSet ⊆ b.toZFSet ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: 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
⊢ a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ toZFSet 0 = ∅

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (o + 1).toZFSet = insert o.toZFSet o.toZFSet

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toZFSet.card = o.card

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (V_ o).card = preBeth o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toZFSet.IsOrdinal

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x ∈ Set.range toZFSet

Tactic:
by

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

Goal state before:
pp: x✝¹ y z w : ZFSet.{u}
x✝ : { x // x.IsOrdinal }
x : ZFSet.{?u.18}
hx : x.IsOrdinal
⊢ (fun o ↦ ⟨o.toZFSet, ⋯⟩) ((fun x ↦ (↑x).rank) ⟨x, hx⟩) = ⟨x, hx⟩

Tactic:
by

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

Goal state before:
pp: x y z w : ZFSet.{u}
a b : Ordinal.{?u.18}
⊢ { toFun := fun o ↦ ⟨o.toZFSet, ⋯⟩, invFun := fun x ↦ (↑x).rank, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := fun o ↦ ⟨o.toZFSet, ⋯⟩, invFun := fun x ↦ (↑x).rank, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b

Tactic:
by

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
by

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

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ split 0 = (scale 1 o', m)

Tactic:
by

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

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ 1 + (e - 1) = e

Tactic:
by

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

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
by

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

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m

Tactic:
by

Goal state after:
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'
⊢ ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)

Tactic:
by

Goal state after:
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 = ω ^ 1 * ω ^ (e.repr - 1)
⊢ (e - 1).NF

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
lit : ℕ
h : IsInt a (Int.negOfNat lit)
⊢ a = (algebraMap R A) ((Int.negOfNat lit).rawCast + 0) + 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semifield R
inst✝¹ : Semifield A
inst✝ : Algebra R A
a : A
n d : ℕ
h : IsNNRat a n d
⊢ a = (algebraMap R A) (NNRat.rawCast n d + 0) + 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Field R
inst✝¹ : Field A
inst✝ : Algebra R A
a : A
n d : ℕ
h : IsRat a (Int.negOfNat n) d
⊢ a = (algebraMap R A) (Rat.rawCast (Int.negOfNat n) d + 0) + 0

Tactic:
by

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a : A
h : IsNat a 0
⊢ a = 0

Tactic:
by

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
a : A
lit : ℕ
h : IsNat a lit
⊢ a = (algebraMap R A) (↑lit + 0) + 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
sR : CommSemiring R
⊢ Nat.rawCast 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
sR : CommSemiring R
⊢ Nat.rawCast 1 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_3
inst✝ : Ring R
⊢ (Int.negOfNat n).rawCast = -n.rawCast

Tactic:
by

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

Goal state before:
pp: n d : ℕ
R : Type u_3
inst✝ : DivisionSemiring R
⊢ NNRat.rawCast n d = n.rawCast / d.rawCast

Tactic:
by

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

Goal state before:
pp: n d : ℕ
R : Type u_3
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : n.AtLeastTwo
a : A
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
a : A
inst✝ : n.AtLeastTwo
⊢ -OfNat.ofNat n • a = -OfNat.ofNat n * a

Tactic:
by

Goal state after:
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
a : A
⊢ -1 • a = -a

Tactic:
by

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

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

Tactic:
by

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

Goal state before:
pp: d : ℕ
R : Type u_3
A : Type u_4
inst✝³ : Semifield R
inst✝² : Semifield A
inst✝¹ : Algebra R A
a : A
inst✝ : d.AtLeastTwo
⊢ (1 / OfNat.ofNat d) • a = 1 / OfNat.ofNat d * a

Tactic:
by

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

Goal state before:
pp: n d : ℕ
R : Type u_3
A : Type u_4
inst✝⁴ : Semifield R
inst✝³ : Semifield A
inst✝² : Algebra R A
a : A
inst✝¹ : n.AtLeastTwo
inst✝ : d.AtLeastTwo
⊢ (OfNat.ofNat n / OfNat.ofNat d) • a = OfNat.ofNat n / OfNat.ofNat d * a

Tactic:
by

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

Goal state before:
pp: d : ℕ
R : Type u_3
A : Type u_4
inst✝³ : Field R
inst✝² : Field A
inst✝¹ : Algebra R A
a : A
inst✝ : d.AtLeastTwo
⊢ (-1 / OfNat.ofNat d) • a = -1 / OfNat.ofNat d * a

Tactic:
by

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

Goal state before:
pp: n d : ℕ
R : Type u_3
A : Type u_4
inst✝⁴ : Field R
inst✝³ : Field A
inst✝² : Algebra R A
a : A
inst✝¹ : n.AtLeastTwo
inst✝ : d.AtLeastTwo
⊢ (-OfNat.ofNat n / OfNat.ofNat d) • a = -OfNat.ofNat n / OfNat.ofNat d * a

Tactic:
by

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 : R
h : r = 0
⊢ r • 1 = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a b : A
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
by

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
⊢ r • 1 = s • 1

Tactic:
by

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha₁ : a₁ = 0
ha₂ : a₂ = b₁ + b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
by

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
hb₁ : b₁ = 0
ha : a₁ + a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
by

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha : a₁ = b₁
hb : a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
by

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

Goal state before:
pp: A : Type u_2
e₁ e₂ a b : A
ha : e₁ = a
hb : e₂ = b
hab : a = b
⊢ e₁ = e₂

Tactic:
by

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
c a b : A
h : a = b
⊢ c * a = c * b

Tactic:
by

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 t : R
h : r + s = t
⊢ (algebraMap R A) r + (algebraMap R A) s = (algebraMap R A) t

Tactic:
by

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

Goal state before:
pp: x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + 0).repr = x.repr

Tactic:
by

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
⊢ 0 = ↑0

Tactic:
by

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 ((algebraMap R A) r + (algebraMap R A) s) 0

Tactic:
by

Goal state after: