mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ 1 ≤ a⁻¹

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ a ≤ 1
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
⊢ IsLeast {y | y ∈ ⊤ ∧ 0 < y} x

Tactic:
simpa using

Goal state after:
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
⊢ IsLeast {y | 0 < y} x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg.refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x y : G
H : ¬IsLeast {y | 0 < y} (y - x)
hxy : x < y
z : G
hz : 0 < z ∧ z < y - x
⊢ x + z < y

Tactic:
simpa using

Goal state after:
case neg.refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x y : G
H : ¬IsLeast {y | 0 < y} (y - x)
hxy : x < y
z : G
hz : 0 < z ∧ z < y - x
⊢ x + z < y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
h : G ≃+o ℤ
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
simpa using

Goal state after:
case inl
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
h : G ≃+o ℤ
⊢ Nonempty (G ≃+o ℤ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₁
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ ∃ r₁, (algebraMap R K) r₁ = ({ u := 1, r := 0, s := 0, t := 0 } • W).a₁

Tactic:
simpa using

Goal state after:
case h.h₁
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ (valuation R K) W.a₁ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₂
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ ∃ r₂, (algebraMap R K) r₂ = ({ u := 1, r := 0, s := 0, t := 0 } • W).a₂

Tactic:
simpa using

Goal state after:
case h.h₂
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ (valuation R K) W.a₂ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₃
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ ∃ r₃, (algebraMap R K) r₃ = ({ u := 1, r := 0, s := 0, t := 0 } • W).a₃

Tactic:
simpa using

Goal state after:
case h.h₃
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ (valuation R K) W.a₃ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₄
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ ∃ r₄, (algebraMap R K) r₄ = ({ u := 1, r := 0, s := 0, t := 0 } • W).a₄

Tactic:
simpa using

Goal state after:
case h.h₄
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ (valuation R K) W.a₄ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₆
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ ∃ r₆, (algebraMap R K) r₆ = ({ u := 1, r := 0, s := 0, t := 0 } • W).a₆

Tactic:
simpa using

Goal state after:
case h.h₆
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ (valuation R K) W.a₆ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := List.idxOf lmax l
hi : i < l.length
hi₁ : (valuation R K) l₀[i] = l[i]
⊢ (valuation R K) l₀[i] = lmax

Tactic:
simpa using

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := List.idxOf lmax l
hi : i < l.length
hi₁ : (valuation R K) l₀[i] = l[i]
⊢ l[i] = lmax
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
⊢ γ₀' ≠ 0

Tactic:
simpa using

Goal state after:
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
⊢ γ₀' ≠ 0
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
hx : ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
y : K
hy₁ : v y < ↑γ
hy₂ : embedding ((restrict₀ (ofClass v)) y) = embedding γ₀'
⊢ v y = γ₀

Tactic:
simpa using

Goal state after:
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
y : K
hy₁ : v y < ↑γ
hy₂ : embedding ((restrict₀ (ofClass v)) y) = embedding γ₀'
⊢ v y = embedding γ₀'
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
inst✝ : IsMinimal R W
⊢ IsIntegral R W

Tactic:
simpa using

Goal state after:
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
inst✝ : IsMinimal R W
⊢ IsIntegral R W
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
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : ↑y ∈ s
hy₁ : embedding ((restrict₀ (ofClass v)) y) = embedding γ₀'
⊢ v y = γ₀

Tactic:
simpa using

Goal state after:
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 : K
hy₂ : ↑y ∈ s
hy₁ : embedding ((restrict₀ (ofClass v)) y) = embedding γ₀'
⊢ v y = embedding γ₀'
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
hW : IsMinimal R W
h :
  ¬(valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) < 1 ↔
    (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
⊢ IsMinimal R W ∧ (valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) = 1 ↔
    ¬(valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) < 1

Tactic:
simpa using

Goal state after:
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
hW : IsMinimal R W
h :
  ¬(valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) < 1 ↔
    (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
⊢ (integralModel R W).Δ ∉ (IsDiscreteValuationRing.maximalIdeal R).asIdeal ↔
    1 ≤ (valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ)
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 (extensionValuation.restrict ↑⋯.choose) = embedding 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ v ⋯.choose = 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a * (monomial n) b = (monomial (m + n)) (a * b)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (MvPowerSeries.monomial (single () m)) a * (MvPowerSeries.monomial (single () n)) b =
    (MvPowerSeries.monomial (single () m + single () n)) (a * b)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
H : X = 0
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
H : X = 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X) = (coeff n) (ψ * X)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X) = (coeff n) (ψ * X)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : x = 0
⊢ (if h : extensionValuation ↑xy = 0 then 0 else ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩) =
    if h : extensionValuation ↑y = 0 then 0
    else if h : extensionValuation ↑x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simpa using

Goal state after:
case pos
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
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : x = 0
⊢ xy = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X * φ) = (coeff n) (X * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X * φ) = (coeff n) (X * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : y = 0
⊢ (if h : extensionValuation ↑xy = 0 then 0 else ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩) =
    if h : extensionValuation ↑y = 0 then 0
    else if h : extensionValuation ↑x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simpa using

Goal state after:
case pos
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
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : y = 0
⊢ xy = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ a * (coeff (m + n - m)) φ = a * (coeff n) φ

pp: case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n

Tactic:
add_tsub_cancel_left

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ a * (coeff n) φ = a * (coeff n) φ

case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X ^ k) = (coeff n) (ψ * X ^ k)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X ^ k) = (coeff n) (ψ * X ^ k)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X ^ k * φ) = (coeff n) (X ^ k * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X ^ k * φ) = (coeff n) (X ^ k * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) (φ * ψ) = (coeff n) (ψ * φ)

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ = ∑ p ∈ antidiagonal n, (coeff p.1) ψ * (coeff p.2) φ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

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

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

Tactic:
· rw [hx, zero_mul, if_pos rfl, zero_mul]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
m : ℕ
inst✝ : NeZero m
n : σ →₀ ℕ
a : R
i : σ
H : n + single i m = 0
⊢ False

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
m : ℕ
inst✝ : NeZero m
n : σ →₀ ℕ
a : R
i : σ
H : n + single i m = 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
m : ℕ
hm : m < n
⊢ (single () m) () < n

Tactic:
simpa using

Goal state after:
case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
m : ℕ
hm : m < n
⊢ m < n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n) (φ * C a) = (coeff n) φ * a

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n) (φ * C a) = (coeff n) φ * a
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n) (C a * φ) = a * (coeff n) φ

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n) (C a * φ) = a * (coeff n) φ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
h : single s 1 ≤ 0
⊢ False

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
h : single s 1 ≤ 0
⊢ False
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
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
· exact min_le_left _ _

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
⊢ Irreducible (Associates.mk v.asIdeal)