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

Goal state before:
pp: case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (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')).NFBelow
    b

pp: case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (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')).NFBelow
    b

pp: case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (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')).NFBelow
    b

Tactic:
<;>

Goal state after:
case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (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')).NFBelow
    b

case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (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')).NFBelow
    b

case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (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')).NFBelow
    b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
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
nf : (a.add o).NF
h : a.add o = zero
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

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
nf : (a.add o).NF
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

Tactic:
<;>

Goal state after:
case zero
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
nf : (a.add o).NF
h : a.add o = zero
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

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
nf : (a.add o).NF
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
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
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)

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
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)

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

Tactic:
<;>

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

Goal state before:
pp: case oadd.lt.h₁.zero
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'
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ e'.repr
he' : e' = zero
⊢ ω ^ e.repr * ↑↑n < ω ^ zero.repr

pp: case oadd.lt.h₁.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
he : e.cmp e' = Ordering.lt
ee : e < e'
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ e'.repr
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
he' : e' = a✝².oadd a✝¹ a✝
⊢ ω ^ e.repr * ↑↑n < ω ^ (a✝².oadd a✝¹ a✝).repr

Tactic:
<;>

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

case oadd.lt.h₁.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
he : e.cmp e' = Ordering.lt
ee : e < e'
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ e'.repr
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
he' : e' = a✝².oadd a✝¹ a✝
⊢ ω ^ e.repr * ↑↑n < ω ^ (a✝².oadd a✝¹ a✝).repr
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}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank

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}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank

Tactic:
<;>

Goal state after:
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}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank

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}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank
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}
⊢ ∀ (x : α✝¹), succ (A✝¹ x).rank = x✝ → ∃ y, succ (A✝ y).rank = x✝

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}
⊢ ∀ (x : α✝), succ (A✝ x).rank = x✝ → ∃ y, succ (A✝¹ y).rank = x✝

Tactic:
<;>

Goal state after:
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}
⊢ ∀ (x : α✝¹), succ (A✝¹ x).rank = x✝ → ∃ y, succ (A✝ y).rank = x✝

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}
⊢ ∀ (x : α✝), succ (A✝ x).rank = x✝ → ∃ y, succ (A✝¹ y).rank = x✝
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.lt.h₁.zero
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'
he' : e' = zero
this : ω ^ e.repr * ↑↑n + a.repr < 1
⊢ ω ^ e.repr * ↑↑n < 1

pp: case oadd.lt.h₁.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
he : e.cmp e' = Ordering.lt
ee : e < e'
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
he' : e' = a✝².oadd a✝¹ a✝
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ (ω ^ a✝².repr * ↑↑a✝¹ + a✝.repr)
⊢ ω ^ e.repr * ↑↑n < ω ^ (ω ^ a✝².repr * ↑↑a✝¹ + a✝.repr)

Tactic:
<;>

Goal state after:
case oadd.lt.h₁.zero
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'
he' : e' = zero
this : ω ^ e.repr * ↑↑n + a.repr < 1
⊢ ω ^ e.repr * ↑↑n < 1

case oadd.lt.h₁.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
he : e.cmp e' = Ordering.lt
ee : e < e'
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
he' : e' = a✝².oadd a✝¹ a✝
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ (ω ^ a✝².repr * ↑↑a✝¹ + a✝.repr)
⊢ ω ^ e.repr * ↑↑n < ω ^ (ω ^ a✝².repr * ↑↑a✝¹ + a✝.repr)
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
simp [pair]

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

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

pp: case oadd
b : Ordinal.{0}
x✝ : NFBelow 0 b
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).NFBelow b

Tactic:
<;>

Goal state after:
case zero
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : zero.NF
⊢ (0 - zero).NFBelow b

case oadd
b : Ordinal.{0}
x✝ : NFBelow 0 b
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).NFBelow b
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < ?m.36

pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?m.36 < x.rank

pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ Ordinal.{u_1}

Tactic:
<;>

Goal state after:
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < ?m.36

x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?m.36 < x.rank

x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ Ordinal.{u_1}
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

pp: case x
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ PSet.{u_1}

pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x

Tactic:
<;>

Goal state after:
case a
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

case x
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ PSet.{u_1}

x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
obtain h | h := eq_zero_or_pos (invVeblen₁ x)
  · rw [invVeblen₂_le_iff, h, veblen_zero]
  · convert! (invVeblen₂_lt x).le
    rw [← veblen_zero_apply, veblen_eq_of_lt_invVeblen₁ h]

Goal state after:
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
⊢ ∀ c < lift.{u + 1, u} x.rank, c < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

pp: x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ ∀ (i : { b // b ∈ x }), succ (lift.{u + 1, u} (↑i).rank) ≤ lift.{u + 1, u} x.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
⊢ ∀ c < lift.{u + 1, u} x.rank, c < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ ∀ (i : { b // b ∈ x }), succ (lift.{u + 1, u} (↑i).rank) ≤ lift.{u + 1, u} x.rank
Module: Mathlib.SetTheory.Ordinal.Notation

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

pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match 0 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 pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : n₁ = n₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 - zero).repr = repr 0 - zero.repr

pp: case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).repr = repr 0 - (a✝².oadd a✝¹ a✝).repr

Tactic:
<;>

Goal state after:
case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 - zero).repr = repr 0 - zero.repr

case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).repr = repr 0 - (a✝².oadd a✝¹ a✝).repr
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.f
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ x → y✝.rank < x.rank

pp: case a.g
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ y → y✝.rank < y.rank

Tactic:
<;>

Goal state after:
case a.f
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ x → y✝.rank < x.rank

case a.g
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ y → y✝.rank < y.rank
Module: Mathlib.SetTheory.ZFC.Rank

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

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

Tactic:
<;>

Goal state after:
case a.h₁
x y : ZFSet.{u_1}
⊢ x.rank ≤ (x ∪ y).rank

case h₂
x y : ZFSet.{u_1}
⊢ y.rank ≤ (x ∪ y).rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.h₁
x y : ZFSet.{u_1}
⊢ x ⊆ x ∪ y

pp: case h₂
x y : ZFSet.{u_1}
⊢ y ⊆ x ∪ y

Tactic:
<;>

Goal state after:
case a.h₁
x y : ZFSet.{u_1}
⊢ x ⊆ x ∪ y

case h₂
x y : ZFSet.{u_1}
⊢ y ⊆ x ∪ y
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
apply (gamma_le_gamma.2 zero_le).trans_lt'
  simpa using iterate_veblen_lt_gamma_zero 2

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

Goal state before:
pp: case a.h₁
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ x
⊢ x✝ ∈ x ∪ y

pp: case h₂
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ y
⊢ x✝ ∈ x ∪ y

Tactic:
<;>

Goal state after:
case a.h₁
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ x
⊢ x✝ ∈ x ∪ y

case h₂
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ y
⊢ x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < ?m.36

pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?m.36 < x.rank

pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ Ordinal.{u_1}

Tactic:
<;>

Goal state after:
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < ?m.36

x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?m.36 < x.rank

x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ Ordinal.{u_1}
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

pp: case x
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ZFSet.{u_1}

pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x

Tactic:
<;>

Goal state after:
case a
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

case x
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ZFSet.{u_1}

x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
exact (rank_lt_of_mem hy).trans_le (Ordinal.le_iSup _ _)

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

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

pp: case mpr
x : ZFSet.{u}
⊢ ⋃₀ x ⊆ x → x.IsTransitive

Tactic:
<;>

Goal state after:
case mp
x : ZFSet.{u}
⊢ x.IsTransitive → ⋃₀ x ⊆ x

case mpr
x : ZFSet.{u}
⊢ ⋃₀ x ⊆ x → x.IsTransitive
Module: Mathlib.SetTheory.ZFC.Class

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

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

Tactic:
<;>

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

case refine_2
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : y✝ ∈ z✝
hzw : z✝ ∈ w✝
hwx : w✝ ∈ x
⊢ y✝ ∈ w✝
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
⊢ ∀ c < lift.{u + 1, u} x.rank, c < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

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

Tactic:
<;>

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

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

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

pp: case eq.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
⊢ (match n✝ + 1 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
<;>

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

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
⊢ (match n✝ + 1 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.VonNeumann

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

pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ (∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o) → x ⊆ V_ o

Tactic:
<;>

Goal state after:
case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o → ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o

case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ (∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o) → x ⊆ V_ o