mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑(n + 1) ↔ projectiveDimension M + ↑1 ≤ ↑(n + 1)

Tactic:
Nat.cast_add

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑(n + 1) ↔ projectiveDimension M + ↑1 ≤ ↑n + ↑1
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
⊢ IsRegularRing R[X]

Tactic:
apply isRegularRing_iff.mpr (fun p hp ↦ ?_)
  let q := p.comap C
  let S := (Localization.AtPrime q)[X]
  let pc := Submonoid.map Polynomial.C.toMonoidHom q.primeCompl
  let : Algebra R[X] S := algebra R (Localization.AtPrime q)
  have : IsLocalization pc S := Polynomial.isLocalization _ _
  let pS := p.map (algebraMap R[X] S)
  have disj : Disjoint (pc : Set R[X]) (p : Set R[X]) := by
    simpa [pc, q] using! Set.disjoint_image_left.mpr
      (Set.disjoint_compl_left_iff_subset.mpr (fun _ a ↦ a))
  have : pS.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint pc _ _ ‹_› disj
  have : IsLocalization.AtPrime (Localization.AtPrime pS) p := by
    convert IsLocalization.isLocalization_isLocalization_atPrime_isLocalization pc
      (Localization.AtPrime pS) pS
    exact (IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj).symm
  have := isRegularRing_iff.mp ‹_› q
  have eq : comap C pS = maximalIdeal (Localization.AtPrime q) := by
    rw [← IsLocalization.map_under q.primeCompl _ (comap C pS),
      ← IsLocalization.map_under q.primeCompl _ (maximalIdeal (Localization.AtPrime q))]
    simp only [comap_comap, S, pS]
    rw [← Polynomial.algebraMap_eq (R := Localization.AtPrime q),
      ← IsScalarTower.algebraMap_eq R (Localization.AtPrime q) (Localization.AtPrime q)[X],
      IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime q)[X], ← comap_comap,
      ← Ideal.under_def R[X], IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj]
    simp [q, IsLocalization.AtPrime.under_maximalIdeal (Localization.AtPrime q) q]
  have := isRegularLocalRing_localization_atPrime_of_comap_eq_maximalIdeal _ pS eq
  exact IsRegularLocalRing.of_ringEquiv (IsLocalization.algEquiv p.primeCompl
    (Localization.AtPrime pS) (Localization.AtPrime p)).toRingEquiv

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact

Goal state before:
pp: case refine_4
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(↑R (LinearMap.baseChange S g))

Tactic:
exact LinearMap.lTensor_surjective S surj₁

Goal state after:
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
x y : ↥(integralClosure (↥v.valuationSubring) L)
⊢ ↑⟨(algebraMap L E) ↑(x + y), ⋯⟩ = ↑(⟨(algebraMap L E) ↑x, ⋯⟩ + ⟨(algebraMap L E) ↑y, ⋯⟩)

Tactic:
simp only [map_add, Subalgebra.coe_add]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)) =
    ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n)

Tactic:
by
      rw [commutes_symm, RingHom.comp_assoc]

Goal state after:
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n + 1] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

Tactic:
iterate_verschiebung_mul

Goal state after:
case succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ b.coeff 0 ≠ 0

Tactic:
contrapose hc
    simp [hc, zero_pow <| pow_ne_zero _ hp.out.ne_zero]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk ↑{k | p k}

Tactic:
rw [count_eq_card_fintype, ← Cardinal.mk_fintype]
  exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
n₁ n₂ : ℕ
⊢ o * ↑(n₂ + n₁) = o * (↑n₂ + ↑n₁)

Tactic:
Nat.cast_add

Goal state after:
case refine_2
o : Ordinal.{u_1}
n₁ n₂ : ℕ
⊢ o * (↑n₂ + ↑n₁) = o * (↑n₂ + ↑n₁)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : f (lfpApprox f x a) = lfpApprox f x a
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
induction b using WellFoundedLT.induction with | ind b IH
   =>  _ 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
⊢ lfpApprox f x b = lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : o < b ^ e
⊢ (coeff b o) e = 0

