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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hP : W.NonsingularLift P
hQ : W.NonsingularLift Q
⊢ W.NonsingularLift (W.addMap P Q)

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : ¬W.Nonsingular P
⊢ toAffine W P = 0

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z = 0
⊢ toAffine W P = 0

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ P x / P z ^ 2 ≠ Q x / Q z ^ 2

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
⊢ toAffine W P = Affine.Point.some (P x / P z ^ 2) (P y / P z ^ 3) ⋯

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
X Y : F
h : W.Nonsingular ![X, Y, 1]
⊢ toAffine W ![X, Y, 1] = Affine.Point.some X Y ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := hB.topology
⊢ IsOpen[hB.topology] (B i).toAddSubgroup.carrier

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ NonarchimedeanAddGroup M

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q

Tactic:
by

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ toAffine W (W.add P Q) = toAffine W Q

pp: case neg
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 (W.add P Q) = toAffine W Q

Tactic:
· rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]

Goal state after:
case neg
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 (W.add P Q) = toAffine W Q
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
⊢ 0 ≤ᵥ x

Tactic:
by

Goal state after:
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 Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
H : Units.mk0 (v x) hx < 1
k : ℕ
hk : Units.mk0 (v x) hx ^ k < r
⊢ v (x ^ k) ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
⊢ ¬x <ᵥ 0

Tactic:
by

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
⊢ y ≠ 0

Tactic:
by

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 z : R
hx : 0 <ᵥ x
⊢ x * y ≤ᵥ x * z ↔ y ≤ᵥ z

Tactic:
by

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 z : R
⊢ x * y * z =ᵥ x * z * y

Tactic:
by

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 z w : R
⊢ x * y * (z * w) =ᵥ x * z * (y * w)

Tactic:
by

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
hx : 0 <ᵥ x
hy : 0 <ᵥ y
⊢ 0 <ᵥ x * y

Tactic:
by

Goal state after:
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 Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
H : (Units.mk0 (v x) hx)⁻¹ < 1
k : ℕ
hk : (Units.mk0 (v x) hx)⁻¹ ^ k < r
⊢ v (x ^ (-↑k)) ≠ 0

Tactic:
by

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
u : ↥(posSubmonoid R)
⊢ x * ↑u ≤ᵥ y * ↑u ↔ x ≤ᵥ y

Tactic:
by

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
u : ↥(posSubmonoid R)
⊢ ↑u * x ≤ᵥ ↑u * y ↔ x ≤ᵥ y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ ↑x ≠ 0

Tactic:
by

Goal state after:
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:
by

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
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.addX P Q * (P z * Q z) ^ 2 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q -
          W'.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 -
        P x * Q z ^ 2 * addZ P Q ^ 2 -
      Q x * P z ^ 2 * addZ P Q ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i j : (ofClass v).ValueGroup₀ˣ),
    ∃ k,
      v.ltAddSubgroup ((Units.map ↑embedding) k) ≤
        v.ltAddSubgroup ((Units.map ↑embedding) i) ⊓ v.ltAddSubgroup ((Units.map ↑embedding) j)

Tactic:
by

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
⊢ ∀ {x y z : R × ↥(posSubmonoid R)},
    (match x with
      | (x, s) =>
        match y with
        | (y, t) => x * ↑t ≤ᵥ y * ↑s ∧ y * ↑s ≤ᵥ x * ↑t) →
      (match y with
        | (x, s) =>
          match z with
          | (y, t) => x * ↑t ≤ᵥ y * ↑s ∧ y * ↑s ≤ᵥ x * ↑t) →
        match x with
        | (x, s) =>
          match z with
          | (y, t) => x * ↑t ≤ᵥ y * ↑s ∧ y * ↑s ≤ᵥ x * ↑t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : ValueGroupWithZero.mk x y = 0
⊢ x ≤ᵥ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : x ≤ᵥ 0
⊢ x * ↑1 ≤ᵥ 0 * ↑y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : x ≤ᵥ 0
⊢ 0 * ↑y ≤ᵥ x * ↑1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ ↑x * ↑1 ≤ᵥ 1 * ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ 1 * ↑x ≤ᵥ ↑x * ↑1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ 1 * ↑1 ≤ᵥ 1 * ↑1

Tactic:
by

Goal state after:
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
⊢ W.addX P Q =
    ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q -
            W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 -
          P x * Q z ^ 2 * addZ P Q ^ 2 -
        Q x * P z ^ 2 * addZ P Q ^ 2) /
      (P z * Q z) ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x y = 1 ↔ x ≤ᵥ ↑y ∧ ↑y ≤ᵥ x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : (ofClass v).ValueGroup₀ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in : v.restrict r < ↑γ₀
s : R
s_in : v.restrict s < ↑γ₀
⊢ v.restrict r * v.restrict s < ↑γ₀ * ↑γ₀

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i : (ofClass v).ValueGroup₀ˣ),
    ∃ j,
      ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) * ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
        ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))

Tactic:
by

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
⊢ ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)),
    x * ↑t ≤ᵥ y * ↑s →
      y * ↑s ≤ᵥ x * ↑t →
        z * ↑u ≤ᵥ w * ↑v →
          w * ↑v ≤ᵥ z * ↑u → ValueGroupWithZero.mk (x * z) (s * v) = ValueGroupWithZero.mk (y * w) (t * u)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
α : Type u_2
inst✝ : Mul α
f : R → ↥(posSubmonoid R) → α
hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
a b : ValueGroupWithZero R
⊢ ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ (restrict₀ (ofClass v)) x ≠ 0

Tactic:
by

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
a b c : ValueGroupWithZero R
⊢ a * b * c = a * (b * c)

Tactic:
by

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
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), 1 * ValueGroupWithZero.mk x y = ValueGroupWithZero.mk x y

Tactic:
by

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
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y * 1 = ValueGroupWithZero.mk x y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
⊢ embedding ↑u⁻¹ = ↑γx⁻¹

Tactic:
by

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
u v : R
⊢ W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q

Tactic:
by

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
n : ℕ
⊢ ∀ (x y : R) (t s : ↥(posSubmonoid R)),
    x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → ValueGroupWithZero.mk (x ^ n) (s ^ n) = ValueGroupWithZero.mk (y ^ n) (t ^ n)

Tactic:
by

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
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y ^ 0 = 1

Tactic:
by

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
n : ℕ
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.mk x y ^ (n + 1) = ValueGroupWithZero.mk x y ^ n * ValueGroupWithZero.mk x y

Tactic:
by

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

Goal state before:
pp: 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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
by

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
a b : ValueGroupWithZero R
⊢ a * b = b * a

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift

Tactic:
by

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
x✝ : ↥(posSubmonoid R)
⊢ 0 * ValueGroupWithZero.mk x✝¹ x✝ = 0

Tactic:
by

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
x✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ x✝ * 0 = 0

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
⊢ Function.LeftInverse fromAffine toAffineLift

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
⊢ Function.RightInverse fromAffine toAffineLift

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝² x✝¹ x✝ : W.Point
⊢ x✝² + x✝¹ + x✝ = x✝² + (x✝¹ + x✝)

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ 0 + x✝ = x✝

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
P : W.Point
⊢ -P + P = 0

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝¹ x✝ : W.Point
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (i : (ofClass v).ValueGroup₀ˣ),
    ∃ j,
      ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
        (fun x_1 ↦ x * x_1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))

Tactic:
by

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

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg (⇑f ∘ P) = ⇑f ∘ (W'⁄A).neg P

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P P = 0

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'⁄F).add P Q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ 𝓝 = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ 𝓝 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)

Tactic:
by

Goal state after: