mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : K
H : (valuation K (maximalIdeal A)) x ≤ 1
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
by
  obtain ⟨π, hπ⟩ := exists_irreducible A
  obtain ⟨a, b, hb, h_frac⟩ := IsFractionRing.div_surjective A x
  by_cases ha : a = 0
  · rw [← h_frac]
    use 0
    rw [ha, map_zero, zero_div]
  · rw [← h_frac] at H
    obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible ha hπ
    obtain ⟨m, w, rfl⟩ := eq_unit_mul_pow_irreducible (nonZeroDivisors.ne_zero hb) hπ
    replace hb := (mul_mem_nonZeroDivisors.mp hb).2
    rw [mul_comm (w : A) _, map_mul _ (u : A) _, map_mul _ _ (w : A), div_eq_mul_inv, mul_assoc,
      Valuation.map_mul, Integers.one_of_isUnit' u.isUnit (valuation_le_one _), one_mul,
      mul_inv, ← mul_assoc, Valuation.map_mul, map_mul, map_inv₀, map_inv₀,
      Integers.one_of_isUnit' w.isUnit (valuation_le_one _), inv_one, mul_one, ← div_eq_mul_inv,
      ← map_div₀, ← IsFractionRing.mk'_mk_eq_div hb,
      valuation_of_mk', map_pow, map_pow] at H
    have h_mn : m ≤ n := by
      have v_π_lt_one := (intValuation_lt_one_iff_dvd (maximalIdeal A) π).mpr
          (dvd_of_eq ((irreducible_iff_uniformizer _).mp hπ))
      have v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0 := intValuation_ne_zero _ _ hπ.ne_zero
      zify
      rw [← WithZero.coe_one, div_eq_mul_inv, ← zpow_natCast, ← zpow_natCast, ← ofAdd_zero,
        ← zpow_neg, ← zpow_add₀ v_π_ne_zero, ← sub_eq_add_neg] at H
      rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]
    use u * π ^ (n - m) * w.2
    simp only [← h_frac, Units.inv_eq_val_inv, _root_.map_mul, _root_.map_pow, map_units_inv,
      mul_assoc, mul_div_assoc ((algebraMap A _) ↑u) _ _]
    congr 1
    rw [div_eq_mul_inv, mul_inv, mul_comm ((algebraMap A _) ↑w)⁻¹ _, ←
      mul_assoc _ _ ((algebraMap A _) ↑w)⁻¹]
    congr
    rw [pow_sub₀ _ _ h_mn]
    apply IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
    rw [mem_nonZeroDivisors_iff_ne_zero]
    exact hπ.ne_zero

Goal state after:
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 Γ₀
⊢ ∀ (s : Set K), IsClosed[hv.toTopologicalSpace] s → s.Nonempty → IsClosed (⇑v.restrict '' s)

Tactic:
intro U

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
⊢ IsClosed[hv.toTopologicalSpace] U → U.Nonempty → IsClosed (⇑v.restrict '' U)
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 Γ₀
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
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
c : Continuous fun x ↦ x * x₀⁻¹
⊢ (fun x ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀

Tactic:
exact c.continuousAt V'_in

Goal state after:
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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ 0 ∈ {x | v x < ↑γ} ∧ ↑0 = 0

Tactic:
simp only [mem_ofPred_eq, Valuation.map_zero, Units.zero_lt, true_and]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ ↑0 = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

Tactic:
simp only [(Valuation.zero_iff _).mp h, mem_ofPred_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]
      apply subset_closure
      exact ⟨0, by simp only [mem_ofPred_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ Commute φ ((monomial n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a

Tactic:
by
  rw [commute_iff_eq, MvPowerSeries.ext_iff]
  refine ⟨fun h m => ?_, fun h m => ?_⟩
  · have := h (m + n)
    rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this
  · rw [coeff_mul_monomial, coeff_monomial_mul]
    split_ifs <;> [apply h; rfl]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0

Tactic:
split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0

case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
⊢ 0 * b = a * b

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0

case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : σ
⊢ (map f) (X s) = X s

Tactic:
simp [MvPowerSeries.X]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
· exact h_dvd_xy

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
⊢ (coeff n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) φ

Tactic:
have h₁ (i : ℕ) : Function.const ℕ φ i = φ := rfl

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
⊢ (coeff n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ.inr
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'

pp: case inr.succ.inr
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'
⊢ n' > 0

Tactic:
· conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]
            move_mul [← constantCoeff φ ^ (n' - 1)]
            conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
            rw [← pow_add (a := constantCoeff φ)]
            conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']
            ring

Goal state after:
case inr.succ.inr
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'
⊢ n' > 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤

Tactic:
lt_top_iff_ne_top,

Goal state after:
case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} ≠ ⊤
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ eval₂ PowerSeries.C PowerSeries.X φ = ↑φ

Tactic:
by
  nth_rw 2 [← eval₂_C_X (p := φ)]
  rw [← coeToPowerSeries.ringHom_apply, eval₂_eq_sum_range, eval₂_eq_sum_range, map_sum]
  apply Finset.sum_congr rfl
  intros
  rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]

Goal state after:
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 Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
hγ : γ ≠ 0
r : hat K
hr : v r = γ
⊢ ¬(restrict₀ (ofClass v)) r = 0

Tactic:
← embedding_inj,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
hγ : γ ≠ 0
r : hat K
hr : v r = γ
⊢ ¬embedding ((restrict₀ (ofClass v)) r) = embedding 0
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x ↦ f i) = f

Tactic:
ext i

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x ↦ f i) i = f i
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
lt_top_iff_ne_top,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (⨅ l, ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ (truncTotal n) ↑p = p ↔ p.totalDegree < n

Tactic:
by
  rw [truncTotal, truncFinset_coe_eq_self_iff, Set.Finite.subset_toFinset,
    MvPolynomial.totalDegree, Finset.sup_lt_iff (bot_lt_iff_ne_bot.mpr h), Set.subset_def]
  simp [degree, sum]

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

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
⊢ f = (weightedHomogeneousComponent w p) f → IsWeightedHomogeneous w f p

Tactic:
intro hf
    rw [hf]
    exact isWeightedHomogeneous_weightedHomogeneousComponent w f p

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ Tendsto f u (𝓝 g) ↔ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f i)) u (𝓝 ((coeff d) g))

Tactic:
by
  rw [nhds_pi, tendsto_pi]
  exact forall_congr' (fun d => Iff.rfl)

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ eval₂ G s ((trunc 0) f) = ∑ i ∈ range 0, G ((coeff i) f) * s ^ i

Tactic:
rw [trunc_zero', range_zero, sum_empty, eval₂_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
⊢ (trunc 1) p = Polynomial.C ((coeff 0) p)

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i : ℕ
⊢ ((trunc 1) p).coeff i = (Polynomial.C ((coeff 0) p)).coeff i
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
⊢ (trunc 1) p = Polynomial.C ((coeff 0) p)

Tactic:
by
  ext i; simp +contextual [coeff_trunc, Polynomial.coeff_C]

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

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

Tactic:
ext i

Goal state after:
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
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

Tactic:
ext i

Goal state after:
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
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
φ ψ : R⟦X⟧
⊢ (trunc n) (φ - ψ) = (trunc n) φ - (trunc n) ψ

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
φ ψ : R⟦X⟧
i : ℕ
⊢ ((trunc n) (φ - ψ)).coeff i = ((trunc n) φ - (trunc n) ψ).coeff i
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ f.order.toNat * f.divXPowOrder * (X ^ g.order.toNat * g.divXPowOrder) =
    f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat)

Tactic:
by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg : g ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
uv : (σ →₀ ℕ) × (σ →₀ ℕ)
huv : uv ∈ Finset.antidiagonal e
⊢ (coeff uv.1) f * (coeff uv.2) g ∈ Jd.1

Tactic:
exact TwoSidedIdeal.mul_mem_left _ _ _
        (hg _ (le_trans (Finset.HasAntidiagonal.antidiagonal.snd_le huv) he))

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

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
this : UniformSpace S := ⊥
⊢ HasSubst fun x ↦ 0

Tactic:
simpa [hasSubst_iff_hasEval_of_discreteTopology] using! HasEval.zero

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (coeff e) ((map (algebraMap R S)) f) = (coeff e) (subst X f)

Tactic:
rw [coeff_map, coeff_subst HasSubst.X f e, finsum_eq_single _ e]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (coeff e) f • (coeff e) (e.prod fun s e ↦ X s ^ e)

σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ e → (coeff x) f • (coeff e) (x.prod fun s e ↦ X s ^ e) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos
σ : 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
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent ((algebraMap R S) ((coeff 0) f))

Tactic:
simpa using IsNilpotent.map hf (algebraMap R S)

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 =
    0

Tactic:
Function.extend_apply',

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ 0 (a, b).2 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 = 0

case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ ¬∃ a_1, q ^ a_1 = (a, b).2
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

Tactic:
Function.extend_apply',

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ 0 (a, b).1 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 = 0

case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ ¬∃ a_1, q ^ a_1 = (a, b).1
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 =
    0

Tactic:
Function.extend_apply',

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ 0 (a, b).2 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 = 0

case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ ¬∃ a_1, q ^ a_1 = (a, b).2
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

Tactic:
Function.extend_apply',

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ 0 (a, b).1 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 = 0

case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ ¬∃ a_1, q ^ a_1 = (a, b).1