Tactic:
apply coeff_of_notMem_CNF
  intro he
  rw [mem_map] at he
  obtain ⟨⟨e, c⟩, he, rfl⟩ := he
  obtain rfl | he' := eq_or_ne e 0
  · simp_all
  · exact (opow_le_of_le_log he' (fst_le_log he)).not_gt h

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

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ∀ i_1 < i, f (lfpApprox f x i_1) ≤ a

Tactic:
← ha.eq

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ∀ i_1 < i, f (lfpApprox f x i_1) ≤ f a
Module: Mathlib.Topology.Order.SuccPred

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

Tactic:
· simp [nhds_eq_pure.2 ho', ho, ho']

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

Goal state before:
pp: case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
simp only [h] at this
      exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

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

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

Tactic:
by
  simpa using veblenWith_add_one hf 0

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < f b

Tactic:
exact hp.trans_le (hf.monotone zero_le)

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

Goal state before:
pp: x x' y : ZFSet.{u_1}
⊢ ∀ ⦃b₂ : ZFSet.{u_1}⦄, x.pair y = x'.pair b₂ → x = x' ∧ y = b₂

Tactic:
y'

Goal state after:
x x' y y' : ZFSet.{u_1}
⊢ x.pair y = x'.pair y' → x = x' ∧ y = y'
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
· simp_rw [mem_range_veblen h, veblen_opow_eq_opow_iff]
      exact fun o ↦ veblen_eq_of_lt_invVeblen₁

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

Goal state before:
pp: x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
intro _

Goal state after:
x y✝ : PSet.{u_1}
⊢ (∃ z ∈ x, y✝ ∈ z) → y✝.rank < x.rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : PSet.{u_1}
a✝ : z ∈ x
⊢ ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x

Tactic:
intro _

Goal state after:
x z : PSet.{u_1}
a✝ : z ∈ x
z✝ : PSet.{u_1}
⊢ z✝ ∈ z → z✝ ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
intro _

Goal state after:
case a.h₁
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ x → x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
intro _

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
intro _

Goal state after:
x y✝ : ZFSet.{u_1}
⊢ (∃ z ∈ x, y✝ ∈ z) → y✝.rank < x.rank
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
intro _

Goal state after:
x z : ZFSet.{u_1}
a✝ : z ∈ x
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ z → x✝ ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : ZFSet.{u}
⊢ Function.Injective fun x ↦ ⟨↑x, ⋯⟩

Tactic:
intro _

Goal state after:
x a₁✝ : ZFSet.{u}
⊢ ∀ ⦃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 : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
⊢ z ∈ m → z ∈ x

Tactic:
hzm

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 : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
⊢ z ∈ 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 : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
⊢ (fun x ↦ f (c - x⁻¹)) = f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv

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:
· ext
    simp [AddGroupWithOne.sub_eq_add_neg]

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
⊢ Tendsto f (𝓝[<] c) l
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : FriendlyOperation op₁
h₂ : FriendlyOperation op₂
P : Option α → Prop
inst✝ : DecidablePred P
⊢ FriendlyOperation fun s ↦ if P s.head then op₁ s else op₂ s

Tactic:
rw [friendlyOperation_iff_dist_le_dist] at h₁ h₂ ⊢

Goal state after:
α : 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 α), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ LipschitzWith 2⁻¹ F

Tactic:
· exact h

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

Goal state before:
pp: case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr + ↑m)

Tactic:
rw [← pow_succ, ← opow_natCast, ← opow_natCast]

Goal state after:
case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ ↑(k + 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
γ : Type u_1
γ' : Type u_2
g : γ' → γ
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperationClass op
⊢ FriendlyOperationClass fun c ↦ op (g c)

Tactic:
have : Seq.FriendlyOperationClass (fun c ↦ op (g c)) := Seq.FriendlyOperationClass.comp _ _
  constructor

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

Goal state before:
pp: case cons.cons
hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_length : (hd :: tl).length = (basis_tl_hd :: basis_tl_tl).length
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
⊢ Majorized (toFun (hd :: tl) (basis_tl_hd :: basis_tl_tl)) basis_hd 0

Tactic:
simp only [List.length_cons, Nat.add_right_cancel_iff, toFun_cons] at h_length ⊢

Goal state after:
case cons.cons
hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
⊢ Majorized (basis_tl_hd ^ hd * toFun tl basis_tl_tl) basis_hd 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
basis_tl : Basis
hlo : ∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ toLogFun (e :: es) basis_tl =o[atTop] (log ∘ basis_hd)

Tactic:
cases basis_tl with
    | nil =>
      simp only [toLogFun_nil_basis]
      exact Asymptotics.isLittleO_zero _ _
    | cons b bs =>
      exact (IsLittleO.const_mul_left (hlo b (by simp)) e).add (ih (by grind))

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

Goal state before:
pp: left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.toFun (left ++ right) =o[atTop] t2'.toFun (left ++ right)

Tactic:
apply isLittleO_of_lt_exps h_basis

Goal state after:
case h1
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t1.unit = List.length (left ++ right)

case h2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t2'.unit = List.length (left ++ right)

case h_coef2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.coef ≠ 0

case h_lt
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.unit < t2'.unit
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.toFun (left ++ right) =o[atTop] t1.toFun (left ++ right)

Tactic:
apply isLittleO_of_lt_exps h_basis

Goal state after:
case h1
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t2'.unit = List.length (left ++ right)

case h2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t1.unit = List.length (left ++ right)

case h_coef2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.coef ≠ 0

case h_lt
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.unit < t1.unit
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq = Multiseries.nil
⊢ ms.IsZero

Tactic:
convert IsZero.nil ms.toFun

Goal state after:
case e'_2
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq = Multiseries.nil
⊢ ms = mk Multiseries.nil ms.toFun