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

Goal state before:
pp: case inr.inl
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (0, (single 0 o) 0) ∈ [(0, o)]

Tactic:
simp

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

Goal state before:
pp: case inl
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e 0 + f) = b ^ e * 0 + eval b f

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
⊢ IsSuccLimit a

Tactic:
rw [← isOpen_singleton_iff.not_left]
  rw [frontier_eq_closure_inter_closure] at ha
  grind [mem_closure_iff, Set.Nonempty]

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

Goal state before:
pp: case zero
b e x : Ordinal.{u_1}
h : ∀ e' ∈ support 0, e' ≤ e
⊢ eval b (single e x + 0) = b ^ e * x + eval b 0

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ (↑0).repr = ↑0

Tactic:
simp

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (↑(n✝ + 1)).repr = ↑(n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case zero
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ support 0, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (0 + f₂) = eval b 0 + eval b f₂

Tactic:
simp

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

Goal state before:
pp: case eq.eq
e₁ a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
h₂ : ↑n₂ = ↑n₂
⊢ e₁.oadd n₂ a₁ = e₁.oadd n₂ a₁

Tactic:
simp

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

Goal state before:
pp: s : Set Ordinal.{u}
ι : Type u
w✝ : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ type WellOrderingRel ≠ 0

Tactic:
simp

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

Goal state before:
pp: case zero
b : Ordinal.{u_1}
hb : 1 < b
hf : ∀ (e : Ordinal.{u_1}), 0 e < b
⊢ coeff b (eval b 0) = 0

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬IsMin o ∧ ∀ b < o, (S ∩ Ioo b o).Nonempty) ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ IsClosedBelow (⋂₀ S) o

Tactic:
isClosedBelow_iff

Goal state after:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x < b

pp: case single_add.hy
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ eval b f < b ^ e

Tactic:
· apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false

Goal state after:
case single_add.hy
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ eval b f < b ^ e
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x : PSet.{u_1}
y : PSet.{u_2}
inst✝¹ : IsEmpty x.Type
inst✝ : IsEmpty y.Type
⊢ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)

Tactic:
simp

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

Goal state before:
pp: x y z : PSet.{u_1}
⊢ x ∈ {y, z} ↔ x.Equiv y ∨ x.Equiv z

Tactic:
simp

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

Goal state before:
pp: x x✝ : PSet.{u}
⊢ x✝ ∈ (⋃₀ x).toSet ↔ x✝ ∈ ⋃₀ (toSet '' x.toSet)

Tactic:
simp

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

Goal state before:
pp: ⊢ #↥∅ = lift.{u_1 + 1, u_1} 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 0 a ∈ range f

Tactic:
simp

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

Goal state before:
pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f 0 (veblenWith f o a) ∈ range f

Tactic:
simp

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

Goal state before:
pp: a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(ZFSet.sep p a) ↔ x✝ ∈ {x | x ∈ a ∧ p x}

Tactic:
simp

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

Goal state before:
pp: case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Tactic:
rw [← ha]

Goal state after:
case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ veblenWith f o a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
x✝¹ : NF 0
x✝ : o.NF
⊢ (0 + o).repr = repr 0 + o.repr

Tactic:
simp

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

Goal state before:
pp: z✝ : ZFSet.{u}
⊢ z✝ ∈ ⋃₀ ∅ ↔ z✝ ∈ ∅

Tactic:
simp

Goal state after:
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)
IH : ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 (a :: l) ≤ veblenWith f b 0

Tactic:
obtain ⟨b, hb, hb'⟩ := IH
    refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
      hb'.trans <| veblenWith_left_monotone hf _ <|
        (le_max_right a.1 b).trans (le_succ _)).trans ?_⟩
    rw [veblenWith_veblenWith_of_lt hf]
    rw [lt_succ_iff]
    exact le_max_left _ b

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
by
  simpa using veblenWith_veblenWith_eq_veblenWith_iff hf zero_le

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:
simp

Goal state after:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ 0 < veblen 0 0

Tactic:
simp

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

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

Tactic:
simp

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

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

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

pp: case inr.inr
o x : Ordinal.{u}
h : x.invVeblen₁ < o
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
· exact iff_of_true ⟨_, veblen_opow_eq_opow_iff.2 <| veblen_eq_of_lt_invVeblen₁ h⟩ h.le

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

case inr.inr
o x : Ordinal.{u}
h : x.invVeblen₁ < o
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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:
simp

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

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

Tactic:
subset_iff

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

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

Tactic:
subset_iff

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.ZFC.Basic

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

Tactic:
simp [prod]

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ 0 < veblen 0 0

Tactic:
simp

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

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

Tactic:
apply le_antisymm
  · simp_rw [rank_le_iff, mem_union, lt_max_iff]
    intro
    apply Or.imp <;> apply rank_lt_of_mem
  · apply max_le <;> apply rank_mono <;> intro _ h <;> simp [h]

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

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

Tactic:
simp

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

Goal state before:
pp: z✝ : ZFSet.{u}
⊢ (⋃₀ ∅) z✝ ↔ ∅ z✝

Tactic:
simp

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

Goal state before:
pp: case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x

pp: case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
· obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy
    exact h.mem_trans hz' hz

Goal state after:
case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ 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:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: ⊢ ∀ (x y : Ordinal.{u_1}), x ≤ y ↔ V_ x ⊆ V_ y

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ (V_ 0).card = preBeth 0

Tactic:
simp

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

Goal state before:
pp: x y z w : ZFSet.{u}
a b : Ordinal.{?u.18}
⊢ { toFun := fun o ↦ ⟨o.toZFSet, ⋯⟩, invFun := fun x ↦ (↑x).rank, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := fun o ↦ ⟨o.toZFSet, ⋯⟩, invFun := fun x ↦ (↑x).rank, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
sR : CommSemiring R
⊢ Nat.rawCast 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
sR : CommSemiring R
⊢ Nat.rawCast 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n : ℕ
R : Type u_3
inst✝ : Ring R
⊢ (Int.negOfNat n).rawCast = -n.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n d : ℕ
R : Type u_3
inst✝ : DivisionSemiring R
⊢ NNRat.rawCast n d = n.rawCast / d.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n d : ℕ
R : Type u_3
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ -1 • a = -a

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
b₁ b₂ : A
⊢ 0 + (b₁ + b₂) = b₁ + b₂

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ : A
⊢ a₁ + a₂ = 0 + (a₁ + a₂)

Tactic:
simp

Goal state after:
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
this : a.NF
e0 : e = 0
⊢ (x + 0).repr = x.repr

Tactic:
simp

Goal state after:
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 s : R
h : r + s = 0
⊢ 0 = ↑0

Tactic:
simp

Goal state after:
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 : R
h : IsNat r 1
⊢ 1 = ↑1

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: case e'_8
f g basis_hd : ℝ → ℝ
exp✝ : ℝ
hf : Majorized f basis_hd exp✝
hg : g =O[atTop] fun x ↦ 1
exp : ℝ
h_exp : exp > exp✝
⊢ basis_hd ^ exp = fun x ↦ (basis_hd ^ exp) x * 1

Tactic:
simp

Goal state after:
case e'_8
f g basis_hd : ℝ → ℝ
exp✝ : ℝ
hf : Majorized f basis_hd exp✝
hg : g =O[atTop] fun x ↦ 1
exp : ℝ
h_exp : exp > exp✝
⊢ basis_hd ^ exp = fun x ↦ basis_hd x ^ exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ List.Sublist basis_tl (basis_hd :: basis_tl)

Tactic:
simp

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

Goal state before:
pp: left right : Basis
h : WellFormedBasis (left ++ right)
⊢ List.Sublist right (left ++ right)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ n ≤ n + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ n, (1 / 2) ^ PiNat.firstDiff ↑s ↑t = 2⁻¹ ^ n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ 1 / 2 = 2⁻¹

Tactic:
simp

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : ∀ (g : ℝ → ℝ), (basis_hd :: basis_tl).head? = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_hd :: basis_tl
⊢ (basis_hd :: basis_tl).head? = some basis_hd

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ (Seq.cons x s).head ≠ nil.head

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist (Seq.cons x s) nil = 1

Tactic:
simp

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

Goal state before:
pp: case nil.nil
α : Type u_1
h : True
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

Tactic:
simp

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

Goal state before:
pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

Tactic:
simp

Goal state after:
case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ x✝ = x✝¹
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case inl
α : Type u_1
⊢ dist nil nil ≤ 2⁻¹

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
hd : α
s' t' : Stream'.Seq α
⊢ dist (Seq.cons hd s') (Seq.cons hd t') ≤ 2⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ 1 = 1 * 1

Tactic:
simp

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

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Sublist right (left ++ right)

Tactic:
simp

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

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
⊢ List.Sublist left (left ++ right)

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
⊢ dist
      (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
      (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (g b'))) ≤
    2⁻¹ * dist f g

Tactic:
simp

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

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ List.Sublist left (left ++ right)

Tactic:
simp

Goal state after: