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

Goal state before:
pp: 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
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e'.repr * ↑↑n' + a'.repr

pp: case oadd.lt.h₁
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
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr

pp: case oadd.lt.h₂
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
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr ≤ ω ^ e'.repr * ↑↑n'

Tactic:
]

Goal state after:
case oadd.lt.h₁
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
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr

case oadd.lt.h₂
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
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr ≤ ω ^ e'.repr * ↑↑n'
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case cons
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✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ veblenWith f (succ (max (↑a) b)) 0 ≤ veblenWith f (succ (max (↑a) b)) 0

pp: case cons.h
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✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a < succ (max (↑a) b)

Tactic:
]

Goal state after:
case cons.h
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✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a < succ (max (↑a) b)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case cons.h
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✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a ≤ max (↑a) b

Tactic:
]

Goal state after:
case cons.h
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✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a ≤ max (↑a) b
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
]

Goal state after:
x y : ZFSet.{u_1}
H : {x} = {y}
this : x = y
⊢ x = y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mp
α✝¹ : 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)
x✝ : Ordinal.{u_1}
a : α✝¹
h : succ (A✝¹ a).rank = x✝
b : α✝
h' : (A✝¹ a).Equiv (A✝ b)
⊢ succ (A✝ b).rank = succ (A✝ b).rank

Tactic:
]

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

Goal state before:
pp: case mpr
α✝¹ : 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)
x✝ : Ordinal.{u_1}
a : α✝
h : succ (A✝ a).rank = x✝
b : α✝¹
h' : (A✝¹ b).Equiv (A✝ a)
⊢ succ (A✝ a).rank = succ (A✝ a).rank

Tactic:
]

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✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank

Tactic:
]

Goal state after:
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ (A a).rank < o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (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) =
      Ordering.lt ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (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) =
      Ordering.lt ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e'.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e'.repr * (↑↑n + ↑↑n') + a'.repr

Tactic:
]

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
⊢ ¬(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) =
        Ordering.gt ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ ¬(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) =
        Ordering.gt ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (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) =
      Ordering.eq ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (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) =
      Ordering.eq ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: ⊢ (fun x ↦ ω ^ x) = fun a ↦ ω ^ a

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inl
o a : Ordinal.{u}
h : o < a.invVeblen₁
⊢ a < a ↔ a.invVeblen₁ ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ x = x
hz' : veblen o z = ω ^ x
⊢ False

Tactic:
]

Goal state after:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ x = x
hz' : veblen o z = ω ^ x
⊢ False
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank

Tactic:
]

Goal state after:
case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ a < veblen o a

Tactic:
]

Goal state after:
case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ a < veblen o a
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
rwa [← lt_veblen_iff_invVeblen₁_le, veblen_lt_veblen_iff_right]

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

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ ω ^ veblen o a ∈ range (veblen o)

Tactic:
]

Goal state after:
case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ ω ^ veblen o a ∈ range (veblen o)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a ∈ range (veblen o)

Tactic:
]

Goal state after:
case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a ∈ range (veblen o)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ a < (fun a ↦ ω ^ a) a

Tactic:
]

Goal state after:
a : Ordinal.{u}
h : a < ω ^ a
⊢ a < (fun a ↦ ω ^ a) a
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : PSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
]

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

Goal state before:
pp: x : PSet.{u_1}
⊢ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
]

Goal state after:
x : PSet.{u_1}
⊢ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x z : PSet.{u_1}
a✝ : z ∈ x
⊢ ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x

Tactic:
]

Goal state after:
x z : PSet.{u_1}
a✝ : z ∈ x
⊢ ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x < veblen x.invVeblen₁ x

Tactic:
]

Goal state after:
x : Ordinal.{u_1}
⊢ x < veblen x.invVeblen₁ x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
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.eq
⊢ (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₁).NFBelow
    b

Tactic:
]

Goal state after:
case eq
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.eq
⊢ (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₁).NFBelow
    b
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z

Tactic:
]

Goal state after:
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inl
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
⊢ ω ^ x ≤ (fun a ↦ ω ^ a) x

Tactic:
]

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

Goal state before:
pp: x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x = x

Tactic:
]

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

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

Tactic:
IsWellFounded.rank_eq

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 = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) ↑b)
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
]

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

Goal state before:
pp: 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 = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) ↑b)

Tactic:
]

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 = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) ↑b)
Module: Mathlib.SetTheory.Ordinal.Veblen

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

pp: case h
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ 0 < o

Tactic:
]

Goal state after:
case h
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ 0 < o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case refine_1.inl
a x : Ordinal.{u}
h : a < (fun a ↦ ω ^ a) a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a

Tactic:
]

Goal state after:
case refine_1.inl
a x : Ordinal.{u}
h : a < (fun a ↦ ω ^ a) a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
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
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
⊢ f z = f z

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case refine_1.inr
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a = x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
]

Goal state after:
case refine_1.inr
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a = x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : PSet.{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 : PSet.{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.Ordinal.Veblen

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ nfp (fun a ↦ ω ^ a) 0 ≤ o

Tactic:
]

Goal state after:
o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ nfp (fun a ↦ ω ^ a) 0 ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℕ
⊢ (fun a ↦ ω ^ a)^[n] 0 < nfp (fun a ↦ ω ^ a) 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ nfp (fun x ↦ veblen x 0) 0 ≤ o

Tactic:
]

Goal state after:
o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ nfp (fun x ↦ veblen x 0) 0 ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℕ
⊢ (fun a ↦ veblen a 0)^[n] 0 < nfp (fun x ↦ veblen x 0) 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ Γ_ o = Γ_ o

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o

Tactic:
]

Goal state after:
case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
by
  constructor
  · rw [mem_range_gamma, or_iff_not_imp_left]
    refine fun h ho ↦ (left_le_veblen ..).antisymm' ?_
    conv_rhs => rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]
    simp
  · aesop

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ZFSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
]

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 x
⊢ A x

Tactic:
]

Goal state after:
A : Class.{u}
x : ZFSet.{u}
x✝ : A.ToSet ↑x
y : ZFSet.{u}
yx : ↑y = ↑x
py : A x
⊢ A x
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
]

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

Goal state before:
pp: x z : ZFSet.{u_1}
a✝¹ : z ∈ x
x✝ : ZFSet.{u_1}
a✝ : x✝ ∈ z
⊢ ∃ z ∈ x, x✝ ∈ z

Tactic:
]

Goal state after:
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
x✝ : ZFSet.{u_1}
a✝ : x✝ ∈ z
⊢ ∃ z ∈ x, x✝ ∈ z
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:
]

Goal state after:
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
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}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y

Tactic:
]

Goal state after:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y
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
wy : w = y
fw : f w = z
⊢ f y = f y

Tactic:
]

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
⊢ y ∈ x

Tactic:
]

Goal state after:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
n : ¬∃ y_1, y_1 ∈ y
⊢ y ∈ x
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun z ↦ z ∈ y) ∈ y

Tactic:
]

Goal state after:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun z ↦ z ∈ y) ∈ y
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∧ z ∈ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
]

Goal state after:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ (⋃₀ {x, y}).IsTransitive
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ = x ∨ y✝ = y → y✝.IsTransitive

Tactic:
]

Goal state after:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ = x ∨ y✝ = y → y✝.IsTransitive
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:
]

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

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

Tactic:
]

Goal state after:
case refine_1
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
b : (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)).Type
h2 : x = mk ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)).Func b)
⊢ x ∈ s