mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
⊢ HasGoodReduction R W ↔ (reduction R W).IsElliptic

Tactic:
refine Iff.trans ?_ (W.reduction R).isElliptic_iff.symm
  simp only [reduction, map_Δ, isUnit_iff_ne_zero, ne_eq, residue_eq_zero_iff]
  have h :
      ¬(valuation K (maximalIdeal R) (algebraMap R K (integralModel R W).Δ) < 1)
      ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R :=
    not_iff_not.mpr <| valuation_lt_one_iff_mem _ _
  refine ((integralModel_Δ_eq R W ▸ hasGoodReduction_iff _ _).trans ?_).trans h
  simpa [hW] using (valuation_le_one (R := R) (K := K) _ _).ge_iff_eq.symm

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

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ (coeff (i, j).1) p * (coeff (i, j).2) (X ^ n) = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Goal state after:
case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff x.1) p * (coeff x.2) (X ^ n) = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Goal state after:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff n) ((rescale 0) x) = (coeff n) ((C.comp constantCoeff) x)

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk,
    coeff_C]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) =
    if n = 0 then constantCoeff x else 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : s = t
⊢ (m - single s n + single s n) t = m t

Tactic:
subst t

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
⊢ (m - single s n + single s n) s = m s
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s = 0
⊢ (coeff m) φ = 0

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s < 1
⊢ (coeff m) φ = 0

Tactic:
· exact h m (hm.symm ▸ zero_lt_one)

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s < 1
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
lhs; arg 2; rw [mul_comm, ← mul_assoc]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ * (↑n' * (coeff 1) φ) * constantCoeff φ ^ (n' - 1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = f ^ #(range n)

Tactic:
card_range

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = f ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∏ i ∈ range n, (coeff (k i)) f = 0

Tactic:
rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ (∏ x ∈ range n \ s, (coeff (k x)) f) * ∏ x ∈ s, (coeff (k x)) f = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ m + #(range n \ {i ∈ range n | k i = 0}) ≤ #(range n)

Tactic:
card_range

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ m + #(range n \ {i ∈ range n | k i = 0}) ≤ n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
⊢ (if x : 0 = 0 then ⊤ else ↑(Nat.find ⋯)) = ⊤

Tactic:
dif_pos rfl

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case ind
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ k.succ) = (coeff x) (p ^ k.succ)

Tactic:
simp_rw [Nat.succ_eq_add_one, pow_add, pow_one, MvPolynomial.coeff_mul, coeff_mul]

Goal state after:
case ind
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
⊢ ∑ x ∈ antidiagonal x, MvPolynomial.coeff x.1 ((truncTotal n) p ^ k) * MvPolynomial.coeff x.2 ((truncTotal n) p) =
    ∑ p_1 ∈ antidiagonal x, (coeff p_1.1) (p ^ k) * (coeff p_1.2) p
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)

Tactic:
induction m using Nat.caseStrongRecOn generalizing x with
  | zero => grind [coeff_one, MvPolynomial.coeff_one]
  | ind k ih =>
    simp_rw [Nat.succ_eq_add_one, pow_add, pow_one, MvPolynomial.coeff_mul, coeff_mul]
    congr! 2 with _ _
    · exact ih _ k.le_refl (by grind [mem_antidiagonal])
    · exact coeff_truncTotal _ (by grind [mem_antidiagonal])

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
⊢ (coeff d) (f + g) ≠ 0 → (weight w) d = p

Tactic:
by
  rw [not_imp_comm]
  intro hd
  rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst✝⁵, inst✝²] ⇑φ
a : R
ha : Tendsto (fun x ↦ a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ φ a ^ x) atTop (𝓝 0)

Tactic:
← map_pow

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst✝⁵, inst✝²] ⇑φ
a : R
ha : Tendsto (fun x ↦ a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ φ (a ^ x)) atTop (𝓝 0)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = MvPowerSeries.order φ

Tactic:
refine eq_of_le_of_ge ?_ ?_
  · refine MvPowerSeries.le_order fun d hd => by
      have : coeff ↑(Finsupp.degree d) φ = 0 := coeff_of_lt_order _ hd
      have eq_aux : d.degree = d () := Finset.sum_eq_single _ (by simp) (by simp)
      exact (PowerSeries.coeff_def rfl (R := R)) ▸ (eq_aux ▸ this)
  · refine le_order φ (MvPowerSeries.order φ) fun i hi => by
      rw [← Finsupp.degree_single () i] at hi
      exact MvPowerSeries.coeff_of_lt_order hi

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
⊢ Multipliable fun n ↦ 1 + -X ^ (n + 1)

Tactic:
apply multipliable_one_add_of_tendsto_order_atTop_nhds_top

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
⊢ Tendsto (fun i ↦ (-X ^ (i + 1)).order) atTop (𝓝 ⊤)
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : UniformSpace S
φ : R →+* S
a : σ → S
r : R
⊢ MvPolynomial.eval₂ φ a (MvPolynomial.C r) = φ r

Tactic:
MvPolynomial.eval₂_C

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : UniformSpace S
φ : R →+* S
a : σ → S
r : R
⊢ φ r = φ r
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
⊢ subst a ↑p = (MvPolynomial.aeval a) p

Tactic:
let : UniformSpace R := ⊥

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this : UniformSpace R := ⊥
⊢ subst a ↑p = (MvPolynomial.aeval a) p
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
⊢ ⇑(substAlgHom ha) = subst a

Tactic:
let : UniformSpace R := ⊥

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
this : UniformSpace R := ⊥
⊢ ⇑(substAlgHom ha) = subst a
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
⊢ ⇑(substAlgHom ⋯) = id

Tactic:
let : UniformSpace R := ⊥

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
this : UniformSpace R := ⊥
⊢ ⇑(substAlgHom ⋯) = id
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
e : τ →₀ ℕ
⊢ (coeff e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ a s ^ e)

Tactic:
let : UniformSpace R := ⊥

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this : UniformSpace R := ⊥
⊢ (coeff e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ a s ^ e)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
⊢ (AlgHom.restrictScalars R (substAlgHom hb)).comp (substAlgHom ha) = substAlgHom ⋯

Tactic:
let : UniformSpace R := ⊥

Goal state after:
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this : UniformSpace R := ⊥
⊢ (AlgHom.restrictScalars R (substAlgHom hb)).comp (substAlgHom ha) = substAlgHom ⋯
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬(coeff i) f = 0
⊢ (⨅ i, (order ∘ a) i) * ↑(Finsupp.degree i) ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i

Tactic:
· simp only [Function.comp_apply, order, Finsupp.degree, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
      Nat.cast_sum, Finset.mul_sum, Finsupp.weight_apply, nsmul_eq_mul]
    exact Finset.sum_le_sum fun j hj => by
      simp [mul_comm, mul_le_mul_right (iInf_le_iff.mpr fun _ a ↦ a j)]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ ≤ C * ((↑n ^ (s + (1 - ↑x)).re)⁻¹ * ↑n ^ s.re)

Tactic:
← Real.rpow_neg <| Nat.cast_nonneg _,

Goal state after:
case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ ≤ C * (↑n ^ (-(s + (1 - ↑x)).re) * ↑n ^ s.re)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
F : Filter ι
g : ArithmeticFunction R
⊢ Tendsto f F (nhds g) ↔ ∀ (n : ℕ), ∀ᶠ (i : ι) in F, (f i) n = g n

Tactic:
let : UniformSpace R := ⊥

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
F : Filter ι
g : ArithmeticFunction R
this : UniformSpace R := ⊥
⊢ Tendsto f F (nhds g) ↔ ∀ (n : ℕ), ∀ᶠ (i : ι) in F, (f i) n = g n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ CompleteSpace (ArithmeticFunction R)

Tactic:
let : UniformSpace R := ⊥

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
⊢ CompleteSpace (ArithmeticFunction R)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
⊢ ∀ (n : ℕ), ∀ᶠ (s : Finset ι) in atTop, (∏ i ∈ s, f i) n = (eulerProduct f) n

Tactic:
let : UniformSpace R := ⊥

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this : UniformSpace R := ⊥
⊢ ∀ (n : ℕ), ∀ᶠ (s : Finset ι) in atTop, (∏ i ∈ s, f i) n = (eulerProduct f) n
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ₑ ≠ 0 ∨ egauge 𝕜 s x ≠ 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
⊢ rescaleAlgHom 1 = AlgHom.id R (MvPowerSeries σ R)

Tactic:
by
  ext1 f
  simp [rescaleAlgHom, subst_self]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
x : ℕ → MvPowerSeries σ R
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ (substAlgHom ha) (∑' (i : ℕ), x i) = ∑' (i : ℕ), (substAlgHom ha) (x i)

Tactic:
substAlgHom_eq_aeval ha,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
x : ℕ → MvPowerSeries σ R
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ (aeval ⋯) (∑' (i : ℕ), x i) = ∑' (i : ℕ), (aeval ⋯) (x i)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : y ∈ closedBall 0 ↑r
⊢ ‖(fun x ↦ c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
rw [mem_closedBall_zero_iff, ← coe_nnnorm, NNReal.coe_le_coe] at hy

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖(fun x ↦ c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
x✝ : ℕ
⊢ (x✝ ∈ Function.support fun d ↦ (coeff d) P * if d = 1 then k else 0) → x✝ ∈ {1}

Tactic:
by simp +contextual

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

Goal state before:
pp: R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ (substAlgHom ha) (∑' (i : ℕ), x i) = ∑' (i : ℕ), (substAlgHom ha) (x i)

Tactic:
substAlgHom_eq_aeval ha,

Goal state after:
R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ (aeval ⋯) (∑' (i : ℕ), x i) = ∑' (i : ℕ), (aeval ⋯) (x i)
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
this : 𝓝[s \ {x}] x = 𝓝[t \ {x}] x
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' (t \ {x}) x

Tactic:
by simp only [HasFDerivWithinAt, this]

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: a : ℝ
⊢ (interior (Iic a)).Nonempty

Tactic:
by simp only [interior_Iic, nonempty_Iio]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun x ↦ c) s x = 0

Tactic:
rw [fderivWithin, if_pos]

Goal state after:
case hc
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
x : E
s : Set E
c : F
⊢ HasFDerivWithinAt (fun x ↦ c) 0 s x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ f =o[𝕜; l] g ↔
    ∀ (i : ιE),
      pE i → ∃ j, pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)

Tactic:
rw [isLittleOTVS_iff]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE),
      pE i → ∃ j, pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousNeg E
h : (-f) =O[𝕜; l] g
⊢ f =O[𝕜; l] g

Tactic:
simpa using h.neg_left

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousNeg E
h : (-f) =o[𝕜; l] g
⊢ f =o[𝕜; l] g

Tactic:
simpa using h.neg_left

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
g : α → F
inst✝ : ContinuousNeg E
f₁ f₂ : α → E
h : (f₁ - f₂) =o[𝕜; l] g
⊢ (f₂ - f₁) =o[𝕜; l] g

Tactic:
simpa using h.neg_left

Goal state after: