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

Goal state before:
pp: case oadd
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
cases he : cmp e e'

Goal state after:
case oadd.lt
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.lt
⊢ (match Ordering.lt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

case oadd.eq
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.eq
⊢ (match Ordering.eq with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

case oadd.gt
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.gt
⊢ (match Ordering.gt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (?m.63 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ a

Tactic:
exact hb'.trans (IH b hb)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Iio o)
this : ∃ b < o, List.foldr (?m.63 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ a

Tactic:
by

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

Goal state before:
pp: α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u_1}
h : x.Nonempty
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
by

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

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
by

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

Goal state before:
pp: ⊢ ⋂₀ ∅ = ∅

Tactic:
by

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

Goal state before:
pp: x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
⊢ ↑(⋃₀ x) = ⋃₀ (SetLike.coe '' ↑x)

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
h : x.Nonempty
⊢ ↑(⋂₀ x) = ⋂₀ (SetLike.coe '' ↑x)

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u_1}
H : {x} = {y}
⊢ x = y

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ IsNormal fun x ↦ veblenWith f x 0

Tactic:
by

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

Goal state before:
pp: x y z : ZFSet.{u}
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

Tactic:
by

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

Goal state before:
pp: x y z : ZFSet.{u}
⊢ z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₂ ≤ o₁
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a ↔ veblenWith f o₁ a = a

Tactic:
by

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

Goal state before:
pp: x y z : ZFSet.{u}
⊢ z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x ∪ y) = ↑x ∪ ↑y

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x ∩ y) = ↑x ∩ ↑y

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₂ ≤ o₁
⊢ veblenWith f o₂ a < veblenWith f o₁ (veblenWith f o₂ a) ↔ a < veblenWith f o₁ a

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x \ y) = ↑x \ ↑y

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o (f a) = f a ↔ veblenWith f o a = a

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
hxy : x ⊆ y
⊢ x ∩ y = x

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ f a < veblenWith f o (f a) ↔ a < veblenWith f o a

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
hyx : y ⊆ x
⊢ x ∩ y = y

Tactic:
by

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

Goal state before:
pp: x✝ y z x : ZFSet.{u}
⊢ Function.LeftInverse (fun s ↦ ⟨ZFSet.sep (fun x_1 ↦ x_1 ∈ ↑s) x, ⋯⟩) fun y ↦ ⟨↑↑y, ⋯⟩

Tactic:
by

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

Goal state before:
pp: x✝ y z x : ZFSet.{u}
⊢ Function.RightInverse (fun s ↦ ⟨ZFSet.sep (fun x_1 ↦ x_1 ∈ ↑s) x, ⋯⟩) fun y ↦ ⟨↑↑y, ⋯⟩

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u_1}
⊢ insert x y = {x} ∪ y

Tactic:
by

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ f ⟦x✝¹⟧ ∈ image f ⟦PSet.mk α✝ A✝⟧

Tactic:
by

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

Goal state before:
pp: f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x : ZFSet.{u_1}
⊢ ↑(image f x) = f '' ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f ↔ ∃ i, f i = ⟦y⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ↑(range f) = Set.range f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
a : α
⊢ f a ∈ range f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (i : α), f i ↔ ∃ i, x ∈ f i

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x.pair y) = {{x}, {x, y}}

Tactic:
by

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

Goal state before:
pp: p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
by

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

Goal state before:
pp: α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
⊢ (mk α✝¹ A✝¹).rank = (mk α✝ A✝).rank

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ x✝.rank < (mk α✝ A✝).rank

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
⊢ (mk α✝ A).rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a < veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Tactic:
by

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

Goal state before:
pp: x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ ?m.27

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
by

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

Goal state before:
pp: ⊢ ∅.rank = 0

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a = veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Tactic:
by

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

Goal state before:
pp: x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ y = x → y = y'

Tactic:
by

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

Goal state before:
pp: ⊢ veblen 0 = fun a ↦ ω ^ a

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ veblen 0 a = ω ^ a

Tactic:
by

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

Goal state before:
pp: o a : Ordinal.{u}
⊢ 0 < ω ^ 0

Tactic:
by

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

Goal state before:
pp: ⊢ 0 < ω ^ 0

Tactic:
by

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

Goal state before:
pp: o : ONote
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : o.NF
⊢ (0 - o).NFBelow b

Tactic:
by

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

Goal state before:
pp: o a : Ordinal.{u_1}
⊢ 0 < ω ^ 0

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ a < veblen a a

Tactic:
by

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

Goal state before:
pp: o x : Ordinal.{u}
h : o < x.invVeblen₁
⊢ veblen o x = x

Tactic:
by

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

Goal state before:
pp: o a : Ordinal.{u}
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
by

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

Goal state before:
pp: x y : PSet.{u_1}
⊢ (insert x y).rank = max (succ x.rank) y.rank

Tactic:
by

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

Goal state before:
pp: x : PSet.{u_1}
⊢ max (succ x.rank) ∅.rank = succ x.rank

Tactic:
by

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

Goal state before:
pp: x y : PSet.{u_1}
⊢ {x, y}.rank = max (succ x.rank) (succ y.rank)

Tactic:
by

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

Goal state before:
pp: o x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
by

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

Goal state before:
pp: x : PSet.{u_1}
⊢ x.powerset.rank = succ x.rank

Tactic:
by

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

Goal state before:
pp: o a : Ordinal.{u}
h : a < veblen o a
⊢ (veblen o a).invVeblen₁ = o

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₁ = 0

Tactic:
by

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

Goal state before:
pp: x : PSet.{u_1}
⊢ (⋃₀ x).rank ≤ x.rank

Tactic:
by

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ = a ↔ ω ^ x = veblen x.invVeblen₁ a

Tactic:
by

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a

Tactic:
by

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ ≤ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a

Tactic:
by

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

Goal state before:
pp: ⊢ Function.Injective2 pair

Tactic:
by

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x

Tactic:
by

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ a ≤ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x

Tactic:
by

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x.invVeblen₂ < ω ^ x

Tactic:
by

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

Goal state before:
pp: x y z : ZFSet.{u}
⊢ z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b

Tactic:
by

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

Goal state before:
pp: x y a b : ZFSet.{u}
⊢ a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

Tactic:
by

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

Goal state before:
pp: x : PSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
by

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

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

Tactic:
induction x using mem_wf.induction with

Goal state after:
case h
x✝ x : PSet.{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
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y f : ZFSet.{u}
⊢ f ∈ x.funs y ↔ x.IsFunc y f

Tactic:
by

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x.invVeblen₂ ≤ x

Tactic:
by

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

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

Tactic:
induction x using mem_wf.induction with | _ x ih
   =>  _ 

Goal state after:
case h
x✝ x : PSet.{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
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₂ = a

Tactic:
by

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

Goal state before:
pp: ⊢ invVeblen₂ 0 = 0

Tactic:
by

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

Goal state before:
pp: o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ (veblen o a).invVeblen₂ = a

Tactic:
by

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w ↦ z.pair w ∈ map f x) y
⊢ y = f z

Tactic:
by

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

Tactic:
by

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

Goal state before:
pp: o a x : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ o = deriv (fun a ↦ ω ^ a) o

Tactic:
by

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

Goal state before:
pp: ⊢ ε_ 0 = nfp (fun a ↦ ω ^ a) 0

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ (succ o) = nfp (fun a ↦ ω ^ a) (succ (ε_ o))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ ε_ 0 ≤ o

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u}
o : Ordinal.{u}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
by

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x → p ∅

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ max (succ x.rank) ∅.rank = succ x.rank

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ^ ε_ o = ε_ o

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u_1}
⊢ {x, y}.rank = max (succ x.rank) (succ y.rank)

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o < ε_ 0 ↔ ∃ n, o < (fun a ↦ ω ^ a)^[n] 0

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.Ordinal.Veblen

Goal state before:
pp: n : ℕ
⊢ (fun a ↦ ω ^ a)^[n] 0 < ε_ 0

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω < ε_ o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ Γ_ 0 ≤ o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o < Γ_ 0 ↔ ∃ n, o < (fun a ↦ veblen a 0)^[n] 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (fun a ↦ veblen a 0)^[n] 0 < Γ_ 0

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₁ = Γ_ o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₂ = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ (⋃₀ x).rank ≤ x.rank

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : Class.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) a

Tactic:
by

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

Goal state before:
pp: ⊢ congToClass ∅ = ∅

Tactic:
by

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

Goal state before:
pp: ⊢ ∅.classToCong = ∅

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ z ∈ x ↔ z ∈ y

Tactic:
by

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

Goal state before:
pp: A : Class.{u}
x : ZFSet.{u}
x✝ : A.ToSet ↑x
y : ZFSet.{u}
yx : ↑y = ↑x
py : A y
⊢ A x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ (∃ z, ↑x z ∧ y ∈ z) ↔ ∃ z ∈ x, y ∈ z

Tactic:
by

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

Goal state before:
pp: x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset

Tactic:
mem_powerset

Goal state after:
x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ⊆ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
by

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
by

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

Goal state before:
pp: x : Class.{u}
y : ZFSet.{u}
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

Tactic:
by

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

Goal state before:
pp: x y z : Class.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z

Tactic:
by

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

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
by

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

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
by

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

Goal state before:
pp: ⊢ ⋂₀ ∅ = univ

Tactic:
by

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

Goal state before:
pp: A : Class.{u_1}
hA : A.powerset ⊆ A
⊢ ∀ (x : ZFSet.{u_1}), A x

Tactic:
by

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

Goal state before:
pp: A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
x✝ : A.iota y
x' : ZFSet.{u_1}
h : {x | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ ↑x'
⊢ ↑x y

Tactic:
by

Goal state after: