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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
· rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]

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

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑v * ↑w ≤ᵥ t * ↑v * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
veq_mul_right_comm r,

Goal state after:
case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑w * ↑v ≤ᵥ t * ↑v * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑0 + ↑a = ↑a

Tactic:
← coe_add,

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑(0 + a) = ↑a
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑a + ↑0 = ↑a

Tactic:
← coe_add,

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑(a + 0) = ↑a
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑x + ↑y = ↑y + ↑x

Tactic:
← coe_add,

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑(x + y) = ↑y + ↑x
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑(x + y) = ↑y + ↑x

Tactic:
← coe_add,

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑(x + y) = ↑(y + x)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑a * (↑b + ↑c) = ↑a * ↑b + ↑a * ↑c

Tactic:
← coe_add,

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑a * ↑(b + c) = ↑a * ↑b + ↑a * ↑c
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a * (b + c)) = ↑(a * b) + ↑(a * c)

Tactic:
← coe_add,

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a * (b + c)) = ↑(a * b + a * c)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ (↑a + ↑b) * ↑c = ↑a * ↑c + ↑b * ↑c

Tactic:
← coe_add,

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a + b) * ↑c = ↑a * ↑c + ↑b * ↑c
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑((a + b) * c) = ↑(a * c) + ↑(b * c)

Tactic:
← coe_add,

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑((a + b) * c) = ↑(a * c + b * c)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf✝ : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension (⇑f) (↑a + ↑b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b

Tactic:
← coe_add,

Goal state after:
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf✝ : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension ⇑f ↑(a + b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (range coe')
⊢ x ∈ closure (c '' {0}ᶜ)

Tactic:
← image_univ,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' univ)
⊢ x ∈ closure (c '' {0}ᶜ)
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ v.IsNontrivial

Tactic:
apply IsNontrivial.mk
  by_contra! h1
  have hvalueGroup : valueGroup (.ofClass v) = ⊥ := by
    simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      closure_eq_bot_iff, subset_singleton_iff, mem_preimage, mem_range, forall_exists_index,
      Units.ext_iff]
    intro y x
    specialize h1 x
    aesop
  aesop (add safe forward [generator_lt_one, generator_zpowers_eq_valueGroup])

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 ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v ↑π₁ = ↑(generator v)

Tactic:
← IsUniformizer.iff

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v.IsUniformizer ↑π₁
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 = Units.mk0 (v ↑r) hr₀
⊢ v ↑π.val ^ m = ↑(Units.mk0 (v ↑r) hr₀)

Tactic:
← 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 = Units.mk0 (v ↑r) hr₀
⊢ v ↑π.val ^ m = ↑(Units.mk0 (v ↑π.val) ⋯ ^ m)
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h.left
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
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ Units.mk0 (v π) ⋯ ∈ (MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A))).valueGroup

Tactic:
apply mem_valueGroup
      use π
      simp [v]

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 y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (⇑embedding ∘ extension) (x + y) ≤ max ((⇑embedding ∘ extension) x) ((⇑embedding ∘ extension) y)

Tactic:
simp_rw [le_max_iff, Function.comp_apply]
    rw [embedding_strictMono.le_iff_le, embedding_strictMono.le_iff_le (f := embedding)]
    apply Completion.induction_on₂ x y
      (p := fun x y => extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y)
    · have cont : Continuous (Valued.extension : hat K → _) := Valued.continuous_extension
      exact (isClosed_le (by fun_prop) <| cont.comp continuous_fst).union
          (isClosed_le (by fun_prop) <| cont.comp continuous_snd)
    · intro x y
      norm_cast
      exact le_max_iff.mp (v.restrict.map_add x y)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ⇑(coeff 0) = ⇑constantCoeff

Tactic:
by
  rw [coeff, Finsupp.single_zero]
  rfl

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then (coeff (m - n)) φ * a else 0) = if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
split_ifs <;> [apply h; rfl]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
hy,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ (if x * 0 = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * 0})).factors))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if 0 = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {0})).factors))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
hy,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef (x + 0) ≤ max (v.intValuationDef x) (v.intValuationDef 0)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ antidiagonal n, f ((coeff x.1) φ * (coeff x.2) ψ) =
    ∑ p ∈ antidiagonal n, ((coeff p.1) fun n ↦ f ((coeff n) φ)) * (coeff p.2) fun n ↦ f ((coeff n) ψ)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal n,
    f ((coeff x.1) φ * (coeff x.2) ψ) = ((coeff x.1) fun n ↦ f ((coeff n) φ)) * (coeff x.2) fun n ↦ f ((coeff n) ψ)
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) =
    ∑ 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)

Tactic:
apply Finset.sum_congr rfl

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 : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    (coeff x.1) (f a) * (coeff x.2) (∏ x ∈ s, f x) =
      ∑ 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)
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)
u v : σ →₀ ℕ
⊢ ∑ x ∈ (s.finsuppAntidiag v).attach, (coeff u) (f a) * ∏ i ∈ s, (coeff (↑x i)) (f i) =
    ∑ x ∈ (s.finsuppAntidiag v).attach, ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a u x_1)) (f x_1)

Tactic:
apply Finset.sum_congr rfl

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)
u v : σ →₀ ℕ
⊢ ∀ x ∈ (s.finsuppAntidiag v).attach,
    (coeff u) (f a) * ∏ i ∈ s, (coeff (↑x i)) (f i) =
      ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a u x_1)) (f x_1)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : x = 0
⊢ 0 < ↑⟨Units.mk0 ((ofClass extensionValuation) ↑⋯.choose) ?pos.hnc✝, ⋯⟩ ↔ extension 0 < ↑γ

pp: case pos.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : x = 0
⊢ ¬(ofClass extensionValuation) ↑⋯.choose = 0

Tactic:
· have hext : hv.extension 0 = 0 := by rw [extension_eq_zero_iff]
              simp [hext]

Goal state after:
case pos.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : x = 0
⊢ ¬(ofClass extensionValuation) ↑⋯.choose = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ∑ i ∈ Finset.range (φ.natDegree + 1), PowerSeries.C (φ.coeff i) * PowerSeries.X ^ i =
    ∑ x ∈ Finset.range (φ.natDegree + 1), coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ∀ x ∈ Finset.range (φ.natDegree + 1),
    PowerSeries.C (φ.coeff x) * PowerSeries.X ^ x = coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R (MvPowerSeries σ A)) r = C ((algebraMap R A) r)

Tactic:
by
  change (MvPowerSeries.map (algebraMap R A)).comp C r = _
  simp

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

Goal state before:
pp: case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff d) f = 0
⊢ f = 0

Tactic:
ext d

Goal state after:
case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff d) f = 0
d : σ →₀ ℕ
⊢ (coeff d) f = (coeff d) 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ (MvPowerSeries.monomial (p • e)) r = MvPowerSeries.C r * e.prod fun s e ↦ (MvPowerSeries.X s ^ p) ^ e

Tactic:
rw [MvPowerSeries.monomial_eq', Finsupp.prod_of_support_subset _ Finsupp.support_smul _
    (by simp), Finsupp.prod]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ MvPowerSeries.C r * ∏ x ∈ e.support, MvPowerSeries.X x ^ (p • e) x =
    MvPowerSeries.C r * ∏ a ∈ e.support, (MvPowerSeries.X a ^ p) ^ e a
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

Tactic:
have hγz : WithZero.coe γ ≠ 0 := WithZero.coe_ne_zero

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ
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 : ι →₀ α
⊢ #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Tactic:
simp [Iic_eq_Icc, card_Icc, bot_eq_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ ↑((truncTotal n) p) = ∑ i ∈ range n, (homogeneousComponent i) p

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (coeff d) ↑((truncTotal n) p) = (coeff d) (∑ i ∈ range n, (homogeneousComponent i) p)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ (truncTotal n) (p ^ m) = (truncTotal n) (↑((truncTotal n) p) ^ m)

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ MvPolynomial.coeff d ((truncTotal n) (p ^ m)) = MvPolynomial.coeff d ((truncTotal n) (↑((truncTotal n) p) ^ m))
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, ↑(degree d) < (g i).order) → (coeff d) (f * ∏ i ∈ s, (1 - g i)) = (coeff d) f

Tactic:
by
  rw [degree_eq_weight_one]
  exact coeff_mul_prod_one_sub_of_lt_weightedOrder _ d s f g

Goal state after:
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

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ((coeff d) fun d ↦ if (weight w) d = p then (coeff d) (f + g) else 0) =
    (coeff d)
      ((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)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ¬(weight w) d = p
⊢ 0 = 0 + 0

Tactic:
· rw [add_zero]

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

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

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
a : R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ((coeff d) fun d ↦ if (weight w) d = p then (coeff d) (a • f) else 0) =
    (coeff d) ((RingHom.id R) a • fun d ↦ if (weight w) d = p then (coeff d) f else 0)
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
⊢ (weightedHomogeneousComponent w p) f = 0

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
⊢ (coeff d) ((weightedHomogeneousComponent w p) f) = (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
⊢ f = (weightedHomogeneousComponent w p) f

Tactic:
ext d

Goal state after:
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 = (coeff d) ((weightedHomogeneousComponent w p) f)