mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case h.«1»
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun i ↦ i) ⟨1, ⋯⟩, m) ∈ univ ×ˢ range (n + 1)
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩).1
      ⟨(↑⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) ⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ (range fun n ↦ f ⟨t, ht⟩ (g n)) ⊆ t

Tactic:
grind

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : cof α < ℵ₀
⊢ IsClub (⋂₀ s)

pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)

Tactic:
· apply IsClub.sInter_of_cof_le_one _ hs
    rwa [← cof_lt_aleph0_iff]

Goal state after:
case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
t : Set (List A)
ht : t ∈ S
hx : x ++ [a] ∈ t
⊢ x ∈ sSup S

Tactic:
use t, ht, hS ht hx

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
⊢ o₁ + (o₁ + o₃) = o₁ + (o₃ + o₁)

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ ∀ i < a, ∃ i', ∃ (_ : i' < b), f (lfpApprox f x i) ≤ f (lfpApprox f x i')

Tactic:
grind

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

Goal state before:
pp: case refine_2.inl
b o✝ o : Ordinal.{u}
ho : o ≠ 0
H : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).1 ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).1 ≤ log b o

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩
  obtain - | ⟨h₁, h₂⟩ := h
  · simp [Lists'.Subset.refl]
  · exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case refl
α : Type u_1
a : α
⊢ atom a = atom a

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case refl
α : Type u_1
l₁ : Lists α
⊢ l₁ ~ l₁

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mp
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ Lists'.atom a✝ = Lists'.atom a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, Lists'.atom a✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Decidable (a ∈ l₂)
⊢ a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons ⟨b✝, b⟩ l₂

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ (∃ i < o, Ioc i o ⊆ s) ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∀ i < a, ∃ x ∈ Ioc i a, x ≠ a ∧ x ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, ∃ x ∈ s, x ∈ Ioo b a

Tactic:
grind

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₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
by
    revert h; simp only [cmp]
    cases h₁ : cmp e₁ e₂ <;> intro h <;> try cases h
    obtain rfl := eq_of_cmp_eq h₁
    revert h; cases h₂ : _root_.cmp (n₁ : ℕ) n₂ <;> intro h <;> try cases h
    obtain rfl := eq_of_cmp_eq h
    rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂
    obtain rfl := Subtype.ext h₂
    simp

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

Goal state before:
pp: 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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ x < b

Tactic:
apply (hb e').trans_eq'

Goal state after:
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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ (single e' x + f) e' = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ eval b (coeff b o) = o

Tactic:
conv_rhs => rw [← CNF.foldr b o]
  rw [eval, support_coeff, (toFinset_sort _ _).2, foldr_map]
  · apply foldr_ext
    intro a ha x
    rw [coeff_of_mem_CNF ha]
  · exact (CNF.sortedGT b o).sortedGE.pairwise
  · exact (CNF.sortedGT b o).nodup

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

Goal state before:
pp: case eq
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.eq ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

pp: case gt
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.gt ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
case gt =>
        rcases nh with nh | nh
        · cases nh; contradiction
        · obtain ⟨_, nh⟩ := nh
          rw [ite_eq_iff] at nh; rcases nh with nh | nh
          · exact oadd_lt_oadd_2 h₂ nh.left
          · cases nh; contradiction

Goal state after:
case eq
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.eq ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
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 [cardinalMk_coe_sort, ← coe_range, -mem_range] using mk_range_le_lift (f := f)

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

Goal state before:
pp: n✝ : ZFSet.{u}
x : PSet.{u}
x✝ : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n })
⊢ insert (mk (PSet.omega.Func { down := n })) (mk (PSet.omega.Func { down := n })) =
    insert (mk (ofNat n)) (mk (ofNat n))

Tactic:
rfl

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

pp: case gt
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.gt
⊢ (match Ordering.gt 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]
      simp only [h, Ordering.compares_eq] at this
      subst e₂
      cases (n₁ : ℕ) - n₂
      · by_cases en : n₁ = n₂ <;> simp only [en, ↓reduceIte]
        · exact h'.mono (le_of_lt h₁.lt)
        · exact NFBelow.zero
      · exact NFBelow.oadd h₁.fst h₁.snd h₁.lt

Goal state after:
case gt
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.gt
⊢ (match Ordering.gt 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
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case inr
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ ↑y
⊢ p ∅

Tactic:
· exact IH a ha (h.mem ha)

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

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

Tactic:
apply iterate_lt_nfp (isNormal_opow one_lt_omega0).strictMono

Goal state after:
n : ℕ
⊢ 0 < ω ^ 0
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: ⊢ congToClass ∅ = ∅

Tactic:
rfl

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ (∃ z, ↑x z ∧ y ∈ z) ↔ ∃ z ∈ x, y ∈ z

Tactic:
rfl

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

Goal state before:
pp: case lt
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
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt 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₁).repr =
    0

Tactic:
rfl

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

Goal state before:
pp: case mpr.inl
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ 0 * zero = 0

Tactic:
rfl

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

Goal state before:
pp: case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ 0 * a✝².oadd a✝¹ a✝ = 0

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ zero * 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ a✝².oadd a✝¹ a✝ * 0 = 0

Tactic:
rfl

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Type = o.ToType

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: A : Type u_2
b : A
⊢ b = b

Tactic:
rfl

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

Goal state before:
pp: case zero.zero
⊢ zero.mulNat 0 = zero * ↑0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case oadd.zero
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ (a✝².oadd a✝¹ a✝).mulNat 0 = a✝².oadd a✝¹ a✝ * ↑0

Tactic:
rfl

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

Goal state before:
pp: case oadd.succ
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
n✝ : ℕ
⊢ (a✝².oadd a✝¹ a✝).mulNat (n✝ + 1) = a✝².oadd a✝¹ a✝ * ↑(n✝ + 1)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
o : ONote
⊢ o.mulNat n = o * ↑n

Tactic:
by cases o <;> cases n <;> rfl

Goal state after:
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 (add_lt_add_iff_left (repr a0)).2 e0

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 x ^ exp

Tactic:
rfl

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

Goal state before:
pp: f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g ∈ basis_begin
h :
  List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
    ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Tendsto f atTop atTop
⊢ (Real.log ∘ basis_end) =o[atTop] (Real.log ∘ g)

Tactic:
grind

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

Goal state before:
pp: case inr.inr
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g = basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
grind

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 : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ n + 1 ≤ n + 1

Tactic:
rfl

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ basis_hd)

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst✝ : DecidablePred P
s t : Stream'.Seq α
h_head : s.head = t.head
⊢ dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t

Tactic:
grind

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

pp: case right
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)
⊢ ∀ f ∈ left ++ right, Tendsto f atTop atTop

Tactic:
· simpa [List.pairwise_append, h_left, h_right] using h

Goal state after:
case right
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)
⊢ ∀ f ∈ left ++ right, Tendsto f atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case right
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)
⊢ ∀ f ∈ left ++ right, Tendsto f atTop atTop

Tactic:
grind

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)
g : ℝ → ℝ
hg : g ∈ left
⊢ ∀ (g_1 : ℝ → ℝ), (f :: right).head? = some g_1 → (Real.log ∘ g_1) =o[atTop] (Real.log ∘ g)

Tactic:
grind

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

Goal state before:
pp: case h
α : 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 : β
a : α
c : γ
b' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ ∀ (a : β), dist (f a) (g a) ≤ C

Tactic:
grind

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

Goal state before:
pp: case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h : WellFormedBasis (hd :: tl)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (x : ℝ), (basis_hd ∈ basis_hd :: basis_tl → 0 < basis_hd x) → 0 < basis_hd x

Tactic:
grind

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

Goal state before:
pp: case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
⊢ nil.head = nil.head

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
hd : α
s_tl t_tl : Stream'.Seq α
⊢ (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head

Tactic:
rfl

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

Goal state before:
pp: case keep
basis : Basis
basis_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
ex : BasisExtension basis_tl✝
ih : List.Sublist basis_tl✝ ex.getBasis
⊢ (basis_hd✝ :: basis_tl✝).Sublist (keep basis_hd✝ ex).getBasis

Tactic:
| keep _ ex ih =>

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

Goal state before:
pp: basis : Basis
⊢ zero.toFun = 0

Tactic:
rfl

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

Goal state before:
pp: basis : Basis
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ zero.toFun = 0

Tactic:
rfl

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

Goal state before:
pp: basis : Basis
⊢ (fun x ↦ 1) = 1

Tactic:
rfl

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

Goal state before:
pp: head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ (fun x ↦ 0) =ᶠ[atTop] 0

Tactic:
rfl

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

Goal state before:
pp: case nil
r : ℝ
n : Fin [].length
⊢ (monomialRpow [] (↑n) r).toFun = [][n] ^ r

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : Option.map Prod.fst s.destruct = Option.map Prod.fst t.destruct
⊢ Option.map (Prod.fst ∘ fun x ↦ (x.1, ↑x.2 s.tail)) (h.unfold (Option.map Prod.fst t.destruct)) =
    Option.map (Prod.fst ∘ fun x ↦ (x.1, ↑x.2 t.tail)) (h.unfold (Option.map Prod.fst t.destruct))

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
hst✝ : ¬s = t
n : ℕ
hst : dist s t = 2⁻¹ ^ n
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
grind

Goal state after: