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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := ⋯
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
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⋯
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑(π.val ^ n) * ↑↑h_unit_a.unit

Tactic:
IsUnit.unit_spec,

Goal state after:
case h
Γ : 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
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑(π.val ^ n) * ↑a
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case IJ
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
⊢ x ∈ maximalIdeal ↥v.valuationSubring → x ∈ span {π.val}

Tactic:
hx

Goal state after:
case IJ
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
⊢ x ∈ span {π.val}
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
x : WithVal v
⊢ x ∈
      {x |
        Valued.v.restrict x <
          ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)} →
    (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
hx

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
x : WithVal v
hx :
  x ∈
    {x |
      Valued.v.restrict x <
        ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)}
⊢ (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
⊢ x ∈ {x | Valued.v.restrict x < ↑(Units.mk0 (Valued.v.restrict ((equiv v) r) / Valued.v.restrict ((equiv v) s)) ⋯)} →
    (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
hx

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : x ∈ {x | Valued.v.restrict x < ↑(Units.mk0 (Valued.v.restrict ((equiv v) r) / Valued.v.restrict ((equiv v) s)) ⋯)}
⊢ (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : h_val.orderMonoidIso (Valued.v.restrict b) < ↑y
⊢ Valued.v.restrict b < ↑x

Tactic:
hy_def,

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : h_val.orderMonoidIso (Valued.v.restrict b) < ↑(Units.mk0 y₀ hy₀_ne_zero)
⊢ Valued.v.restrict b < ↑x
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
⊢ ↑x ∈ s → ∀ (a : X), ↑a ∈ s → x < a → ∃ a_2, (↑a_2 ∈ s ∧ x < a_2) ∧ a_2 < a

Tactic:
hx

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
⊢ ∀ (a : X), ↑a ∈ s → x < a → ∃ a_2, (↑a_2 ∈ s ∧ x < a_2) ∧ a_2 < a
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x : G₀
hxg : x ≤ g
⊢ ¬x = 0 → g⁻¹ ≤ x⁻¹

Tactic:
hx

Goal state after:
case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ g⁻¹ ≤ x⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
a✝ : MulArchimedean α
⊢ MulArchimedean (WithZero α)

Tactic:
· infer_instance

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
a✝ : MulArchimedean G₀
⊢ MulArchimedean G₀ˣ

Tactic:
· infer_instance

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
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
· by_cases hy : y = 0
    · rw [hy, add_zero]
      order
    · by_cases hxy : x + y = 0
      · rw [intValuationDef, if_pos hxy]; exact zero_le
      · rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy,
          le_max_iff]
        simp only [exp_le_exp, neg_le_neg_iff, Nat.cast_le, ← min_le_iff]
        set nmin :=
          min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
            ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
        have h_dvd_x : x ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff x nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
          · exact min_le_left _ _
          exact v.associates_irreducible
        have h_dvd_y : y ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff y nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]
          · exact min_le_right _ _
          exact v.associates_irreducible
        have h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y}) := by
          rw [Associates.le_singleton_iff]
          exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y
        rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy
        · exact h_dvd_xy
        exact v.associates_irreducible

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ emultiplicity v.asIdeal (Ideal.span {r}) ≤ ↑n

Tactic:
← ENat.lt_natCast_add_one_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ emultiplicity v.asIdeal (Ideal.span {r}) < ↑n + 1
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) φ + constantCoeff φ ^ (n' - 1) * constantCoeff φ * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]

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'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1) * constantCoeff φ ^ 1 * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)

Tactic:
by
  rcases Nat.eq_zero_or_pos n with (rfl | hn)
  · simp
  induction n with
  | zero => lia
  | succ n' ih =>
      have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
      have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
      rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]
      · simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
          add_tsub_cancel_right]
        have h₀ : n' = 0 ∨ 1 ≤ n' := by lia
        rcases h₀ with h' | h'
        · by_contra h''
          rw [h'] at h''
          simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''
          norm_num at h''
        · rw [ih]
          · 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
          exact h'
      · decide

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
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
⊢ ↑n ≤ weightedOrder w f

Tactic:
by_contra! H
  have : (f.weightedOrder w).toNat = f.weightedOrder w := by
    rw [natCast_toNat_eq_self]; exact ne_top_of_lt H
  obtain ⟨d, hfd, hd⟩ := exists_coeff_ne_zero_and_weightedOrder w this
  rw [← hd, Nat.cast_lt] at H
  exact hfd (h d H)

Goal state after:
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
n : ℕ
h : weightedOrder w f = ↑n
d : σ →₀ ℕ
hd : (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
⊢ (∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0

Tactic:
exact ⟨⟨d, by simpa [h, Nat.cast_inj, ne_eq] using hd⟩,
      fun e he ↦ f.coeff_eq_zero_of_lt_weightedOrder w (by simp only [h, Nat.cast_lt, he])⟩

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ (monomial d) 0 = 0

Tactic:
map_zero

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ 0 = 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x ∈ Finset.antidiagonal d → (coeff x.1) f * (coeff x.2) g = 0

Tactic:
hx

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x ∈ Finset.antidiagonal d
⊢ (coeff x.1) f * (coeff x.2) g = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
⊢ (fun d ↦ if (weight w) d = p then (coeff d) (f + g) else 0) =
    (fun d ↦ if (weight w) d = p then (coeff d) f else 0) + fun d ↦ if (weight w) d = p then (coeff d) g else 0

Tactic:
ext d
    simp only [map_add, coeff_apply]
    split_ifs with h
    · rfl
    · rw [add_zero]

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

Goal state before:
pp: 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

Tactic:
map_zero

Goal state after:
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 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: 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
x : (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x ∈ Finset.antidiagonal d →
    (coeff x.1) f * (coeff x.2) g =
      (coeff x.1) ((weightedHomogeneousComponent w p) f) * (coeff x.2) ((weightedHomogeneousComponent w q) g)

Tactic:
hx

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
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x ∈ Finset.antidiagonal d
⊢ (coeff x.1) f * (coeff x.2) g =
    (coeff x.1) ((weightedHomogeneousComponent w p) f) * (coeff x.2) ((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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 0) } = 0

Tactic:
apply adicCompletion.ext

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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 0) }.toCompletion = toCompletion 0
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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 1) } = 1

Tactic:
apply adicCompletion.ext

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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 1) }.toCompletion = toCompletion 1
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
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) } =
    { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } +
      { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }

Tactic:
apply adicCompletion.ext

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
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } +
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x * y)) } =
    { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } *
      { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }

Tactic:
apply adicCompletion.ext

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
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x * y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } *
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }).toCompletion
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 : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g) (p + q)

Tactic:
exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

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
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S₀ (adicCompletion K v)) x = (algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)

Tactic:
apply adicCompletion.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
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ ((algebraMap S₀ (adicCompletion K v)) x).toCompletion =
    ((algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)).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
inst✝ : Algebra S K
r : S
x : WithVal (valuation K v)
⊢ { toCompletion := ↑(r • x) } = r • { toCompletion := ↑x }

Tactic:
apply adicCompletion.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
inst✝ : Algebra S K
r : S
x : WithVal (valuation K v)
⊢ { toCompletion := ↑(r • x) }.toCompletion = (r • { toCompletion := ↑x }).toCompletion
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✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
r : R
i : M
hi : i ∈ A
x y : M
x✝¹ : x ∈ AddSubgroup.closure S
x✝ : y ∈ AddSubgroup.closure S
hx : r • x ∈ A
hy : r • y ∈ A
⊢ r • x + r • y ∈ A

Tactic:
exact add_mem hx hy

Goal state after:
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✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
x y : M
x✝¹ : x ∈ AddSubgroup.closure S
x✝ : y ∈ AddSubgroup.closure S
hx : r' • x ∈ A
hy : r' • y ∈ A
⊢ r' • x + r' • y ∈ A

Tactic:
exact add_mem hx hy

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ (monomial n) 0 = 0

Tactic:
map_zero

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

Tactic:
simp +contextual [coeff_trunc, coeff_X_pow_mul']

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
⊢ x ∈ antidiagonal n → (coeff x.1) φ * (coeff x.2) ψ = 0

Tactic:
hx

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x ∈ antidiagonal n
⊢ (coeff x.1) φ * (coeff x.2) ψ = 0