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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b : ValueGroupWithZero R
hab : a ≤ b
hba : b ≤ a
⊢ a = b

Tactic:
induction a using ValueGroupWithZero.ind
    induction b using ValueGroupWithZero.ind
    exact ValueGroupWithZero.sound hab hba

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

Goal state before:
pp: case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑⟨x, hx⟩ * ↑t ≤ᵥ ↑s * ↑⟨y, hy⟩

Tactic:
veq_mul_comm _ y

Goal state after:
case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑⟨x, hx⟩ * ↑t ≤ᵥ y * ↑s
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✝
f : α ≃+* β
hf : Continuous ⇑f
hf' : Continuous ⇑f.symm
⊢ (mapRingHom f.toRingHom hf).comp (mapRingHom f.symm.toRingHom hf') = RingHom.id (Completion β)

Tactic:
by simp [mapRingHom_comp]

Goal state after:
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✝
f : α ≃+* β
hf : Continuous ⇑f
hf' : Continuous ⇑f.symm
⊢ (mapRingHom f.symm.toRingHom hf').comp (mapRingHom f.toRingHom hf) = RingHom.id (Completion α)

Tactic:
by simp [mapRingHom_comp]

Goal state after:
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
x : K
⊢ (↑x)⁻¹ = ↑x⁻¹

Tactic:
by
  by_cases h : x = 0
  · rw [h, inv_zero]
    dsimp [Inv.inv]
    norm_cast
    simp
  · conv_lhs => dsimp [Inv.inv]
    rw [if_neg]
    · exact hatInv_extends h
    · exact fun H => h (isDenseEmbedding_coe.injective H)

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
y : (ofClass v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v)) ((WithZero.map' ↑(valueGroupEquiv v).symm) y) = y

Tactic:
by
    match y with
    | 0 => simp
    | .coe b => simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.addXYZ P Q =
    addZ P Q •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
by
  have hZ {n : ℕ} : IsUnit <| addZ P Q ^ n := (isUnit_addZ_of_X_ne hx).pow n
  erw [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
    ← addY_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, mul_one]

Goal state after:
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
⊢ (valuation K (maximalIdeal A)).IsRankOneDiscrete

Tactic:
have : Nontrivial (valueGroup
      (.ofClass (valuation K (maximalIdeal A)))) := by
    let v := (maximalIdeal A).valuation K
    let π := valuation_exists_uniformizer K (maximalIdeal A) |>.choose
    have hπ : v π = ↑(ofAdd (-1 : ℤ)) :=
      valuation_exists_uniformizer K (maximalIdeal A) |>.choose_spec
    rw [Subgroup.nontrivial_iff_exists_ne_one]
    use Units.mk0 (v π) (by simp [hπ])
    constructor
    · apply mem_valueGroup
      use π
      simp [v]
    · simpa [hπ] using not_eq_of_beq_eq_false rfl

Goal state after:
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
this : Nontrivial ↥(MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A))).valueGroup
⊢ (valuation K (maximalIdeal A)).IsRankOneDiscrete
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: 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
⊢ ∃ ia, ∀ (x_1 : R), Valued.v.restrict x_1 < ↑ia → Valued.v.restrict x_1 < ↑x

Tactic:
set y₀ := h_val.orderMonoidIso x with hy₀_def

Goal state after:
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
⊢ ∃ ia, ∀ (x_1 : R), Valued.v.restrict x_1 < ↑ia → Valued.v.restrict x_1 < ↑x
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: 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
⊢ ∃ ia, ∀ (x_1 : R), Valued.v.restrict x_1 < ↑ia → Valued.v.restrict x_1 < ↑x

Tactic:
set y := (Units.mk0 y₀ hy₀_ne_zero) with hy_def

Goal state after:
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
⊢ ∃ ia, ∀ (x_1 : R), Valued.v.restrict x_1 < ↑ia → Valued.v.restrict x_1 < ↑x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Continuous[hv.toTopologicalSpace, _] ⇑v.restrict

Tactic:
rw [continuous_iff_continuousAt]
  intro x
  rcases eq_or_ne x 0 with (rfl | h)
  · rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
    intro γ hγ
    rw [Filter.Eventually, Valued.mem_nhds_zero]
    use Units.mk0 γ hγ; rfl
  · have v_ne : (v.restrict x : ValueGroup₀ (.ofClass hv.v)) ≠ 0 :=
      (Valuation.ne_zero_iff _).mpr h
    rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]
    simp_rw [v.restrict_inj]
    apply Valued.locally_const (by simpa [restrict₀_apply] using v_ne)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff (n + 1)) (X * φ) = (coeff n) φ

Tactic:
simp only [coeff, Finsupp.single_add, add_comm n 1]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () 1 + single () n)) (X * φ) = (MvPowerSeries.coeff (single () n)) φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ b c : ℕ
H : b + c = n✝
⊢ a ^ (b + c) * ((coeff b) f * (coeff c) g) = a ^ b * (coeff b) f * (a ^ c * (coeff c) g)

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ b c : ℕ
H : b + c = n✝
⊢ a ^ b * a ^ c * ((coeff b) f * (coeff c) g) = a ^ b * (coeff b) f * (a ^ c * (coeff c) g)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0

Tactic:
constructor
  · rintro ⟨φ, rfl⟩ m h
    rw [coeff_mul, Finset.sum_eq_zero]
    rintro ⟨i, j⟩ hij
    rw [coeff_X_pow, if_neg, zero_mul]
    contrapose! h
    dsimp at h
    subst i
    rw [mem_antidiagonal] at hij
    rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
    exact Nat.le_add_right n _
  · intro h
    refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
    ext m
    by_cases H : m - single s n + single s n = m
    · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
      · rw [coeff_X_pow, if_pos rfl, one_mul]
        simpa using! congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
      · rintro ⟨i, j⟩ hij hne
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]
        · exact zero_mul _
      · intro hni
        exfalso
        apply hni
        rwa [mem_antidiagonal, add_comm]
    · rw [h, coeff_mul, Finset.sum_eq_zero]
      · rintro ⟨i, j⟩ hij
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
        · exact zero_mul _
      · contrapose! H
        ext t
        by_cases hst : s = t
        · subst t
          simpa using! tsub_add_cancel_of_le H
        · simp [hst]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : d = 0
⊢ 1 = ↑(#{0})

Tactic:
simp only [card_singleton, Nat.cast_one]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
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
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : embedding ((restrict₀ (ofClass v)) ⋯.choose) = embedding ↑γ
⊢ ↑⟨Units.mk0 ((ofClass extensionValuation) x) ⋯, ⋯⟩ < valueGroup₀_equiv_extensionValuation ↑γ ↔ extension x < ↑γ

Tactic:
simp only [← hy_def, embedding_restrict₀, coe_ofClass] at hy

Goal state after:
case neg
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
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ↑⟨Units.mk0 ((ofClass extensionValuation) x) ⋯, ⋯⟩ < valueGroup₀_equiv_extensionValuation ↑γ ↔ extension x < ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
this : m ≤ #s
m' : ℕ
hm' : #s = m + m'
⊢ constantCoeff f ^ (m + m') = 0

Tactic:
pow_add,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
this : m ≤ #s
m' : ℕ
hm' : #s = m + m'
⊢ constantCoeff f ^ m * constantCoeff f ^ m' = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ ↑(C a) = PowerSeries.C a

Tactic:
have := coe_monomial 0 a
  rwa [PowerSeries.monomial_zero_eq_C_apply] at this

Goal state after:
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
i : ι
x✝ : i ∈ f.support
⊢ #(f i) = (fun i ↦ ↑(#(f i))) i (f i)

Tactic:
simp only [Pi.natCast_apply, Nat.cast_id]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff m) φ else 0

Tactic:
by
  simpa using! coeff_truncFinset (s := Iio n) (x := m) φ

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

Goal state before:
pp: case ind
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ (k + 1)) = (coeff x) (p ^ (k + 1))

Tactic:
pow_add,

Goal state after:
case ind
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ k * (truncTotal n) p ^ 1) = (coeff x) (p ^ k * p ^ 1)
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
⊢ a ^ (n + (i - n)) = 0

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
⊢ a ^ n * a ^ (i - n) = 0
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
g : MvPowerSeries σ R
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : σ →₀ ℕ),
      Tendsto (fun s ↦ ∑ x ∈ s, (coeff d) (f x)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))

Tactic:
← map_sum

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : σ →₀ ℕ),
      Tendsto (fun s ↦ (coeff d) (∑ b ∈ s, f b)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ ↑n = ↑i + ↑j

Tactic:
rw [← Nat.cast_add, hij]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
⊢ constantCoeff f.divXPowOrder = (coeff f.order.toNat) f

Tactic:
by
  simp [← coeff_zero_eq_constantCoeff]

Goal state after:
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⟧
g : R⟦X⟧
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : ℕ), Tendsto (fun s ↦ ∑ x ∈ s, (coeff d) (f x)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))

Tactic:
← map_sum

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : ℕ), Tendsto (fun s ↦ (coeff d) (∑ b ∈ s, f b)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.divXPowOrder = 1

Tactic:
ext n
  simp [coeff_X]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
⊢ n =ᶠ[cofinite] 0

Tactic:
filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
s : σ
has : a s ∈ ↑I
⊢ n s = 0 s
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
r : R
⊢ (↑↑(eval₂Hom ⋯ ha)).toFun ((algebraMap R (MvPowerSeries σ R)) r) = (algebraMap R S) r

Tactic:
by
    simp only [toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe]
    rw [← c_eq_algebraMap, coe_eval₂Hom, eval₂_C]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < (f ^ (k * (n + 1) + m)).order

Tactic:
pow_add,

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < (f ^ (k * (n + 1)) * f ^ m).order
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (subst a f) = (truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f))

Tactic:
ext d
  by_cases hd : d.degree < k
  · simp_rw [coeff_truncTotal _ hd, coeff_subst ha]
    have h1 := coeff_subst_finite ha f d
    have h2 := coeff_subst_finite ha (∑ i ∈ range k, (homogeneousComponent i) f) d
    rw [finsum_eq_sum _ h1, finsum_eq_sum _ h2]
    have : h2.toFinset ⊆ h1.toFinset := by simp +contextual [coeff_homogeneousComponent]
    have aux {n : σ →₀ ℕ} : coeff d (n.prod fun s e ↦ a s ^ e) ≠ 0 → n.degree ≤ d.degree := by
      contrapose!
      intro hc
      rw [Finsupp.prod]
      refine coeff_of_lt_order (lt_of_lt_of_le (Nat.cast_lt.mpr hc)
        (.trans ?_ (le_order_prod _ n.support)))
      exact_mod_cast sum_le_sum fun i hi => le_order_pow_of_constantCoeff_eq_zero _ (ha₁ i)
    rw [← Finset.sum_subset this]
    · congr! 2 with n hn
      simp only [map_sum, coeff_homogeneousComponent, sum_ite_eq, mem_range, left_eq_ite_iff,
        not_lt]
      have : n.degree ≤ d.degree := by
        simp only [map_sum, Set.Finite.mem_toFinset, Function.mem_support, ne_eq] at hn
        exact aux (right_ne_zero_of_smul hn)
      grind
    · simp +contextual only [Set.Finite.mem_toFinset, Function.mem_support, ne_eq, map_sum,
        coeff_homogeneousComponent, sum_ite_eq, mem_range, ite_smul, zero_smul, ite_eq_right_iff,
        imp_false, not_lt, not_le]
      grind [right_ne_zero_of_smul]
  simp_rw [coeff_truncTotal_eq_zero _ (not_lt.mp hd)]

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ c • univ

Tactic:
simp_all [smul_set_univ₀]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
⊢ ∃ a, ∀ (k l : Finset ι), a ⊆ k → a ⊆ l → (∏ b ∈ k, f b) n = (∏ b ∈ l, f b) n

Tactic:
replace hf : ∀ k ∈ Set.Iic n, ∀ᶠ (x : ι) in cofinite, (f x) k = (1 : ArithmeticFunction R) k :=
    fun k hk ↦ hf k

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
hf : ∀ k ∈ Set.Iic n, ∀ᶠ (x : ι) in cofinite, (f x) k = 1 k
⊢ ∃ a, ∀ (k l : Finset ι), a ⊆ k → a ⊆ l → (∏ b ∈ k, f b) n = (∏ b ∈ l, f b) n