mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case even.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ ↑(expCoeff (m + 2)) ^ 2 * ↑(expCoeff (m + 3)) * ↑(expCoeff (m + 5)) -
      ↑(expCoeff (m + 1)) * (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) *
        (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) ^ 2 =
    ↑(expCoeff (2 * (m + 3)))

Tactic:
h₃.2,

Goal state after:
case even.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ ↑(expCoeff (m + 2)) ^ 2 * ↑(expCoeff (m + 3)) * ↑(expCoeff (m + 5)) -
      ↑(expCoeff (m + 1)) * ↑(expCoeff (m + 3)) * (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) ^ 2 =
    ↑(expCoeff (2 * (m + 3)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : E.IsElliptic
inst✝¹ : E'.IsElliptic
inst✝ : CharP F 3
heq : E.j = E'.j
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharThreeNF

Goal state after:
case of_j_ne_zero
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝³ : E.IsElliptic
inst✝² : E'.IsElliptic
inst✝¹ : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝ : (C • E).IsCharThreeJNeZeroNF
⊢ ∃ C, C • E = E'

case of_j_eq_zero
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝³ : E.IsElliptic
inst✝² : E'.IsElliptic
inst✝¹ : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝ : (C • E).IsShortNF
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.negY P = -P y

Tactic:
negY,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ -P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3 = -P y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z ^ 3 + (-W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * (P z ^ 3 / P z ^ 3)) -
      (W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3) + (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
negY,

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3) / P z ^ 3 + (-W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * (P z ^ 3 / P z ^ 3)) -
      (W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3) + (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0
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
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) + -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - W'.negY P) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0

Tactic:
negY,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - W'.negY P) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = P y - W.negY P

Tactic:
negY,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = P y - (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ⊆ (fun y ↦ a + y) ⁻¹' s

Tactic:
rintro b b_in

Goal state after:
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ ↑(B i)
⊢ b ∈ (fun y ↦ a + y) ⁻¹' s
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := ⋯
a : A
a_in : a ∈ (B i).carrier
⊢ {b | b - a ∈ B i} ⊆ (B i).carrier

Tactic:
rintro b b_in

Goal state after:
case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := hB.topology
a : A
a_in : a ∈ (B i).carrier
b : A
b_in : b ∈ {b | b - a ∈ B i}
⊢ b ∈ (B i).carrier
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:
linear_combination (norm := (rw [addX, addZ]; ring1)) -Q z ^ 6 * (equation_iff P).mp hP
    - P z ^ 6 * (equation_iff Q).mp hQ

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:
simpa using h

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

Goal state before:
pp: case h
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) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ v y * ↑γx < ↑((Units.map ↑embedding) γ)

Tactic:
Units.val_mul,

Goal state after:
case h
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) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding (↑u⁻¹ * ↑γ)
⊢ v y * ↑γx < ↑((Units.map ↑embedding) γ)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∉ s
⊢ Disjoint (𝓟 s) (𝓝ˢ t)

Tactic:
disjoint_principal_nhdsSet

Goal state after:
case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∉ s
⊢ Disjoint (closure[topologicalSpace] s) t
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ _i.toUniformSpace = IsTopologicalAddGroup.rightUniformSpace R

Tactic:
refine UniformSpace.ext ((hasBasis_uniformity R Γ₀).eq_of_same_basis ?_)
  convert! v.subgroups_basis.hasBasis_nhds_zero.comap _
  simp_rw [restrict_lt_iff_lt_embedding, sub_eq_add_neg]
  simp

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
    induction a using ValueGroupWithZero.ind
    induction b using ValueGroupWithZero.ind
    rw [ValueGroupWithZero.mk_le_mk, ValueGroupWithZero.mk_le_mk]
    apply vle_total

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x : R
h : v x ≠ 0
⊢ {y | v y = v x} ∈ 𝓝 x

Tactic:
v.mem_nhds_iff

Goal state after:
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x : R
h : v x ≠ 0
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {y | v y = v x}
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ {x | v.restrict x < r} ∈ 𝓝 x

Tactic:
v.mem_nhds_iff

Goal state after:
case inr
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x < r}
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
x : R
hx : r < v.restrict x
⊢ {x | v.restrict x ≤ r}ᶜ ∈ 𝓝 x

Tactic:
v.mem_nhds_iff

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
x : R
hx : r < v.restrict x
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x ≤ r}ᶜ
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x = 0}

Tactic:
convert! v.isClosed_closedBall 0 using 3
    simp

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

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ (ofClass v) a * (ofClass v) ↑s < (ofClass v) b * (ofClass v) ↑r

Tactic:
simpa using h

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
hPz : P 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 * Q z +
                                          3 * P x * P y * Q x ^ 2 * P z * 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 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                  W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * P z * Q z ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6 +
        (W'.negY Q - Q y) * Q z ^ 3 * P x ^ 3 -
      ((P x * Q z) ^ 3 * W'.negY Q + (W'.negY Q - Q y) * Q z ^ 3 * P y ^ 2) =
    0

Tactic:
negY,

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 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                          3 * P x * P y * Q x ^ 2 * P z * 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 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                  W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * P z * Q z ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * P z ^ 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: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : {y | y.hatInv = y⁻¹} ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x

Tactic:
exact ContinuousAt.congr (continuous_hatInv x_ne) this

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
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 * Q z +
                                          3 * P x * P y * Q x ^ 2 * P z * 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 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                  W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * P z * Q z ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6 +
        (P y - W'.negY P) * P z ^ 3 * Q x ^ 3 -
      ((-(Q x * P z)) ^ 3 * W'.negY P + (P y - W'.negY P) * P z ^ 3 * Q y ^ 2) =
    0

Tactic:
negY,

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 * Q z +
                                          3 * P x * P y * Q x ^ 2 * P z * 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 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                  W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * P z * Q z ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 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.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
hPz : P z = 0
⊢ -((P x * Q z) ^ 3 * W'.negY Q) - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3 = (P x * Q z) ^ 3 * Q y

Tactic:
negY,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3)) - W'.a₁ * W'.addX P Q * addZ P Q -
      W'.a₃ * addZ P Q ^ 3 =
    (P x * Q z) ^ 3 * Q y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * W'.negY P) - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3 = (-(Q x * P z)) ^ 3 * P y

Tactic:
negY,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) - W'.a₁ * W'.addX P Q * addZ P Q -
      W'.a₃ * addZ P Q ^ 3 =
    (-(Q x * P z)) ^ 3 * P y
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
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q] =
    ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addXYZ P Q y, (u * v) ^ 2 * W'.addXYZ P Q z]

Tactic:
addXYZ_Y,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q] =
    ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * W'.addXYZ P Q z]
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ (↑n + -↑m) ≤ ↑(ofAdd 0)
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ ↑m ≤ ↑n

Tactic:
← sub_eq_add_neg

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ (↑n - ↑m) ≤ ↑(ofAdd 0)
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ ↑m ≤ ↑n
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
Hx : ∀ (z : ↥(closure {x})), z ∈ zpowers ⟨x', ⋯⟩
⊢ ∀ (z : ↥(closure {y})), z ∈ zpowers ⟨y', ⋯⟩

Tactic:
simp_rw [Subtype.forall, hyc, ← zpowers_eq_closure, mem_zpowers_iff, Subtype.ext_iff,
        SubgroupClass.coe_zpow, imp_self, implies_true]

Goal state after: