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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ ⟦P⟧ = ⟦P⟧

Tactic:
]

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
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] = ![W.dblX P, W.dblY P, W.dblZ P]

Tactic:
]

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ ⟦![1, 1, 0]⟧ = ⟦![1, 1, 0]⟧

Tactic:
]

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ ⟦![1, 1, 0]⟧ = ⟦![1, 1, 0]⟧

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * 0 ^ 2 = P x * Q z * Q z

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * 0 ^ 2 = P x * Q z * Q z
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.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)
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ ⟦![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]⟧ =
    ⟦![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:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * 0 ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * 0 ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z
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
this : TopologicalSpace M := hB.topology
⊢ ∀ x ∈ (B i).toAddSubgroup.carrier, (B i).toAddSubgroup.carrier ∈ 𝓝 x

Tactic:
]

Goal state after:
ι : 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
this : TopologicalSpace M := hB.topology
⊢ ∀ x ∈ (B i).toAddSubgroup.carrier, (B i).toAddSubgroup.carrier ∈ 𝓝 x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
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)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ ⟦![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]⟧ =
    ⟦![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:
]

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
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ ∃ i_1 ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis, (fun y ↦ a + y) '' i_1 ⊆ (B i).toAddSubgroup.carrier

Tactic:
]

Goal state after:
ι : 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
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ ∃ i_1 ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis, (fun y ↦ a + y) '' i_1 ⊆ (B i).toAddSubgroup.carrier
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 * Q z ^ 2 = Q x * P z ^ 2

Tactic:
]

Goal state after:
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 * Q z ^ 2 = Q x * P z ^ 2
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
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

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
⊢ Affine.Point.some (P x / P z ^ 2) (P y / P z ^ 3) ⋯ = Affine.Point.some (P x / P z ^ 2) (P y / P z ^ 3) ⋯

Tactic:
]

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z ^ 2 = P x / P z ^ 2 ∧ (u • P) y / (u • P) z ^ 3 = P y / P z ^ 3

Tactic:
]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z ^ 2 = P x / P z ^ 2 ∧ (u • P) y / (u • P) z ^ 3 = P y / P z ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

Tactic:
]

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 y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2))

Tactic:
]

Goal state after:
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 y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case mp
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
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ F ×ˢ F ≤ uniformity G

Tactic:
]

Goal state after:
case mp
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
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ F ×ˢ F ≤ uniformity G
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: case mpr
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
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
]

Goal state after:
case mpr
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
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
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
⊢ map (fun x ↦ x.2 - x.1) (F ×ˢ F) ≤ nhds 0 ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := B.uniformSpace
this : IsUniformAddGroup G
⊢ map (fun x ↦ x.2 - x.1) (F ×ˢ F) ≤ nhds 0 ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

Tactic:
]

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)
⊢ Affine.Point.some
      (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)))
      ⋯ =
    Affine.Point.some
      (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)))
      ⋯

Tactic:
]

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
⊢ toAffine W (W.add P Q) = toAffine W Q

Tactic:
]

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
⊢ toAffine W (W.add P Q) = toAffine W Q
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
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 Q = toAffine W Q

Tactic:
]

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 P = toAffine W P

Tactic:
]

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ (P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                        W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                      2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                    W'.a₃ * Q y * P z ^ 4 * Q z -
                  W'.a₃ * P y * P z * Q z ^ 4 +
                W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
            2 * W'.a₆ * P z ^ 4 * Q z ^ 4) *
          (P z * Q z) ^ 2 +
        (-Q z ^ 6 * 0 +
          P z ^ 6 *
            (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6))) -
      ((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 * (P x * Q z ^ 2 - Q x * P z ^ 2) -
              W'.a₂ * P z ^ 2 * Q z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2 -
            P x * Q z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2 -
          Q x * P z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2 +
        (-Q z ^ 6 *
            (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) +
          P z ^ 6 * 0)) =
    0

Tactic:
]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ (P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                        W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                      2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                    W'.a₃ * Q y * P z ^ 4 * Q z -
                  W'.a₃ * P y * P z * Q z ^ 4 +
                W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
            2 * W'.a₆ * P z ^ 4 * Q z ^ 4) *
          (P z * Q z) ^ 2 +
        (-Q z ^ 6 * 0 +
          P z ^ 6 *
            (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6))) -
      ((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 * (P x * Q z ^ 2 - Q x * P z ^ 2) -
              W'.a₂ * P z ^ 2 * Q z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2 -
            P x * Q z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2 -
          Q x * P z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2 +
        (-Q z ^ 6 *
            (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) +
          P z ^ 6 * 0)) =
    0
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
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.add P Q) = 0

Tactic:
]

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
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.add P Q) = 0
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
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ 0 = 0

Tactic:
]

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

Goal state before:
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
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y * x ≤ᵥ z * x
⊢ y ≤ᵥ z

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y * x ≤ᵥ z * x
⊢ y ≤ᵥ z
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y ≤ᵥ z

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y ≤ᵥ z
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y * x ≤ᵥ z * x

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y * x ≤ᵥ z * x
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y ≤ᵥ z

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y ≤ᵥ z
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 * (z * y) =ᵥ x * (z * y)

Tactic:
]

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

Goal state before:
pp: case inr.inr
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
⊢ v x = 1

Tactic:
]

Goal state after:
case inr.inr
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
⊢ v x = 1
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 * z * (y * w) =ᵥ x * z * (y * w)

Tactic:
]

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : x * y ≤ᵥ 0
⊢ y ≤ᵥ 0
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 : y * x ≤ᵥ 0 * x
⊢ y ≤ᵥ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : y * x ≤ᵥ 0 * x
⊢ y ≤ᵥ 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
this : 0 <ᵥ ↑x
⊢ ↑x ≠ 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
]

Goal state after:
case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑w * ↑v ≤ᵥ t * ↑u * ↑v
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
]

Goal state after:
case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑w * ↑v ≤ᵥ t * ↑u * ↑v
⊢ r * ↑w ≤ᵥ t * ↑u