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

Goal state before:
pp: case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)

Tactic:
;

Goal state after:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)
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.RingTheory.Valuation.ValuativeRel.Basic

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
h : x <ᵥ 0
⊢ False
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
⊢ ¬(if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) = 0

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ¬(if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) = 0
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.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ 0) (b ^ 0)) ⋯ (ValueGroupWithZero.mk x y) = 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ 0) (b ^ 0)) ⋯ (ValueGroupWithZero.mk x y) = 1
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.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) ⋯
        (ValueGroupWithZero.mk x y) =
      ValueGroupWithZero.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) ⋯ (ValueGroupWithZero.mk x y) *
        ValueGroupWithZero.mk x y

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
n : ℕ
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) ⋯
        (ValueGroupWithZero.mk x y) =
      ValueGroupWithZero.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) ⋯ (ValueGroupWithZero.mk x y) *
        ValueGroupWithZero.mk x y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
;

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * P y * P z * P z + P x ^ 2 * P x * P z ^ 2 - W'.a₁ * P x * P y * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * P y * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (0 +
        -2 * P z ^ 2 *
          (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))) =
    0
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 y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ y * ↑u * ↑s * z =ᵥ y * ↑s * (z * ↑u)

Tactic:
veq_mul_comm z,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ y * ↑u * ↑s * z =ᵥ y * ↑s * (↑u * z)
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 y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ w * ↑t * (z * ↑s) =ᵥ w * ↑t * ↑s * z

Tactic:
veq_mul_comm z,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ w * ↑t * (↑s * z) =ᵥ w * ↑t * ↑s * z
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ofClass v).ValueGroup₀ˣ
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s

Tactic:
;

Goal state after:
R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ofClass v).ValueGroup₀ˣ
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s
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 y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ y * ↑s * (z * ↑u) =ᵥ y * ↑u * (↑s * z)

Tactic:
veq_mul_comm z,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ y * ↑s * (↑u * z) =ᵥ y * ↑u * (↑s * z)
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
x✝ : R
⊢ (valuation R) (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r) ↔ v.restrict (x✝ - x) < ↑r

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
x✝ : R
⊢ (valuation R) (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r) ↔ v.restrict (x✝ - x) < ↑r
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
x✝ : R
⊢ v.restrict (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r) ↔ (valuation R) (x✝ - x) < ↑r

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
x✝ : R
⊢ v.restrict (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r) ↔ (valuation R) (x✝ - x) < ↑r
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk 0 1 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk 0 1 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
x✝² x' y y' z : R✝
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
x : R
S : Type u_3
Γ : Type u_4
inst✝¹ : Ring S
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x✝¹ y✝ : S
x✝ : v x✝¹ ≤ v y✝
h : S
⊢ v x✝¹ * v h ≤ v y✝ * v h

Tactic:
;

Goal state after:
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
x✝² x' y y' z : R✝
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
x : R
S : Type u_3
Γ : Type u_4
inst✝¹ : Ring S
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x✝¹ y✝ : S
x✝ : v x✝¹ ≤ v y✝
h : S
⊢ v x✝¹ * v h ≤ v y✝ * v h
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
this : x ≤ᵥ y ∨ y ≤ᵥ x
⊢ x <ᵥ y ↔ x ≤ᵥ y ∧ ¬y ≤ᵥ x

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
this : x ≤ᵥ y ∨ y ≤ᵥ x
⊢ x <ᵥ y ↔ x ≤ᵥ y ∧ ¬y ≤ᵥ x
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ x✝ : R
⊢ ((fun x ↦ x₀ + x) ∘ fun x ↦ -x₀ + x) x✝ = _root_.id x✝

Tactic:
;

Goal state after:
case refine_3
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ x✝ : R
⊢ ((fun x ↦ x₀ + x) ∘ fun x ↦ -x₀ + x) x✝ = _root_.id x✝
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id

Tactic:
;

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
x✝ : ↥K
⊢ (⇑i ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑i) x✝

Tactic:
;

Goal state after:
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
x✝ : ↥K
⊢ (⇑i ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑i) x✝
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
hPz : P z = 0
⊢ -P y * Q x ^ 3 * 0 ^ 3 + 2 * P y * Q y ^ 2 * 0 ^ 3 - 3 * P x ^ 2 * Q x * Q y * 0 ^ 2 * Q z +
                                          3 * P x * P y * Q x ^ 2 * 0 * Q z ^ 2 +
                                        P x ^ 3 * Q y * Q z ^ 3 -
                                      2 * P y ^ 2 * Q y * Q z ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * 0 ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * 0 ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * 0 * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * 0 ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * 0 * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * 0 ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * 0 ^ 6 * Q z -
                  W'.a₄ * P x * Q y * 0 ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * 0 ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * 0 * Q z ^ 6 -
            2 * W'.a₆ * Q y * 0 ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * 0 ^ 3 * Q z ^ 6 +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P x ^ 3 -
      ((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P y ^ 2) =
    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
hPz : P z = 0
⊢ -P y * Q x ^ 3 * 0 ^ 3 + 2 * P y * Q y ^ 2 * 0 ^ 3 - 3 * P x ^ 2 * Q x * Q y * 0 ^ 2 * Q z +
                                          3 * P x * P y * Q x ^ 2 * 0 * Q z ^ 2 +
                                        P x ^ 3 * Q y * Q z ^ 3 -
                                      2 * P y ^ 2 * Q y * Q z ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * 0 ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * 0 ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * 0 * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * 0 ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * 0 * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * 0 ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * 0 ^ 6 * Q z -
                  W'.a₄ * P x * Q y * 0 ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * 0 ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * 0 * Q z ^ 6 -
            2 * W'.a₆ * Q y * 0 ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * 0 ^ 3 * Q z ^ 6 +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P x ^ 3 -
      ((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P y ^ 2) =
    0
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
x✝ : α
⊢ (⇑f ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑f) x✝

Tactic:
;

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
x✝ : α
⊢ (⇑f ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑f) x✝
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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * 0 +
                                          3 * P x * P y * Q x ^ 2 * P z * 0 ^ 2 +
                                        P x ^ 3 * Q y * 0 ^ 3 -
                                      2 * P y ^ 2 * Q y * 0 ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * 0 -
                                W'.a₁ * P x * P y * Q y * P z * 0 ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * 0 ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * 0 +
                          2 * W'.a₂ * P x * P y * Q x * P z * 0 ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * 0 ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * 0 -
                  W'.a₄ * P x * Q y * P z ^ 4 * 0 ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * 0 ^ 4 +
              W'.a₄ * P x * P y * P z * 0 ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * 0 ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * 0 ^ 6 +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * P z ^ 3 * Q x ^ 3 -
      ((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * P z ^ 3 * Q y ^ 2) =
    0

Tactic:
;

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * 0 +
                                          3 * P x * P y * Q x ^ 2 * P z * 0 ^ 2 +
                                        P x ^ 3 * Q y * 0 ^ 3 -
                                      2 * P y ^ 2 * Q y * 0 ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * 0 -
                                W'.a₁ * P x * P y * Q y * P z * 0 ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * 0 ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * 0 +
                          2 * W'.a₂ * P x * P y * Q x * P z * 0 ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * 0 ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * 0 -
                  W'.a₄ * P x * Q y * P z ^ 4 * 0 ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * 0 ^ 4 +
              W'.a₄ * P x * P y * P z * 0 ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * 0 ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * 0 ^ 6 +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * P z ^ 3 * Q x ^ 3 -
      ((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * P z ^ 3 * Q y ^ 2) =
    0
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v π = ↑(IsRankOneDiscrete.generator v)
⊢ 0 < v π

Tactic:
;

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v π = ↑(IsRankOneDiscrete.generator v)
⊢ 0 < v π
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
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * 0 ^ 3) * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    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
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * 0 ^ 3) * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0