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

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ (↑(f.lift h)).toFun (f.mk' a s + f.mk' b s) ≤ max ((↑(f.lift h)).toFun (f.mk' a s)) ((↑(f.lift h)).toFun (f.mk' b s))

Tactic:
convert_to! f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)

Goal state after:
case e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ (↑(f.lift h)).toFun (f.mk' a s + f.mk' b s) = (f.lift h) (f.mk' (a + b) s)

case convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ (f.lift h) (f.mk' (a + b) s) ≤ max ((f.lift h) (f.mk' a s)) ((f.lift h) (f.mk' b s))
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(B i) ⊆ s

Tactic:
hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff

Goal state after:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, id i ⊆ s) ↔ ∃ i, True ∧ ↑(B i) ⊆ s
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
⊢ toAffine W (-(Q x * P z) • P) = toAffine W P + toAffine W Q

Tactic:
toAffine_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg,

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
⊢ toAffine W P = toAffine W P + toAffine W Q
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
x : K
hx : v x ≠ 0
⊢ v x = 1

Tactic:
lift r to Γ₀ˣ using IsUnit.mk0 _ hr
  rcases lt_trichotomy (Units.mk0 _ hx) 1 with H | H | H
  · obtain ⟨k, hk⟩ := exists_pow_lt H r
    specialize h (x ^ k) (by simp [hx])
    simp [← Units.val_lt_val, ← map_pow, h.not_gt] at hk
  · simpa [Units.ext_iff] using H
  · rw [← inv_lt_one'] at H
    obtain ⟨k, hk⟩ := exists_pow_lt H r
    specialize h (x ^ (-k : ℤ)) (by simp [hx])
    simp only [zpow_neg, zpow_natCast, map_inv₀, map_pow] at h
    simp [← Units.val_lt_val, h.not_gt, inv_pow] at hk

Goal state after:
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 x : R
y : ↥(posSubmonoid R)
h : ValueGroupWithZero.mk x y ≠ 0
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1

Tactic:
rw [ne_eq, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_eq_mk] at h

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
h : ¬(x * ↑1 ≤ᵥ 0 * ↑y ∧ 0 * ↑y ≤ᵥ x * ↑1)
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔ F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
by
  rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
  apply and_congr Iff.rfl
  simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]
  constructor
  · intro h γ
    simp_rw [restrict_lt_iff_lt_embedding]
    exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis γ)
  · rintro h - ⟨γ, rfl⟩
    simp_rw [restrict_lt_iff_lt_embedding] at h
    exact h γ

Goal state after:
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✝
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
x : R
S : Type u_3
Γ : Type u_4
inst✝¹ : Ring S
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x✝¹ y✝ : S
x✝ : v x✝¹ ≤ v y✝
h : S
⊢ v (x✝¹ * h) ≤ v (y✝ * h)

Tactic:
by simp only [map_mul]; gcongr

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ y✝ : R
h : x✝ * y✝ ∈ supp R
⊢ x✝ ∈ supp R ∨ y✝ ∈ supp R

Tactic:
by_contra! h'
    simp only [supp_def, not_vle] at h h'
    exact vlt.not_vle (zero_vlt_mul h'.1 h'.2) h

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
inst✝ : IsNontrivial R
⊢ ∃ γ, 0 < γ ∧ γ < 1

Tactic:
by
  obtain ⟨γ, h0, h1⟩ := IsNontrivial.condition (R := R)
  obtain h1 | h1 := lt_or_lt_iff_ne.mpr h1
  · exact ⟨γ, zero_lt_iff.mpr h0, h1⟩
  · exact ⟨γ⁻¹, by simpa [zero_lt_iff], by simp [inv_lt_one_iff₀, h0, h1]⟩

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) - W'.a₁ * ((-(Q x * P z)) ^ 2 * P x) * addZ P Q -
      W'.a₃ * addZ P Q ^ 3 =
    (-(Q x * P z)) ^ 3 * P y

Tactic:
addZ_of_Z_eq_zero_right hQz

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) -
        W'.a₁ * ((-(Q x * P z)) ^ 2 * P x) * (-(Q x * P z) * P z) -
      W'.a₃ * (-(Q x * P z) * P z) ^ 3 =
    (-(Q x * P z)) ^ 3 * P y
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 Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hγ0 : ↑g ∉ {0}
π : K
hπ : v π = ↑g
⊢ ↑(Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup) = ↑(generator v)

Tactic:
by rw [valueGroup_genLTOne_eq_generator]

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
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬↑π.val ^ n = 0

Tactic:
pow_eq_zero_iff',

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 = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬(↑π.val = 0 ∧ n ≠ 0)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
hr' : 0 < v r
⊢ v s / v r ≠ 0

Tactic:
by simp [hs, hr]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (e 1)
⊢ AddSubgroup.zmultiples (e 1) = AddSubgroup.zmultiples 1

Tactic:
simpa [e.surjective, eq_comm] using (e : ℤ →+ ℤ).map_zmultiples 1

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
b : G
hb : b ∈ closure {x}
⊢ { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
        ⟨a, ha⟩ ≤
      { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
        ⟨b, hb⟩ ↔
    ⟨a, ha⟩ ≤ ⟨b, hb⟩

Tactic:
simp only [hx, closure_singleton_one, mem_bot] at ha hb

Goal state after:
case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha✝ : a ∈ closure {x}
b : G
hb✝ : b ∈ closure {x}
ha : a = 1
hb : b = 1
⊢ { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
        ⟨a, ha✝⟩ ≤
      { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
        ⟨b, hb✝⟩ ↔
    ⟨a, ha✝⟩ ≤ ⟨b, hb✝⟩
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
⊢ ⊤.toAddSubsemigroup = (AddSubgroup.closure {x}).toAddSubsemigroup

Tactic:
by simp [this]

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

Goal state before:
pp: case inr
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
⊢ IsClosed {b | ∃ r, embedding (extension b) = v r}

Tactic:
simp_rw [← hr, ← Valuation.restrict_def, h]

Goal state after:
case inr
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
⊢ IsClosed {b | ∃ r, extension b = v.restrict r}
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
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
⊢ (∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t) ↔ γ₀ < ↑γ

Tactic:
refine ⟨fun hx => ?_, fun hx s hs => ?_⟩

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
⊢ γ₀ < ↑γ

case refine_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
⊢ ∃ y, ↑y ∈ s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
⊢ (fun C_1 ↦ IsIntegral R (C_1 • C • W)) 1

Tactic:
by simp only [one_smul, hC.1]

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]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y

Tactic:
by
  simp only [intValuationDef]
  by_cases hx : x = 0
  · rw [hx, zero_mul, if_pos rfl, zero_mul]
  · by_cases hy : y = 0
    · rw [hy, mul_zero, if_pos rfl, mul_zero]
    · rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← exp_add,
        ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
        Associates.count_mul (Associates.mk_ne_zero'.mpr hx) (Associates.mk_ne_zero'.mpr hy)
          v.associates_irreducible,
        Nat.cast_add]

Goal state after:
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
n : σ →₀ ℕ
⊢ f ((coeff n) 1) = (coeff n) 1

Tactic:
rw [coeff_one, coeff_one]
        split_ifs with h
        · simp only [map_one]
        · simp only [map_zero]

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
x : ↥(nonZeroDivisors R)
⊢ 0 < exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors))

Tactic:
exact WithZero.zero_lt_coe _

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : WithZero (Multiplicative ℤ)
⊢ ∃ a, (valuation K v) a = x

Tactic:
rcases GroupWithZero.eq_zero_or_unit x with (rfl | ⟨x, rfl⟩)

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ∃ a, (valuation K v) a = 0

case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ ↑((MvPolynomial.monomial d) r) = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) ((MvPolynomial.monomial d) r))

Tactic:
have : single () (d ()) = d := by ext; simp
    simp only [MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial,
      Polynomial.coe_monomial, PowerSeries.monomial, 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 Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
hγ : γ ≠ 0
r : hat K
hr : v r = γ
⊢ ¬embedding ((restrict₀ (ofClass v)) r) = embedding 0

Tactic:
embedding_restrict₀ r

Goal state after:
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
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: x✝ : ℕ∞ × ℕ∞
a✝ b✝ : ℕ∞
a b : ℕ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ↑b)

Tactic:
simp [ContinuousAt, nhds_prod_eq]

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: case inl
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (0, ⊤)

Tactic:
simp [ContinuousAt, nhds_prod_eq]

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a✝ b✝ : ℕ∞
h : a✝ ≠ ⊤ ∨ b✝ ≠ ⊤
a b : ℕ
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ↑b)

Tactic:
simp [ContinuousAt, nhds_prod_eq]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ ((monomial d) a).order = ↑((weight fun x ↦ 1) d)

Tactic:
exact weightedOrder_monomial_of_ne_zero _ h

Goal state after:
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 : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
⊢ n ≥ d + Finsupp.single s 1 → (coeff d) ↑((trunc R n) f) = (coeff d) f

Tactic:
hn

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ (coeff d) ↑((trunc R n) f) = (coeff d) f
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.toNat

Tactic:
ENat.natCast_lt_natCast

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.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I

Tactic:
have hR'S : uR' • S ⊆ S := calc
    uR' • S = uR' • (J : Set M) ∪ uR • uR' • (J : Set M) := by simp_rw [S, smul_union, smul_comm]
    _ ⊆ J ∪ uR • J := by gcongr
    _ = S := rfl

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
suffices order (φ + ψ) = order φ by
    rw [le_inf_iff, this]
    exact ⟨le_rfl, le_of_lt H⟩
  rw [order_eq]
  constructor
  · intro i hi
    rw [← hi] at H
    rw [(coeff _).map_add, coeff_of_lt_order i H, add_zero]
    exact (order_eq_nat.1 hi.symm).1
  · intro i hi
    rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
⊢ ↑n < φ.order + ψ.order → (coeff n) (φ * ψ) = 0

Tactic:
hn

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ (coeff n) (φ * ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hf : constantCoeff φ = 0
⊢ ↑n ≤ (φ ^ n).order

Tactic:
refine .trans ?_ (le_order_pow _ n)

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hf : constantCoeff φ = 0
⊢ ↑n ≤ n • φ.order
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∑ p ∈ antidiagonal m, (coeff p.1) ↑((trunc n) f) * (coeff p.2) g = ∑ p ∈ antidiagonal m, (coeff p.1) f * (coeff p.2) g

Tactic:
sum_congr rfl

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ (antidiagonal m).sum ?m.70 = ∑ p ∈ antidiagonal m, (coeff p.1) f * (coeff p.2) g

case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∀ x ∈ antidiagonal m, (coeff x.1) ↑((trunc n) f) * (coeff x.2) g = ?m.70 x

R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ℕ × ℕ → R
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑φ.order.toNat < ↑(φ.order.toNat + 1)

Tactic:
ENat.natCast_lt_natCast

Goal state after:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ φ.order.toNat < φ.order.toNat + 1
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → constantCoeff ((map (Ideal.Quotient.mk I)) f) ^ b = 0
n : ℕ
⊢ N + Finsupp.degree d ≤ n → (coeff d) ((map (Ideal.Quotient.mk I)) (f ^ n)) = 0

Tactic:
hn

Goal state after:
case h
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → constantCoeff ((map (Ideal.Quotient.mk I)) f) ^ b = 0
n : ℕ
hn : N + Finsupp.degree d ≤ n
⊢ (coeff d) ((map (Ideal.Quotient.mk I)) (f ^ n)) = 0