mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case h
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hγ0 : ↑g ∉ {0}
π : K
hπ : v π = ↑g
⊢ ↑(Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup) ≤ 1 ∧
    ↑(Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup) = ↑(generator v)

Tactic:
exact ⟨le_of_lt (valueGroup (.ofClass v)).genLTOne_lt_one,
    by rw [valueGroup_genLTOne_eq_generator]⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
H : Associated π₁ π₂
⊢ v.IsUniformizer ↑π₂

Tactic:
obtain ⟨u, hu⟩ := H
  have : v (u.1 : K) = 1 := (Integers.isUnit_iff_valuation_eq_one <| integer.integers v).mp u.isUnit
  rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u

Tactic:
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hm₀

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalRing.maximalIdeal A ≠ ⊥

Tactic:
by simpa [ne_eq, ← isField_iff_maximalIdeal_eq] using not_isField A

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
a : K
h : (valuation K (maximalIdeal A)) a = 1
⊢ ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = a

pp: case refine_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
a : K
h : ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = a
⊢ (valuation K (maximalIdeal A)) a = 1

Tactic:
· obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le
    rw [valuation_eq_one_iff_notMem] at h
    simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
      not_not] at h
    use b, h

Goal state after:
case refine_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
a : K
h : ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = a
⊢ (valuation K (maximalIdeal A)) a = 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)

Tactic:
have : ∃ V' ∈ 𝓝 (1 : hat K), (0 : hat K) ∉ V' ∧ ∀ (x) (_ : x ∈ V') (y) (_ : y ∈ V'),
      x * y⁻¹ ∈ V := by
      have : Tendsto (fun p : hat K × hat K => p.1 * p.2⁻¹) ((𝓝 1) ×ˢ (𝓝 1)) (𝓝 1) := by
        rw [← nhds_prod_eq]
        conv =>
          congr
          rfl
          rfl
          rw [← one_mul (1 : hat K)]
        refine
          Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)
        convert! (continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))).tendsto
        exact inv_one.symm
      rcases tendsto_prod_self_iff.mp this V V_in with ⟨U, U_in, hU⟩
      let hatKstar := ({0}ᶜ : Set <| hat K)
      have : hatKstar ∈ 𝓝 (1 : hat K) := compl_singleton_mem_nhds zero_ne_one.symm
      exact ⟨U ∩ hatKstar, Filter.inter_mem U_in this,
        ⟨fun ⟨_, h'⟩ ↦ h' rfl, fun x ⟨hx, _⟩ y ⟨hy, _⟩ ↦ hU _ _  hx hy⟩⟩

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
this : ∃ V' ∈ 𝓝 1, 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ (⇑embedding ∘ extension) 0 = 0

Tactic:
rw [Function.comp_apply, map_eq_zero, ← v.restrict.map_zero (R := K),
      ← Valued.extension_extends (0 : K), Completion.coe_zero]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
by
  rw [← wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete (g := g⁻¹)]
  refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩ <;>
  · intro
    simp [Function.onFun, inv_le']

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

Goal state before:
pp: case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff m) φ = 0

Tactic:
rw [Finsupp.unique_single m]

Goal state after:
case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff (single default (m default))) φ = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ v.intValuation x ≤ 1

Tactic:
· rw [v.intValuation_if_neg hx, ← exp_zero, exp_le_exp, Right.neg_nonpos_iff]
    exact Int.natCast_nonneg _

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

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∑ p ∈ antidiagonal d, (coeff p.1) (f a) * (coeff p.2) (∏ x ∈ s, f x) =
    ∑
      l ∈
        (antidiagonal d).biUnion fun p ↦
          Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach,
      ∏ i ∈ insert a s, (coeff (l i)) (f i)

Tactic:
sum_biUnion

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∑ p ∈ antidiagonal d, (coeff p.1) (f a) * (coeff p.2) (∏ x ∈ s, f x) =
    ∑ x ∈ antidiagonal d,
      ∑ i ∈ Finset.map { toFun := fun f ↦ (↑f).update a x.1, inj' := ⋯ } (s.finsuppAntidiag x.2).attach,
        ∏ i_1 ∈ insert a s, (coeff (i i_1)) (f i_1)

case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (↑(antidiagonal d)).PairwiseDisjoint fun p ↦
    Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R[X]
n : ℕ
⊢ (PowerSeries.coeff n) ↑(φ * ψ) = (PowerSeries.coeff n) (↑φ * ↑ψ)

Tactic:
simp only [coeff_coe, PowerSeries.coeff_mul, coeff_mul]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
this : ∀ (a : A) (f : MvPowerSeries σ R), a • f = MvPowerSeries.C ((algebraMap A R) a) * f
⊢ (e.prod fun s n ↦ (MvPowerSeries.C ((algebraMap A R) (a s)) * MvPowerSeries.X s) ^ n) =
    (e.prod fun s n ↦ a s ^ n) • (MvPowerSeries.monomial e) 1

Tactic:
simp only [mul_pow, Finsupp.prod_mul, ← map_pow, ← MvPowerSeries.monomial_one_eq, this]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
this : ∀ (a : A) (f : MvPowerSeries σ R), a • f = MvPowerSeries.C ((algebraMap A R) a) * f
⊢ (e.prod fun a_1 b ↦ MvPowerSeries.C ((algebraMap A R) (a a_1 ^ b))) * (MvPowerSeries.monomial e) 1 =
    MvPowerSeries.C ((algebraMap A R) (e.prod fun s n ↦ a s ^ n)) * (MvPowerSeries.monomial e) 1
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) (f + g) ≠ 0

Tactic:
rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w H, add_zero]

Goal state after:
case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) f ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑((truncFinset R t) p)) = MvPolynomial.coeff x ((truncFinset R s) p)

Tactic:
by_cases x ∈ s <;> grind [MvPolynomial.coeff_coe]

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
H : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
by
  obtain ⟨n, hn : (n : ℕ∞) = _⟩ := ENat.ne_top_iff_exists.mp (ne_top_of_lt H)
  rw [← hn, weightedOrder_eq_nat]
  obtain ⟨d, hd', hd⟩ := ((weightedOrder_eq_nat w).mp hn.symm).1
  constructor
  · refine ⟨d, ?_, hd⟩
    rw [← hn, ← hd] at H
    rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w H, add_zero]
    exact hd'
  · intro b hb
    suffices weight w b < weightedOrder w f by
      rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w this,
        coeff_eq_zero_of_lt_weightedOrder w (lt_trans this H), add_zero]
    rw [← hn, Nat.cast_lt]
    exact hb

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑p) = MvPolynomial.coeff x p

Tactic:
by_cases x ∈ s <;> grind [MvPolynomial.coeff_coe]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc R n) p)

Tactic:
simp [coeff_trunc]

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

Goal state before:
pp: case refine_1
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w (p.toSubring T hp) ≤ weightedOrder w p

Tactic:
refine le_weightedOrder w fun d hd => by
      simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a✝ b✝ : (ofClass (valuation K v)).ValueGroup₀
a b : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ↑a ≤ (map' ↑(valueGroupEquiv K v)) ↑b ↔ ↑a ≤ ↑b

Tactic:
simp [← Subtype.coe_le_coe]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
⊢ (if (weight w) d = p then (coeff d) f else 0) = (coeff d) 0

Tactic:
split_ifs with hd

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ (coeff d) f = (coeff d) 0

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ 0 = (coeff d) 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
⊢ (coeff d) f = if (weight w) d = p then (coeff d) f else 0

Tactic:
split_ifs with hd

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ (coeff d) f = (coeff d) f

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ (coeff d) f = 0
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 q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
⊢ (if (weight w) d = p + q then (coeff d) (f * g) else 0) =
    (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

Tactic:
split_ifs with hd

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : (weight w) d = p + q
⊢ (coeff d) (f * g) = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ 0 = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ Valued.v ↑r = (valuation K v) ↑r

Tactic:
rw [← adicCompletion.valued_toCompletion]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ Valued.v (↑r).toCompletion = (valuation K v) ↑r
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) } = (valuation K v) k

Tactic:
rw [← adicCompletion.valued_toCompletion]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) }.toCompletion = (valuation K v) k
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
f : R⟦X⟧
i : ℕ
⊢ ((trunc n) (C r * f)).coeff i = (Polynomial.C r * (trunc n) f).coeff i

Tactic:
simp [coeff_trunc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
r : R
i : ℕ
⊢ ((trunc n) (f * C r)).coeff i = ((trunc n) f * Polynomial.C r).coeff i

Tactic:
simp [coeff_trunc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
d n : ℕ
hdn : d < n
⊢ (coeff d) ↑((trunc n) f) = (coeff d) f

Tactic:
by simp [coeff_trunc, hdn]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
⊢ subst X = id

Tactic:
rw [← coe_substAlgHom HasSubst.X]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
⊢ ⇑(substAlgHom ⋯) = id
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : Summable (term f s)
⊢ Summable (term f s')

Tactic:
← summable_norm_iff

Goal state after:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : Summable fun x ↦ ‖term f s x‖
⊢ Summable fun x ↦ ‖term f s' x‖
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ f =O[atTop] fun n ↦ ↑n ^ s.re

Tactic:
obtain ⟨C, hC⟩ := h.le_const_mul_rpow

Goal state after:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
⊢ f =O[atTop] fun n ↦ ↑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
this✝¹ : UniformSpace R := ⊥
this✝ : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
this : ∀ k ≤ n, (∏ x ∈ u \ t, f x) k = (∏ x ∈ v \ t, f x) k
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = ((∏ x ∈ v \ t, f x) * ∏ x ∈ t, f x) n

Tactic:
rw [mul_apply, mul_apply]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝¹ : UniformSpace R := ⊥
this✝ : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
this : ∀ k ≤ n, (∏ x ∈ u \ t, f x) k = (∏ x ∈ v \ t, f x) k
⊢ ∑ x ∈ n.divisorsAntidiagonal, (∏ x ∈ u \ t, f x) x.1 * (∏ x ∈ t, f x) x.2 =
    ∑ x ∈ n.divisorsAntidiagonal, (∏ x ∈ v \ t, f x) x.1 * (∏ x ∈ t, f x) x.2
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) ((rescale a) f) = (coeff n) (subst (a • X) f)

Tactic:
rw [coeff_rescale]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (n.prod fun s m ↦ a s ^ m) * (coeff n) f = (coeff n) (subst (a • X) f)
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 : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m : ℕ
⊢ (coeff n) (P.substInv ^ m) = (coeff n) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ m)

Tactic:
generalize hB : (∑ i : Fin (n + 1), C (substInvFun P ↑i) * X ^ i.1) = B

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
⊢ (coeff n) (P.substInv ^ m) = (coeff n) (B ^ m)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.derivWithin f s x = deriv f x

Tactic:
unfold _root_.derivWithin deriv
  rw [h.fderivWithin hxs]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
f' : 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
x : 𝕜
hx : x ∈ s
⊢ deriv f x = f' x

Tactic:
rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousAdd E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous[inst✝⁵, inst✝⁴] (p.partialSum n)

Tactic:
unfold partialSum

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousAdd E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous[inst✝⁵, inst✝⁴] fun x ↦ ∑ k ∈ Finset.range n, (p k) fun x_1 ↦ 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✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑δ * ↑‖g x‖₊ ≤ ↑δ * egauge 𝕜 (ball 0 1) (g x)

Tactic:
gcongr; apply le_egauge_ball_one

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun n ↦ ‖p n‖ * ↑r ^ n

Tactic:
obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h
  exact .of_nonneg_of_le (fun _ ↦ by positivity)
    hp ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)

Goal state after: