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

Goal state before:
pp: case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
a✝ : G
⊢ a✝ ∈ {x | -g ≤ x} → ∀ b ∈ {x | -g ≤ x}, a✝ < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ -x) a✝ b

Tactic:
simp [Function.onFun, neg_le]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | x ≤ g} → (fun x ↦ -x) x✝ ∈ {x | -g ≤ x}

Tactic:
simp [Function.onFun, neg_le]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ -x) a✝ b

Tactic:
simp [Function.onFun, neg_le]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
]

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
⊢ x = 0 ↔ x = 0

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
]

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
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
a b : (ofClass v).ValueGroup₀
⊢ a = b ↔ a = b

Tactic:
]

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) = embedding ((restrict₀ (ofClass v)) r)}

Tactic:
← Valuation.restrict_def,

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, embedding (extension b) = embedding (v.restrict r)}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ Nonempty (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
]

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ Nonempty (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : G₀ˣ
⊢ ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a✝) ≤
      ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b✝) ↔
    a✝ ≤ b✝

Tactic:
]

Goal state after:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : G₀ˣ
⊢ ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a✝) ≤
      ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b✝) ↔
    a✝ ≤ b✝
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
⊢ (({x | g ≤ x} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
]

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
⊢ (({x | g ≤ x} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
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:
]

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
⊢ (∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t) ↔ γ₀ < ↑γ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ (({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
]

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ (({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: 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
y : K
hy₁ : v y < ↑γ
hy₂ : v y = γ₀
⊢ v y < ↑γ

Tactic:
]

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
y : K
hy₁ : v y < ↑γ
hy₂ : v y = γ₀
⊢ v y < ↑γ
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
h : IsIntegral R W
r : R
hr : (algebraMap R K) r = W.Δ
⊢ (valuation K (maximalIdeal R)) ((algebraMap R K) r) ≤ 1

Tactic:
]

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
h : IsIntegral R W
r : R
hr : (algebraMap R K) r = W.Δ
⊢ (valuation K (maximalIdeal R)) ((algebraMap R K) r) ≤ 1
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
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
⊢ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
    (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1

Tactic:
]

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
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
⊢ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
    (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1
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
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : (fun C ↦ valuation_Δ_aux R (C • W)) C ≤ (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) →
  (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) ≤ (fun C ↦ valuation_Δ_aux R (C • W)) C :=
  hC.right hj
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)

Tactic:
]

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
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : (fun C ↦ valuation_Δ_aux R (C • W)) C ≤ (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) →
  (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) ≤ (fun C ↦ valuation_Δ_aux R (C • W)) C :=
  hC.right hj
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: 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
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hx : v y < ↑γ
hy₂ : ↑y ∈ s
hy₁ : v y = γ₀
⊢ ∃ y, ↑y ∈ s

Tactic:
]

Goal state after:
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
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hx : v y < ↑γ
hy₂ : ↑y ∈ s
hy₁ : v y = γ₀
⊢ ∃ 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
inst✝ : IsMinimal R W
⊢ IsMinimal R W ∧ (valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) = 1 ∨
    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).c₄) = 1 ∨
      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).c₄) < 1

Tactic:
]

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
⊢ IsMinimal R W ∧ (valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) = 1 ∨
    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).c₄) = 1 ∨
      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).c₄) < 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 Γ₀
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)) ⋯.choose = 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:
]

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

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)) ⋯.choose = a * b
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑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 Γ₀
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

Tactic:
]

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.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.single R (fun x ↦ R) n = LinearMap.single R (fun x ↦ R) n

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.single R (fun x ↦ R) n = LinearMap.single R (fun x ↦ R) n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (if m = n then a else 0) = if m = n then a else 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Unit →₀ ℕ
n : ℕ
h : s () = n
⊢ MvPowerSeries.coeff s = MvPowerSeries.coeff s

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (coeff ?m.21) φ = (coeff ?m.21) ψ

pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.21

pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ ℕ

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (coeff ?m.21) φ = (coeff ?m.21) ψ

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.21

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ ℕ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m = n then a else 0) = if m = n then a else 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.coeff 0) = ⇑constantCoeff

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.coeff 0) = ⇑constantCoeff
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n) ((LinearMap.single R (fun x ↦ R) n) a) = a

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n) ((LinearMap.single R (fun x ↦ R) n) a) = a
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = constantCoeff φ

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ⇑MvPowerSeries.C = ⇑C

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑MvPowerSeries.C = ⇑C
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff m) ((LinearMap.single R (fun x ↦ R) n) a) = 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff m) ((LinearMap.single R (fun x ↦ R) n) a) = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ (if n = 0 then a else 0) = if n = 0 then a else 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ a = a

Tactic:
]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ antidiagonal n = antidiagonal n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
h : n ≠ 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (if n = 1 then 1 else 0) = if n = 1 then 1 else 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
⊢ (if m = n then 1 else 0) = if m = n then 1 else 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ x ∈ antidiagonal n,
      (MvPowerSeries.coeff (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).1) φ *
        (MvPowerSeries.coeff (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).2) ψ =
    ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ x ∈ antidiagonal n,
      (MvPowerSeries.coeff (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).1) φ *
        (MvPowerSeries.coeff (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).2) ψ =
    ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ
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
this : ∀ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ ≠ 0 → p.1 = n
⊢ (if n ≤ m then ∑ x ∈ {(n, m - n)}, (coeff x.1) ((monomial n) a) * (coeff x.2) φ
    else ∑ x ∈ ∅, (coeff x.1) ((monomial n) a) * (coeff x.2) φ) =
    if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ ≠ 0 → p.1 = n
⊢ (if n ≤ m then ∑ x ∈ {(n, m - n)}, (coeff x.1) ((monomial n) a) * (coeff x.2) φ
    else ∑ x ∈ ∅, (coeff x.1) ((monomial n) a) * (coeff x.2) φ) =
    if n ≤ m then a * (coeff (m - n)) φ else 0
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)) φ

Tactic:
]

Goal state after: