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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ ⟦![1, 1, 0]⟧ = ⟦P⟧

Tactic:
Quotient.eq

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![1, 1, 0] P
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![W.dblX P, W.dblY P, W.dblZ P * ![W.dblX P / W.dblZ P ^ 2, W.dblY P / W.dblZ P ^ 3, 1] z]

Tactic:
mul_one

Goal state after:
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] = ![W.dblX P, W.dblY P, W.dblZ P]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
h : P ≈ Q
⊢ toAffine W P = toAffine W Q

Tactic:
rcases h with ⟨u, rfl⟩
  exact toAffine_smul Q u.isUnit

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ toAffine W (W.add P Q) =
    Affine.Point.some (P x / P z ^ 2) (P y / P z ^ 3) ⋯ + Affine.Point.some (Q x / Q z ^ 2) (Q y / Q z ^ 3) ⋯

Tactic:
Affine.Point.add_of_Y_eq
            ((X_eq_iff hPz hQz).mp hxy.left) ((Y_eq_iff' hPz hQz).mp hxy.right)

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ toAffine W (W.add P Q) = 0
Module: Mathlib.Topology.Algebra.UniformRing

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

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑a = ↑a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, W'.addY P P, addZ P P] = ![0, 0, 0]

Tactic:
addY_self hP,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, 0, addZ P P] = ![0, 0, 0]
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
⊢ (ofClass Valued.v).valueGroup = (ofClass v).valueGroup

Tactic:
simp [valueGroup, valueMonoid, ← (WithVal.ofVal_surjective v).range_comp]
  rfl

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
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ ![W.addX P Q, W.addY P Q, addZ P Q] =
    ![W.addX P Q, W.addY P Q, addZ P Q * ![W.addX P Q / addZ P Q ^ 2, W.addY P Q / addZ P Q ^ 3, 1] z]

Tactic:
mul_one

Goal state after:
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
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ ![W.addX P Q, W.addY P Q, addZ P Q] = ![W.addX P Q, W.addY P Q, addZ P Q]
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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ UniformContinuous ⇑(equiv v)

Tactic:
refine uniformContinuous_of_continuousAt_zero _ ?_
  simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]
  intro γ
  obtain ⟨r, s, hr₀, hs₀, hr⟩ := exists_div_eq_of_unit Valued.v γ
  use .mk0 ((instValued v).v.restrict ((WithVal.equiv v).symm r) /
    (instValued v).v.restrict ((WithVal.equiv v).symm s)) (by
    simp [Valuation.restrict_def, restrict₀_eq_zero_iff, (eq_zero h (r := r)).ne, ← hv,
      (eq_zero h (r := s)).ne, hr₀.ne', hs₀.ne'])
  intro x hx
  let y := (WithVal.equiv v) x
  have hy : toVal v y = x := rfl
  have hs0' : 0 < Valued.v.restrict (toVal v s) := by
    simp [restrict_pos_iff, h.pos_iff, ← hv, hs₀]
  have h' : v.restrict.IsEquiv w.restrict := h.restrict
  rw [← hr, equiv_apply, Set.mem_ofPred_eq, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), hv,
    ← map_mul, ← lt_def, ← ofVal_mul,
    ← hy, ← toVal_mul, ←  h'.orderRingIso_apply, ← h'.orderRingIso.lt_symm_apply]
  simp only [toVal_mul, orderRingIso_symm_apply, lt_def, ofVal_mul, restrict_lt_iff]
  simp only [equiv_symm_apply, Units.val_mk0, Set.mem_ofPred_eq, lt_div_iff₀ hs0'] at hx
  rwa [← map_mul, restrict_lt_iff] at hx

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

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ofClass v).ValueGroup₀ˣ
r : K
hr : (restrict₀ (ofClass v)) r = ↑γ
⊢ 0 < v r

Tactic:
rw [← map_zero v]

Goal state after:
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ofClass v).ValueGroup₀ˣ
r : K
hr : (restrict₀ (ofClass v)) r = ↑γ
⊢ v 0 < v r
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, v.restrict x_1 = v.restrict x

Tactic:
v.restrict_inj

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, v x_1 = v x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ y * 1 * y₀⁻¹ ∈ V

Tactic:
mul_one

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ y * y₀⁻¹ ∈ V
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : v.restrict (a * z₀⁻¹) = 1
⊢ v.restrict a = v.restrict (a * 1)

Tactic:
mul_one

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : v.restrict (a * z₀⁻¹) = 1
⊢ v.restrict a = v.restrict a
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 Γ₀
⊢ embedding (v.restrict 1) = 1

Tactic:
Valuation.map_one _,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ embedding 1 = 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h✝ : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
⊢ {b | ∃ r, v.restrict r = extension b} = extension ⁻¹' range ⇑v.restrict

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was: `grind` -/

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h✝ : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
⊢ {b | ∃ r, v.restrict r = extension b} = extension ⁻¹' range ⇑v.restrict
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : Preorder β
inst✝¹ : LE γ
inst✝ : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})
c : γ
b : β
hb : ∀ y ∈ h' ⁻¹' {x | x ≤ c}, y ≤ b
⊢ {a | (h' ∘ h) a ≤ c}.Finite

Tactic:
exact (finite_le (h := h) b).subset <| by grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
⊢ Subsingleton R⟦X⟧

Tactic:
simp only [subsingleton_iff, PowerSeries.ext_iff]
  subsingleton

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n)) φ = (MvPowerSeries.coeff (single () n)) φ * 1

Tactic:
mul_one

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

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

Tactic:
convert! φ.coeff_add_monomial_mul (single () 1) (single () n) _

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff (d, n).1) p * 1 = (coeff d) p

pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff b.1) p * (coeff b.2) (X ^ n) = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff (d, n).1) p = (coeff d) p

case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff b.1) p * (coeff b.2) (X ^ n) = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ (coeff k) ((map f) (mk fun k ↦ Function.surjInv hf ((coeff k) g))) = (coeff k) g

Tactic:
simp only [Function.surjInv, coeff_map, coeff_mk]

Goal state after:
case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ f (Classical.choose ⋯) = (coeff k) g
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b : R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) ((rescale (a * b)) x✝) = (coeff n✝) (((rescale b).comp (rescale a)) x✝)

Tactic:
simp [← rescale_rescale]

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 : ℕ
⊢ v.intValuation r ≤ exp (-↑n) ↔ ↑n ≤ emultiplicity v.asIdeal (Ideal.span {r})

Tactic:
rw [intValuation_le_pow_iff_dvd, pow_dvd_iff_le_emultiplicity]

Goal state after:
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' * (coeff 1) φ) * constantCoeff φ ^ (n' - 1) =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
move_mul [← constantCoeff φ ^ (n' - 1)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff d) (f ^ n) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f

Tactic:
rw [this, coeff_prod]

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

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

Tactic:
simpa [hr]

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

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

Tactic:
mul_one

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r ^ n) * 1)

Tactic:
mul_one

Goal state after:
σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (MvPowerSeries.monomial e) (e.prod fun s n ↦ r ^ n)
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ constantCoeff f = 0 → 1 ≤ f.order

Tactic:
· intro h
    apply coeff_of_lt_order
    simpa using Order.one_le_iff_pos.mp h

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ constantCoeff f = 0 → 1 ≤ f.order
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
x✝ : ℕ
hi : x✝ ≥ 1
⊢ 0 ^ x✝ = 0

Tactic:
zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
x✝ : ℕ
hi : x✝ ≥ 1
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
⊢ Tendsto (fun d ↦ ↑((trunc R d) f)) atTop (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]
  intro d
  obtain ⟨s, _⟩ := (exists_const σ).mpr trivial
  apply tendsto_atTop_of_eventually_const (i₀ := d + Finsupp.single s 1)
  intro n hn
  rw [MvPolynomial.coeff_coe, coeff_trunc, if_pos]
  apply lt_of_lt_of_le _ hn
  simpa [Finsupp.lt_def] using ⟨s, by simp⟩

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

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

Tactic:
simp_rw [HasSum, ← map_sum]
  apply tendsto_iff_coeff_tendsto

Goal state after:
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:
rw [order, dif_neg]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ¬φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
⊢ (coeff i) ((monomial n) a) ≠ 0

Tactic:
rwa [hi, coeff_monomial_same]

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⟧
⊢ HasSum f g ↔ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)

Tactic:
simp_rw [HasSum, ← map_sum]
  apply tendsto_iff_coeff_tendsto

Goal state after:
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
ha : HasSubst a
s : σ
⊢ (substAlgHom ha) (X s) = a s

Tactic:
← MvPolynomial.coe_X,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
s : σ
⊢ (substAlgHom ha) ↑(MvPolynomial.X s) = a s
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

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

Tactic:
mul_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (algebraMap R S) ((coeff e) f)
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ ≤ C * ↑n ^ (-(s + (1 - ↑x)).re + s.re)

Tactic:
simpa using hC n <| Nat.pos_iff_ne_zero.mp hn

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

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
a b : σ → R
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((rescale (a * b)) x✝) = (coeff n✝) (((rescale b).comp (rescale a)) x✝)

Tactic:
simp [← rescale_rescale]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ subst P P.substInv = X

Tactic:
by
  have : Invertible (P.substInv.coeff 1) := by simpa using invertibleInvOf
  let Q := P.substInv.substInv
  have hQ : HasSubst Q := HasSubst.substInv P.substInv
  have eq_aux : P.substInv.subst Q = X := subst_substInv_right P.substInv P.constantCoeff_substInv
  suffices h : Q = P from by simp_rw [← h, eq_aux]
  calc
    _ = PowerSeries.subst Q (P.subst P.substInv) := by
      rw [subst_substInv_right _ hP, subst_X hQ]
    _ = P := by
      simp [subst_comp_subst_apply (HasSubst.substInv P) hQ, eq_aux]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff d) f * (MvPowerSeries.coeff e) ((X₀ + X₁) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f

Tactic:
← MvPolynomial.coe_X,

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff d) f * (MvPowerSeries.coeff e) ((↑(MvPolynomial.X 0) + ↑(MvPolynomial.X 1)) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
⊢ ‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖

Tactic:
simp [← toSpanSingleton_derivWithin]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case convert_3
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), R k = σ' k
⊢ HasDerivAt f f' (R (σ x))

Tactic:
hR,

Goal state after:
case convert_3
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), R k = σ' k
⊢ HasDerivAt f f' (σ' (σ x))