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

Goal state before:
pp: b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
a : Ordinal.{u_1}
ha : a ∈ (single e' y + f).support
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ a
a✝ : single e' y + f = f → eval b (single a x + (single e' y + f)) = b ^ a * x + eval b (single e' y + f)
he' : e' < a
⊢ a ∈ f.support

Tactic:
simpa using

Goal state after:
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
a : Ordinal.{u_1}
ha : a ∈ (single e' y + f).support
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ a
a✝ : single e' y + f = f → eval b (single a x + (single e' y + f)) = b ^ a * x + eval b (single e' y + f)
he' : e' < a
⊢ ¬f a = 0
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
simpa using

Goal state after:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ a = 0
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ⊆ y
⊢ x.card ≤ y.card

Tactic:
simpa using

Goal state after:
x y : ZFSet.{u}
h : x ⊆ y
⊢ x.card ≤ y.card
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ {x}.card = 1

Tactic:
simpa using

Goal state after:
x : ZFSet.{u}
⊢ {x}.card = 1
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ lift.{u + 1, u} x.powerset.card = lift.{u + 1, u} (2 ^ x.card)

Tactic:
simpa using

Goal state after:
x : ZFSet.{u}
⊢ #{ x_1 // x_1 ⊆ x } = 2 ^ #↥x
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
⊢ (image f x).card ≤ x.card

Tactic:
simpa using

Goal state after:
x : ZFSet.{u}
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
⊢ (image f x).card ≤ x.card
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{v + 1, u} #α

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), v} (range f).card ≤ lift.{v + 1, u} #α
Module: Mathlib.SetTheory.ZFC.Cardinal

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

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ ⨆ i, (f i).card ≤ (⋃ (i : α), f i).card
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{v + 1, max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤ lift.{v + 1, max u v} (sum fun i ↦ (f i).card)

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), v} (⋃ (i : α), f i).card ≤ sum fun i ↦ lift.{v + 1, v} (f i).card
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 1 = deriv f

Tactic:
simpa using

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 1 = deriv f
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:
simpa using

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
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
  simp_rw [(right_le_veblenWith hf ..).lt_iff_ne', ne_eq,
    veblenWith_veblenWith_eq_veblenWith_iff hf h]

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:
simpa using

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o (f a) = f a ↔ veblenWith f o a = a
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:
simpa using

Goal state after:
x y : ZFSet.{u}
hxy : x ⊆ y
z✝ : ZFSet.{u}
⊢ z✝ ∈ x → z✝ ∈ y
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:
simpa using

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ f a < veblenWith f o (f a) ↔ a < veblenWith f o a
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:
simpa using

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ y.Equiv ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Func ((equivShrink α) z))

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ y.Equiv (Quotient.out (mk y))
Module: Mathlib.SetTheory.Ordinal.Notation

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

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 ≤ ω ^ e'.repr * ↑↑n'
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
i : α
x : ZFSet.{u}
hx : x ∈ f i
⊢ ∃ i, x ∈ f i
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:
simpa using

Goal state after:
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
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:
simpa [or_and_left] using (H {x}).1 (Or.inl rfl)

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

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

Tactic:
simpa using

Goal state after:
y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
⊢ y = y'
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
simpa using

Goal state after:
o x : Ordinal.{u}
h : o < x.invVeblen₁
⊢ veblen o x = x
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'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
hy : {x, y} = {x, y'}
⊢ y = x ∨ y = y'

Tactic:
simpa using

Goal state after:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
hy : {x, y} = {x, y'}
⊢ y = x ∨ y = y'
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
by
  rw [← rank_powerset]
  apply rank_mono
  rw [subset_iff]
  intro z _
  rw [mem_powerset, subset_iff]
  intro _ _
  rw [mem_sUnion]
  exists z

Goal state after:
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₁).sub ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
rw [Nat.sub_eq]

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

Tactic:
simpa using

Goal state after:
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ ∃ a ∈ x, o ≤ a.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ veblen 1 o = deriv (fun a ↦ ω ^ a) o
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 : { b // b ∈ x }
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
simpa using

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 : { b // b ∈ x }
⊢ (↑h).rank < x.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω < veblen 1 0

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ ω < veblen 1 0
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ 0
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (a : α), (f a).rank + 1 ≤ ⨆ i, (f i).rank + 1
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
w : ZFSet.{u}
hxw : x w
⊢ y ∈ w

Tactic:
simpa using

Goal state after:
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
w : ZFSet.{u}
hxw : x w
⊢ y ∈ w
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
apply (Ordinal.iSup_le _).antisymm'
  · simpa [rank_le_iff, ← add_one_le_iff] using Ordinal.le_iSup _
  · simp [rank_lt_of_mem]

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

Tactic:
simpa using

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ ∃ a ∈ x, o ≤ a.rank
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
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
simpa using

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : ↥x
⊢ (↑h).rank < x.rank
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
simpa using

Goal state after:
x : ZFSet.{u}
h : x.IsOrdinal
a : ZFSet.{u}
ha : a ∈ x
b : ZFSet.{u}
hb : b ∈ x
⊢ a ∈ b ∨ a = b ∨ b ∈ a
Module: Mathlib.SetTheory.ZFC.VonNeumann

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

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
h : IsSuccPrelimit o
z : ZFSet.{u}
⊢ z.rank < o ↔ ∃ a < o, z.rank < a
Module: Mathlib.SetTheory.ZFC.VonNeumann

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

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.card ≤ (V_ o).card
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∃ b, x.Equiv ((PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Func b)) ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∃ b, x.Equiv (↑b.toOrd).toPSet) ↔ ∃ a < o, x.Equiv a.toPSet
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.toZFSet.card = o.card
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
simpa using

Goal state after:
x✝¹ y z w : ZFSet.{u}
x✝ : { x // x.IsOrdinal }
x : ZFSet.{?u.18}
hx : x.IsOrdinal
⊢ x.rank.toZFSet = x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr

Tactic:
simpa using

Goal state after:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
inst✝ : o.NF
n : ℕ
⊢ (o.mulNat n).NF

Tactic:
simpa using

Goal state after:
o : ONote
inst✝ : o.NF
n : ℕ
⊢ (o * ↑n).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
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 < ω
⊢ ω ^ ω ≤ ω ^ (e.repr * ω)

Tactic:
simpa using

Goal state after:
case inr
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 < ω
⊢ ω ≤ e.repr * ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
⊢ 0 < α'

Tactic:
simpa using

Goal state after:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
⊢ 0 < α'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos.succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
k0 : k = 0
m : ℕ
h : a'.repr + ↑(m + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) (k + 1) (m + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) k (m + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(m + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(m + 1)) + R
⊢ (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) 0 (m + 1)).repr < ω ^ 1

Tactic:
simpa using

Goal state after:
case pos.succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
k0 : k = 0
m : ℕ
h : a'.repr + ↑(m + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) (k + 1) (m + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) k (m + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(m + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(m + 1)) + R
⊢ ↑m + 1 < ω
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 : Tendsto (fun x ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[>] c) l

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c + x⁻¹)) atTop l
⊢ map f (𝓝[>] c) ≤ l
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 : Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l
⊢ Tendsto f (𝓝[<] c) l

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l
⊢ map f (𝓝[<] c) ≤ l
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:
simpa using

Goal state after:
α : 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
⊢ map f (𝓝[<] c) ≤ l ∧ map f (𝓝[>] c) ≤ l
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : ∀ exp' > exp1, f =o[atTop] (b ^ exp')
⊢ ∀ exp' > exp2, f =o[atTop] (b ^ exp')

Tactic:
exact fun exp' h_exp ↦ h _ (by linarith)

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

Goal state before:
pp: f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ Tendsto f atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ Tendsto f atTop (𝓝 0)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case hbc.refine_1
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ a0.repr < a0.repr + a0.repr

Tactic:
simpa using

Goal state after:
case hbc.refine_1
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ 0 < a0.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω ∣ ω0

Tactic:
simpa using

Goal state after:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω ∣ ω0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case left
left right : Basis
h_left : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right)

Tactic:
simpa using

Goal state after:
case left
left right : Basis
h_left : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ a ∈ left, ∀ b ∈ right, (Real.log ∘ b) =o[atTop] (Real.log ∘ a)