mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ
n : ℕ
ih :
  ∀ (x : ℝ),
    deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
x : ℝ
⊢ deriv^[n + 1] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Tactic:
replace ih : deriv^[n] _ = _ := _root_.funext ih
    have deriv_gaussian :
      deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [mul_comm, ← neg_mul]`
      rw [deriv_exp (by simp)]
      simp [mul_comm]
    rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ),
      deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
    · ring
    · apply Polynomial.differentiable_aeval
    · apply DifferentiableAt.exp; simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > (p * (1 - X)).natDegree,
    (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
intro n hn

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n k : ℕ
⊢ ∑ b ∈ range (n + 1), (C ((-1) ^ b * ↑(n.choose b) * ↑((n + b).choose n)) * X ^ b).coeff k =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)

Tactic:
coeff_C_mul_X_pow

Goal state after:
n k : ℕ
⊢ (∑ x ∈ range (n + 1), if k = x then (-1) ^ x * ↑(n.choose x) * ↑((n + x).choose n) else 0) =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_2
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R N) (f.toFun' R (1 ⊗ₜ[R] x)) =
    (rTensor N (Algebra.algHom R R S).toLinearMap) (f.toFun' R (1 ⊗ₜ[R] x))

Tactic:
simp only [includeRight_lid]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ s + -(g * ↑⋯.unit⁻¹ * s₁) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
g.eq_X_pow_mul_shift_add_trunc n

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ s + -(((X ^ n * mk fun i ↦ (coeff (i + n)) g) + ↑((trunc n) g)) * ↑⋯.unit⁻¹ * s₁) =
    ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
n : ℕ
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L n)
⊢ HasProjectiveDimensionLT M n

Tactic:
by
  induction n generalizing M with
  | zero =>
    have : Subsingleton (M ⟶ M) := Ext.homEquiv₀.subsingleton_congr.mp (h M ‹_›)
    have : Limits.IsZero M := (Limits.IsZero.iff_id_eq_zero M).mpr (Subsingleton.eq_zero (𝟙 M))
    exact this.hasProjectiveDimensionLT_zero
  | succ n hn =>
    rcases Module.exists_finite_presentation R M with ⟨_, _, _, _, _, f, surjf⟩
    let S : ShortComplex (ModuleCat.{v} R) := f.shortComplexKer
    have hS : S.ShortExact := LinearMap.shortExact_shortComplexKer surjf
    match n with
    | 0 =>
      simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
      have : Subsingleton (Ext M S.X₁ 1) := h S.X₁ inferInstance
      rcases Ext.covariant_sequence_exact₃ M hS (Ext.mk₀ (𝟙 M)) (zero_add 1)
        (Subsingleton.eq_zero _) with ⟨f', hf'⟩
      rcases (Ext.mk₀_bijective M S.X₂).2 f' with ⟨f, hf⟩
      rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'
      exact (Retract.mk f S.g hf').projective
    | n + 1 =>
      rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]
      have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr
      apply hn S.X₁
      simpa [this] using h

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ ↑f * h * g' = ↑(f * f') * (h * h')

Tactic:
H'.eq_mul,

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ ↑f * h * (↑f' * h') = ↑(f * f') * (h * h')
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
i : Fin (n + 1)
⊢ TruncatedWittVector.coeff i (truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂)))) =
    TruncatedWittVector.coeff i fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p

Tactic:
simp only [WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP]

Goal state after:
case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
i : Fin (n + 1)
⊢ (mk p (frobeniusRotationCoeff p ha₁ ha₂)).coeff ↑i ^ p =
    TruncatedWittVector.coeff i fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
ha : a ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * a = ↑p ^ m * b

Tactic:
revert ha

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ a ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * a = ↑p ^ m * b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b

pp: case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
· intro h_eq; rw [Subtype.coe_inj] at h_eq; exact h_nab h_eq

Goal state after:
case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : y ∈ ⋃₀ mk α A
a : (mk α A).Type
c : ((mk α A).Func a).Type
e : y.Equiv ((A a).Func c)
this : (A a).Func c ∈ mk (A a).Type (A a).Func
⊢ (A a).Func c ∈ A (?m.126 α A y x✝ a c e this)

Tactic:
by rwa [eta] at this

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
⊢ 0 < veblenWith f o a

Tactic:
have H (b) : 0 < veblenWith f 0 b := by
    rw [veblenWith_zero]
    exact hp.trans_le (hf.monotone zero_le)

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f o a
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
⊢ (mk α✝ A).rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o

Tactic:
refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩
    rw [succ_le_iff]
    exact h (Mem.mk A a)

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

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

Tactic:
by
  contrapose!; exact rank_le_iff

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

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ (veblen o a).invVeblen₁ ≤ o

Tactic:
← lt_veblen_iff_invVeblen₁_le,

Goal state after:
case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a < veblen o (veblen o a)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₁ ≤ 0

Tactic:
← lt_veblen_iff_invVeblen₁_le,

Goal state after:
a : Ordinal.{u}
h : a < ω ^ a
⊢ a < veblen 0 a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: ⊢ invVeblen₂ 0 = 0

Tactic:
apply invVeblen₂_of_lt_opow
  simp

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

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

Tactic:
by
  contrapose!; exact rank_le_iff

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

Goal state before:
pp: x : ZFSet.{u}
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x

Tactic:
induction x using inductionOn with | _ x ih

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

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
obtain ⟨x, xe⟩ := Nat.exists_eq_succ_of_ne_zero n₂.ne_zero
      simp only [Mul.mul, mul, e0, ↓reduceIte, repr, repr_zero, PNat.mul_coe, natCast_mul,
        opow_zero, one_mul]
      simp only [xe, h₂.zero_of_zero e0, repr_zero, add_zero]
      rw [Nat.cast_add_one x, add_mul_add_one _ ao, mul_assoc]

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a : A
h : IsNat a 0
⊢ a = 0

Tactic:
have := h.out

Goal state after:
A : Type u_2
sA : CommSemiring A
a : A
h : IsNat a 0
this : a = ↑0
⊢ a = 0
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
grw [le_succ b, succ_eq_add_one, add_mul_succ _ (one_add_of_omega0_le h)]
    · gcongr
      · exact omega0_pos
      · exact succ_le_iff.2 <| by gcongr; exact isSuccLimit_omega0.succ_lt l
    · exact omega0_pos

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

Goal state before:
pp: case hl
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f) =ᶠ[atTop] fun x ↦ (g ^ b) x / (f ^ a) x

pp: case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Tendsto (Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f)) atTop atTop

Tactic:
· refine (hf.and (hg.eventually_gt_atTop 0)).mono (fun x ⟨hf, hg⟩ ↦ ?_)
    simp [Real.exp_sub, mul_comm a, mul_comm b, Real.exp_mul, Real.exp_log hg, Real.exp_log hf]

Goal state after:
case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Tendsto (Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
m : UnitMonomial
right : Basis
left_hd : ℝ → ℝ
left_tl : List (ℝ → ℝ)
ih : (List.replicate left_tl.length 0 ++ m).toFun (left_tl ++ right) = m.toFun right
⊢ (List.replicate (left_hd :: left_tl).length 0 ++ m).toFun (left_hd :: left_tl ++ right) = m.toFun right

Tactic:
| cons left_hd left_tl ih =>

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd ≠ 0
⊢ toLogFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd

Tactic:
simp only [toLogFun_cons]
  apply IsEquivalent.refl.add_isLittleO
  apply IsLittleO.const_mul_right' (isUnit_iff_ne_zero.mpr h_nonzero)
  have hlo : ∀ b ∈ basis_tl, (Real.log ∘ b) =o[atTop] (Real.log ∘ basis_hd) :=
    fun b hb => h_basis.tail_isLittleO_head hb
  clear h_basis
  induction exps_tl generalizing basis_tl with
  | nil =>
    simp only [toLogFun_nil]
    exact Asymptotics.isLittleO_zero _ _
  | cons e es ih =>
    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: case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                    UnitMonomial.toFun exps_tl basis_tl := by
          ext x; simp [UnitMonomial.toFun, h.left]

Goal state after:
case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)

Tactic:
have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                    UnitMonomial.toFun exps_tl basis_tl := by
          ext x; simp [UnitMonomial.toFun, h.left]

Goal state after:
case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.right.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < ↑exp ∧ (Multiseries.cons tl_exp tl_coef tl_tl).Sorted

Tactic:
obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim
  constructor
  · simp only [leadingExp_cons, WithBot.coe_lt_coe]
    exact h_all (tl_exp, tl_coef) (by simp [Multiseries.cons])
  · exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise

Goal state after:
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
have nonneg := emod_nonneg a <| Int.ne_of_gt this

Goal state after:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ jacobiSymNat a b = r

Tactic:
have ha' : legendreSym 2 a = 1 := by
    simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
    decide

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
⊢ jacobiSymNat a b = r
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m : ℕ
⊢ a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m % m * (a % m) % m) % m

Tactic:
Nat.mod_mod,

Goal state after:
a b m : ℕ
⊢ a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m * (a % m) % m) % m
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
· exact hn <| Or.inr <| h₂.1 fun Hc ↦ hn' <| Hc.1 _ h

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
α : Type u_7
l : Filter α
f : α → E
x : E
hB_inj : Function.Injective ⇑B
⊢ Tendsto f l (𝓝 x) ↔ ∀ (y : F), Tendsto (fun i ↦ (B (f i)) y) l (𝓝 ((B x) y))

Tactic:
← tendsto_pi_nhds,

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
α : Type u_7
l : Filter α
f : α → E
x : E
hB_inj : Function.Injective ⇑B
⊢ Tendsto f l (𝓝 x) ↔ Tendsto (fun i ↦ ⇑(B (f i))) l (𝓝 ⇑(B x))
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[TopologicalSpace.coinduced (⇑f) inferInstance, inst✝] g ↔
    Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)

Tactic:
continuous_coinduced_dom

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[inferInstance, inst✝] (g ∘ ⇑f) ↔ Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ (c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
by
  apply Submodule.finsuppSum_mem
  intro m hm
  have hsm := (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)).map_smul
  dsimp at hsm
  rw [hsm]
  apply Submodule.smul_mem
  apply Submodule.subset_span
  have hmas : m.val ≤ as := by
    apply hc
    simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm
  refine ⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a hmas, ?_⟩⟩
  simp only [Products.eval, List.map, List.prod_cons]

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
x✝ y✝ : X.A
F : Ultrafilter X.A
hx : ↑F ≤ 𝓝 x✝
hy : ↑F ≤ 𝓝 y✝
⊢ x✝ = y✝

Tactic:
← str_eq_of_le_nhds _ _ hx,

Goal state after:
X : Compactum
x✝ y✝ : X.A
F : Ultrafilter X.A
hx : ↑F ≤ 𝓝 x✝
hy : ↑F ≤ 𝓝 y✝
⊢ X.str F = y✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective (range_equiv_smaller_toFun C o)

Tactic:
by
  dsimp +unfoldPartialApp [range_equiv_smaller_toFun]
  refine ⟨fun a b hab ↦ ?_, fun ⟨a, b, hb⟩ ↦ ?_⟩
  · ext1
    simp only [Subtype.mk.injEq] at hab
    exact injective_πs C o hab
  · use ⟨b, hb.1⟩
    simpa only [Subtype.mk.injEq] using hb.2

Goal state after: