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

Goal state before:
pp: U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
⊢ ↑(map φ f) = (PowerSeries.map φ) ↑f

Tactic:
ext

Goal state after:
U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) ↑(map φ f) = (PowerSeries.coeff n✝) ((PowerSeries.map φ) ↑f)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R[X]
h : ↑x = ↑y
⊢ x = y

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R[X]
h : ↑x = ↑y
n✝ : ℕ
⊢ x.coeff n✝ = y.coeff n✝
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ single () (d ()) = d

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ (single () (d ())) default = d default
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f✝ g f : MvPowerSeries σ R
⊢ ℕ∞

Tactic:
exact dite (f = 0) (fun _ => ⊤) fun h =>
    Nat.find ((ne_zero_iff_exists_coeff_ne_zero_and_weight w).mp h)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
⊢ x = y

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y
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 Γ₀
⊢ Function.Surjective ⇑v ↔ Function.Surjective ⇑v

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v

case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ weightedOrder w f = ↑n →
    (∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ ((∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0) →
    weightedOrder w f = ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (coeff d_1) ((monomial d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0

Tactic:
constructor

Goal state after:
case neg.left
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (coeff d_1) ((monomial d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d

case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : hat K
ha : v a = γ
⊢ ∃ a, v a = γ

pp: case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : K
ha : v a = γ
⊢ ∃ a, v a = γ

Tactic:
· induction a using Completion.induction_on
    · by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
      · simp [H]
      · simp only [H, imp_false]
        rcases eq_or_ne γ 0 with rfl | hγ
        · simp at H
        · obtain ⟨r, hr⟩ := h γ
          have hr' : restrict₀ (.ofClass (valuedCompletion (K := K)).v) r ≠ 0 := by
            rw [ne_eq, ← embedding_inj, embedding_restrict₀ r]
            simpa [hr]
          convert! isClosed_univ.sdiff (isOpen_sphere (hat K) hr') using 1
          ext x
          simp [← hr, ← v.restrict_def, v.restrict_inj]
    · exact ⟨_, by simpa using ha⟩

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : K
ha : v a = γ
⊢ ∃ a, v a = γ
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
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (∃ d, (coeff d) (f + g) ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) (f + g) = 0

Tactic:
constructor

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

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

Goal state before:
pp: σ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R✝
s✝ : Finset (σ →₀ ℕ)
R : Type u_4
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x✝¹ : R
x✝ : MvPowerSeries σ R
⊢ ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) (x✝¹ • x✝)) =
    (RingHom.id R) x✝¹ • ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝)

Tactic:
ext

Goal state after:
σ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R✝
s✝ : Finset (σ →₀ ℕ)
R : Type u_4
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x✝¹ : R
x✝ : MvPowerSeries σ R
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) (x✝¹ • x✝))) =
    MvPolynomial.coeff m✝ ((RingHom.id R) x✝¹ • ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝))
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
⊢ (truncFinset R s) ((monomial x) r) = (MvPolynomial.monomial x) r

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((truncFinset R s) ((monomial x) r)) = MvPolynomial.coeff m✝ ((MvPolynomial.monomial x) r)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
⊢ (truncFinset R s) ((monomial x) r) = 0

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((truncFinset R s) ((monomial x) r)) = MvPolynomial.coeff m✝ 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsBotZeroClass α
inst✝³ : OrderBot α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f : ι →₀ α
⊢ #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
card_Iio_eq_card_Iic_sub_one,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsBotZeroClass α
inst✝³ : OrderBot α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f : ι →₀ α
⊢ #(Iic f) - 1 = ∏ i ∈ f.support, #(Iic (f i)) - 1
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ : (trunc' R m) f = (trunc' R m) g
⊢ (coeff n) f = (coeff n) g

Tactic:
have {f' : MvPowerSeries σ R} : f'.coeff n = (trunc' R m f').coeff n := by
    rw [coeff_trunc', if_pos hm₁]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ : (trunc' R m) f = (trunc' R m) g
this : ∀ {f' : MvPowerSeries σ R}, (coeff n) f' = MvPolynomial.coeff n ((trunc' R m) f')
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a b : ℕ∞
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (a, b)

Tactic:
by
  match a, b, h with
  | (a : ℕ), (b : ℕ), _ => simp [ContinuousAt, nhds_prod_eq]
  | (a : ℕ), ⊤, _ =>
    suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
      simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]
    filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le
  | ⊤, (b : ℕ), _ =>
    suffices ∀ n : ℕ, ∀ᶠ a : ℕ∞ in 𝓝 ⊤, b + n < a by
      simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]
    exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ 1 ≤ f.order ↔ constantCoeff f = 0

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ 1 ≤ f.order → constantCoeff f = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ constantCoeff f = 0 → 1 ≤ f.order
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:
by
  classical
  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 : MvPowerSeries σ R
p : ℕ
⊢ IsWeightedHomogeneous w f p ↔ f = (weightedHomogeneousComponent w p) f

Tactic:
constructor

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

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
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : Ring R'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R' M
inst✝² : SMulCommClass R R' M
inst✝¹ : TopologicalSpace M
inst✝ : DiscreteTopology M
⊢ (pure 0).HasBasis (fun x ↦ True) fun x ↦ ↑⊥

Tactic:
exact hasBasis_pure _

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
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 1)) }, ⋯⟩ = 1

Tactic:
ext

Goal state after:
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
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 1)) }, ⋯⟩).toCompletion =
    (↑1).toCompletion
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
⊢ (∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)) ↔
    ∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)) →
    ∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a

case mpr
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) →
    ∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
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
x y : R
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) (x * y))) }, ⋯⟩ =
    ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) x)) }, ⋯⟩ *
      ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) y)) }, ⋯⟩

Tactic:
ext

Goal state after:
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
x y : R
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) (x * y))) }, ⋯⟩).toCompletion =
    (↑(⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) x)) }, ⋯⟩ *
          ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) y)) }, ⋯⟩)).toCompletion
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
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 0)) }, ⋯⟩ = 0

Tactic:
ext

Goal state after:
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
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 0)) }, ⋯⟩).toCompletion =
    (↑0).toCompletion
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
x y : R
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) (x + y))) }, ⋯⟩ =
    ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) x)) }, ⋯⟩ +
      ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) y)) }, ⋯⟩

Tactic:
ext

Goal state after:
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
x y : R
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) (x + y))) }, ⋯⟩).toCompletion =
    (↑(⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) x)) }, ⋯⟩ +
          ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) y)) }, ⋯⟩)).toCompletion
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ r • x =
    { toFun := fun r ↦ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        r *
      x

Tactic:
ext

Goal state after:
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (↑(r • x)).toCompletion =
    (↑({ toFun := fun r ↦ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }, ⋯⟩,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
            r *
          x)).toCompletion
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ φ.order ≤ ↑n

Tactic:
exact order_le _ h

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
t : R
φ : R⟦X⟧
⊢ truncAux n (t • φ) = (RingHom.id R) t • truncAux n φ

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
t : R
φ : R⟦X⟧
n✝ : ℕ
⊢ (truncAux n (t • φ)).coeff n✝ = ((RingHom.id R) t • truncAux n φ).coeff n✝
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0

case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ 1 ≤ φ.order ↔ constantCoeff φ = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ 1 ≤ φ.order → constantCoeff φ = 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∀ (i : ℕ), ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0

Tactic:
constructor

Goal state after:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0

case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (monomial n) r = C r * X ^ n

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
n n✝ : ℕ
⊢ (coeff n✝) ((monomial n) r) = (coeff n✝) (C r * X ^ n)
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R⟦X⟧
⊢ (trunc n) (X ^ n * p) = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R⟦X⟧
n✝ : ℕ
⊢ ((trunc n) (X ^ n * p)).coeff n✝ = Polynomial.coeff 0 n✝
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M → IsLinearTopology R M

case mpr
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology R M → IsLinearTopology Rᵐᵒᵖ M
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ divXPowOrder 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
n✝ : ℕ
⊢ (coeff n✝) (divXPowOrder 0) = (coeff n✝) 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : n < f.order.toNat
⊢ 0 = (coeff n) f

Tactic:
rw [coeff_of_lt_order_toNat _ h]

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

Goal state before:
pp: case e_f
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d = Finsupp.single () (d ())

Tactic:
ext

Goal state after:
case e_f
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d default = (Finsupp.single () (d ())) default
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d ())

Tactic:
ext

Goal state after:
case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d ())) default
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)) ↔ ∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)) → ∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a

case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) → ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case e'_5.e_5
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ ()) x✝) = x✝

Tactic:
ext

Goal state after:
case e'_5.e_5
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ ()) x✝)) default = x✝ default
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case e'_5.e_6
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ ()) x✝) = x✝

Tactic:
ext

Goal state after:
case e'_5.e_6
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ ()) x✝)) default = x✝ default