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

Goal state before:
pp: case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
h✝¹ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝¹).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
h✝ : o₂ = e₁.oadd n₂ a₁
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₁) h✝).NF
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₁) h✝)

Tactic:
;

Goal state after:
case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
h✝¹ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝¹).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
h✝ : o₂ = e₁.oadd n₂ a₁
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₁) h✝).NF
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₁) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ^ 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ ω ^ 1 ∣ a.repr

Tactic:
;

Goal state after:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ^ 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ ω ^ 1 ∣ a.repr
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y✝ z x y : ZFSet.{u}
hxy : x.toSet = y.toSet
⊢ ∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet

Tactic:
;

Goal state after:
x✝ y✝ z x y : ZFSet.{u}
hxy : x.toSet = y.toSet
⊢ ∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b

Tactic:
;

Goal state after:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y✝ z✝ x y : ZFSet.{u}
hxy : x.toSet = y.toSet
z : ZFSet.{u}
⊢ z ∈ x.toSet ↔ z ∈ y.toSet

Tactic:
;

Goal state after:
x✝ y✝ z✝ x y : ZFSet.{u}
hxy : x.toSet = y.toSet
z : ZFSet.{u}
⊢ z ∈ x.toSet ↔ z ∈ y.toSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b → (e.addAux n (a + o)).NFBelow b

Tactic:
;

Goal state after:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b → (e.addAux n (a + o)).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑∅ ↔ x✝ ∈ ∅

Tactic:
;

Goal state after:
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑∅ ↔ x✝ ∈ ∅
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(insert x y) ↔ x✝ ∈ insert x ↑y

Tactic:
;

Goal state after:
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(insert x y) ↔ x✝ ∈ insert x ↑y
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑{x} ↔ x✝ ∈ {x}

Tactic:
;

Goal state after:
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑{x} ↔ x✝ ∈ {x}
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
;

Goal state after:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
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
⊢ (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:
;

Goal state after:
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
⊢ (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)
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
⊢ (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:
;

Goal state after:
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
⊢ (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)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case 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
⊢ 0 < o ∧ List.foldr (fun x ↦ veblenWith f ↑x) 0 [] ≤ veblenWith f 0 0

Tactic:
;

Goal state after:
case 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
⊢ 0 < o ∧ List.foldr (fun x ↦ veblenWith f ↑x) 0 [] ≤ veblenWith f 0 0
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(x ∪ y) ↔ x✝ ∈ ↑x ∪ ↑y
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(x ∩ y) ↔ x✝ ∈ ↑x ∩ ↑y
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(x \ y) ↔ x✝ ∈ ↑x \ ↑y
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
x y : ZFSet.{u}
hxy : x ⊆ y
z✝ : ZFSet.{u}
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
x y : ZFSet.{u}
hyx : y ⊆ x
z✝ : ZFSet.{u}
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ y
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 simp +contextual [Function.LeftInverse]

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

Goal state before:
pp: x y z✝ : ZFSet.{u_1}
⊢ z✝ ∈ insert x y ↔ z✝ ∈ {x} ∪ y

Tactic:
;

Goal state after:
x y z✝ : ZFSet.{u_1}
⊢ z✝ ∈ insert x y ↔ z✝ ∈ {x} ∪ y
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(image f x) ↔ x✝ ∈ f '' ↑x
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(range f) ↔ x✝ ∈ Set.range f
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
;

Goal state after:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x.rank ≤ o ↔ ∀ y ∈ x, y.rank < o
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:
have h' := sub_nfBelow h₁.snd h₂.snd

Goal state after:
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₁ - a₂).NFBelow e₁.repr
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).NFBelow b
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
apply iff_of_true _ le_rfl

Goal state after:
x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.zero
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
⊢ (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:
by_cases en : n₁ = n₂ <;> simp only [en, ↓reduceIte]

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₂
⊢ (a₁.sub 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₂
⊢ NFBelow 0 b
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
;

Goal state after:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ x.rank ≤ o ↔ ∀ y ∈ x, y.rank < o
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
exact nfp_le_fp (fun _ _ ↦ (opow_le_opow_iff_right one_lt_omega0).2) zero_le h

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
this : a₁.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
;

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this : a₁.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
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
this✝ : a₁.NF
this : a₂.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
;

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
gamma_zero_eq_nfp,

Goal state after:
o : Ordinal.{u}
⊢ o < nfp (fun x ↦ veblen x 0) 0 ↔ ∃ n, o < (fun a ↦ veblen a 0)^[n] 0
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
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
| ((e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂)).repr

Tactic:
;

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
| ((e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂)).repr
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x z : Class.{u_1}
hz : z ∈ x
w : ZFSet.{u_1}
hw : (⋂₀ x) w
⊢ ↑w ∈ z

Tactic:
exact coe_mem.2 (hw z hz)

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:
rw [mem_powerset] at hy ⊢

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: x a₁✝ a₂✝ : ZFSet.{u}
⊢ (fun x ↦ ⟨↑x, ⋯⟩) a₁✝ = (fun x ↦ ⟨↑x, ⋯⟩) a₂✝ → a₁✝ = a₂✝

Tactic:
;

Goal state after:
x a₁✝ a₂✝ : ZFSet.{u}
⊢ (fun x ↦ ⟨↑x, ⋯⟩) a₁✝ = (fun x ↦ ⟨↑x, ⋯⟩) a₂✝ → a₁✝ = a₂✝
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' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hm : m ∈ y ∧ m ∉ x
⊢ m ∈ y

Tactic:
;

Goal state after:
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' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hm : m ∈ y ∧ m ∉ x
⊢ m ∈ y
Module: Mathlib.SetTheory.ZFC.VonNeumann

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y.rank < o

Tactic:
apply (rank_lt_of_mem (hx hy)).trans_le

Goal state after:
case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ (V_ o).rank ≤ o
Module: Mathlib.SetTheory.ZFC.VonNeumann

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

Tactic:
apply iSup_card_le_card_iUnion.antisymm'

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

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

Tactic:
· grw [repr_add, h₂.lt]

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

Goal state before:
pp: o : Ordinal.{u_1}
a✝ : ∀ (y : Ordinal.{u_1}), (invImage (fun x ↦ x) wellFoundedRelation).1 y o → y.toPSet.rank = y
x : ↑(Iio o)
⊢ ↑x < o

Tactic:
;

Goal state after:
o : Ordinal.{u_1}
a✝ : ∀ (y : Ordinal.{u_1}), (invImage (fun x ↦ x) wellFoundedRelation).1 y o → y.toPSet.rank = y
x : ↑(Iio o)
⊢ ↑x < o
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
;

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

Goal state before:
pp: z✝ : ZFSet.{u_1}
⊢ z✝ ∈ toZFSet 0 ↔ z✝ ∈ ∅

Tactic:
;

Goal state after:
z✝ : ZFSet.{u_1}
⊢ z✝ ∈ toZFSet 0 ↔ z✝ ∈ ∅
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
;

Goal state after:
o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ split 0 = (scale 1 o', m)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x✝ : NF 0
⊢ split 0 = (scale 1 0, 0)

Tactic:
;

Goal state after:
x✝ : NF 0
⊢ split 0 = (scale 1 0, 0)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m

Tactic:
;

Goal state after:
o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x✝ : NF 0
⊢ NF 0 ∧ repr 0 = ω * repr 0 + ↑0

Tactic:
;

Goal state after:
x✝ : NF 0
⊢ NF 0 ∧ repr 0 = ω * repr 0 + ↑0
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
⊢ x.scale (e.oadd n a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
;

Goal state after:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ x.scale (e.oadd n a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
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' : Type u_3
inst✝ : HSMul R' A A
r' : R'
r : R
hr : r = 0
h_smul : ∀ (a : A), r • a = r' • a
a : A
⊢ r' • a = 0 * a

Tactic:
simp [← h_smul, hr]

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

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: case intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
left✝ : a.NF
right✝ : o.repr = ω * a.repr + ↑n
⊢ ω ∣ (scale 1 a).repr

Tactic:
;

Goal state after:
case intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
left✝ : a.NF
right✝ : o.repr = ω * a.repr + ↑n
⊢ ω ∣ (scale 1 a).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
m k : ℕ
this : ∀ (m : ℕ), (e.opowAux a0 a k m).NF
⊢ ((e + a0 * ↑k).scale a + e.opowAux a0 a k m.succ).NF

Tactic:
;

Goal state after:
case succ.succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
m k : ℕ
this : ∀ (m : ℕ), (e.opowAux a0 a k m).NF
⊢ ((e + a0 * ↑k).scale a + e.opowAux a0 a k m.succ).NF
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
;

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
x✝ : ℝ
⊢ f x✝ ^ (exp - exp') = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) x✝

Tactic:
;

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
x✝ : ℝ
⊢ f x✝ ^ (exp - exp') = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) x✝
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[≠] c) l

Tactic:
by
  simpa [Tendsto, ← nhdsLT_sup_nhdsGT] using
    ⟨tendsto_nhdsLT_of_tendsto_atTop _ _ h_neg, tendsto_nhdsGT_of_tendsto_atTop _ _ h_pos⟩

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp

Tactic:
;

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp

Tactic:
;

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ exp = f_exp + (exp - f_exp - g_exp) / 2 + (g_exp + (exp - f_exp - g_exp) / 2)

Tactic:
;

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ exp = f_exp + (exp - f_exp - g_exp) / 2 + (g_exp + (exp - f_exp - g_exp) / 2)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
hd : α
x y : Stream'.Seq α
⊢ 2⁻¹ * dist x y ≤ dist x y

Tactic:
linarith [dist_nonneg (x := x) (y := y)]

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

Goal state before:
pp: case pos
o₁ : ONote
inst✝¹ : o₁.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
inst✝ : NF 0
⊢ (o₁ ^ 0).repr = o₁.repr ^ repr 0

Tactic:
;

Goal state after:
case pos
o₁ : ONote
inst✝¹ : o₁.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
inst✝ : NF 0
⊢ (o₁ ^ 0).repr = o₁.repr ^ repr 0