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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

pp: case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : ¬a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

Tactic:
· simp [ha]

Goal state after:
case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : ¬a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
⊢ i ∈ span {x * y}

Tactic:
have hasup : a ∈ I ⊔ span {a} := mem_sup_right (mem_span_singleton_self a)

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
hasup : a ∈ I ⊔ span {a}
⊢ i ∈ span {x * y}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3

Tactic:
rw [Affine.negAddY, toAffine_addX_of_ne hPz hQz hd]
  simp [field]

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

Goal state before:
pp: case a
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst✝¹ : Field K
w : Valuation K Γ
inst✝ : w.IsRankOneDiscrete
⊢ ↑(generator w) ∈ range ⇑w \ ?t

pp: case t
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst✝¹ : Field K
w : Valuation K Γ
inst✝ : w.IsRankOneDiscrete
⊢ Set Γ

Tactic:
← generator_zpowers_eq_range

Goal state after:
case a
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst✝¹ : Field K
w : Valuation K Γ
inst✝ : w.IsRankOneDiscrete
⊢ ↑(generator w) ∈ Units.val '' ↑(zpowers (generator w))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian 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.addY P Q = (-((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z))) ^ 3

Tactic:
← neg_div,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian 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.addY P Q = (-(P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)) ^ 3
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
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    True → ∃ ia, True ∧ ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict x < ↑ib}

Tactic:
true_and,

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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    True → ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict x < ↑ib}
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 : w.IsEquiv v
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    True → ∃ ia, True ∧ ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑ib}

Tactic:
true_and,

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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    True → ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑ib}
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
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    True → ∃ ia, True ∧ ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (RingHom.id R) x ∈ {x | Valued.v.restrict x < ↑ib}

Tactic:
true_and,

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
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    True → ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (RingHom.id R) x ∈ {x | Valued.v.restrict x < ↑ib}
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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

Tactic:
have h1 := IsEquiv.uniformContinuous_equiv (hval := Valued.mk' w) rfl h

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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous ⇑(equiv v)
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))
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 Γ₀
hv : Function.Surjective ⇑v
γ : Γ₀ˣ
⊢ ∃ r s, 0 < v r ∧ 0 < v s ∧ v r / v s = ↑γ

Tactic:
by
  obtain ⟨r, hr⟩ := hv γ
  exact ⟨r, 1, by simp [hr]⟩

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hdef : γ' = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
y : K
hy : y ∈ {y | v.restrict (y - 0) < ↑γ'}
⊢ y ∈ {k | v k < v x}

Tactic:
by
    simp only [Valuation.restrict_lt_iff_lt_embedding, hdef, sub_zero, Units.val_mk0,
      mem_ofPred_eq, embedding_restrict₀] at hy
    simpa using hy

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ T0Space K

Tactic:
suffices T2Space K by infer_instance
  apply IsTopologicalAddGroup.t2Space_of_zero_sep
  intro x x_ne
  refine ⟨{ k | v k < v x }, ?_, fun h => lt_irrefl _ h⟩
  rw [Valued.mem_nhds]
  set γ' := Units.mk0 ((ValueGroup₀.restrict₀ _) x) (v.restrict.ne_zero_iff.mpr x_ne) with hdef
  exact ⟨γ', fun y hy => by
    simp only [Valuation.restrict_lt_iff_lt_embedding, hdef, sub_zero, Units.val_mk0,
      mem_ofPred_eq, embedding_restrict₀] at hy
    simpa using hy⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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
x y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ u, u • x = y

Tactic:
have : (y / x) ∈ MonoidHom.mker (((maximalIdeal A).valuation K)) := by simp_all

Goal state after:
case neg
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
x y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
this : y / x ∈ MonoidHom.mker (valuation K (maximalIdeal A))
⊢ ∃ u, u • x = y
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
x : K
xM : x ∈ M
hyp : v.restrict x < ↑γ₀
this : x ∈ U ∩ M
⊢ False

Tactic:
rwa [H] at this

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₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, ∀ (x : K), ↑x ∈ V → v x = 1

Tactic:
by
      rwa [Completion.isDenseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one

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₀ : 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
⊢ v.restrict (a * z₀⁻¹) = 1

Tactic:
v.restrict_def,

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
⊢ (ValueGroup₀.restrict₀ (ofClass v)) (a * z₀⁻¹) = 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ G ≃*o WithZero (Multiplicative ℤ)

Tactic:
· refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩
    intros
    simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero,
      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
    split_ifs <;>
    simp_all [← Units.val_le_val]

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

Goal state before:
pp: case ih
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)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b

Tactic:
intro x y
      norm_cast
      exact le_max_iff.mp (v.restrict.map_add x y)

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 Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) x = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) y = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : (restrict₀ (ofClass v)) ⋯.choose = a * b
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y

Tactic:
rw [← hxy_def] at hxy

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) x = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) y = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : (restrict₀ (ofClass v)) xy = a * b
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ MvPolynomial.coeff x ((truncFinset S s) ((map f) p)) =
    MvPolynomial.coeff x ((MvPolynomial.map f) ((truncFinset R s) p))

Tactic:
by_cases x ∈ s <;> grind [coeff_map, MvPolynomial.coeff_map]

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

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

Tactic:
intro d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ↑((weight w) d) < weightedOrder w f + weightedOrder w g → (coeff d) (f * g) = 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
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc' R i) f)) atTop (𝓝 ((coeff d) f))

Tactic:
intro d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Tendsto (fun i ↦ (coeff d) ↑((trunc' R i) f)) atTop (𝓝 ((coeff d) f))
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
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc R i) f)) atTop (𝓝 ((coeff d) f))

Tactic:
intro d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Tendsto (fun i ↦ (coeff d) ↑((trunc R i) f)) atTop (𝓝 ((coeff d) f))
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

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

Tactic:
intro d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ HasSum (fun i ↦ (monomial i) ((coeff i) f) d) (f d)
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
simp only [order, h, not_false_iff, dif_neg]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ (coeff (↑(Nat.find ⋯)).toNat) φ ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
⊢ ∀ (d : σ →₀ ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
intro d

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
d : σ →₀ ℕ
⊢ Summable fun i ↦ (coeff d) (f i)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ ↑n < φ.order

Tactic:
← coe_toNat_order h',

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ ↑n < ↑φ.order.toNat
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⟧
u : Filter ι
g : R⟦X⟧
⊢ ∀ (a : Unit →₀ ℕ),
    Tendsto (fun i ↦ (MvPowerSeries.coeff a) (f i)) u (𝓝 ((MvPowerSeries.coeff a) g)) ↔
      Tendsto (fun i ↦ (coeff ((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv a)) (f i)) u
        (𝓝 ((coeff ((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv a)) g))

Tactic:
intro d

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i ↦ (MvPowerSeries.coeff d) (f i)) u (𝓝 ((MvPowerSeries.coeff d) g)) ↔
    Tendsto (fun i ↦ (coeff ((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv d)) (f i)) u
      (𝓝 ((coeff ((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv d)) g))
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc i) f)) atTop (𝓝 ((coeff d) f))

Tactic:
intro d

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
d : ℕ
⊢ Tendsto (fun i ↦ (coeff d) ↑((trunc i) f)) atTop (𝓝 ((coeff d) f))
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
⊢ Multipliable fun n ↦ 1 - X ^ (n + 1)

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
⊢ Multipliable fun n ↦ 1 + -X ^ (n + 1)
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 : σ → ℕ := ⋯
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := ⋯
D : Set (σ →₀ ℕ) := ⋯
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
⊢ ∀ c ∈ p.support, φ (MvPolynomial.coeff c p) * ∏ i ∈ c.support, a i ^ c i ∈ I

Tactic:
intro d

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
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
⊢ d ∈ p.support → φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
⊢ ∀ (d : σ →₀ ℕ) (i : Ideal R), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ℕ) in atTop, (coeff d) (f ^ x) ∈ ↑i

Tactic:
intro d

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
d : σ →₀ ℕ
⊢ ∀ (i : Ideal R), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ℕ) in atTop, (coeff d) (f ^ x) ∈ ↑i
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
⊢ ∀ x ∉ Set.range (Finsupp.single ()), (φ ((MvPowerSeries.coeff x) f) * x.prod fun s e ↦ a ^ e) = 0

Tactic:
intro d

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
d : Unit →₀ ℕ
⊢ d ∉ Set.range (Finsupp.single ()) → (φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case h
σ : 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
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ ε (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p

Tactic:
← MvPolynomial.coe_eval₂Hom,

Goal state after:
case h
σ : 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
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ ε ((MvPolynomial.eval₂Hom φ a) p) = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p