mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
⊢ ∀ i ∈ Finset.univ, 0 ≤ (c.val i).degree.succ

Tactic:
intros

Goal state after:
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
i✝ : Fin n
a✝ : i✝ ∈ Finset.univ
⊢ 0 ≤ (c.val i✝).degree.succ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₆ = W.a₃ ^ 2 + W.a₆

Tactic:
by
  rw [b₆]
  linear_combination W.a₆ * CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).b₂ = f W.b₂

Tactic:
simp only [b₂, map_a₁, map_a₂]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.a₁ ^ 2 + 4 * f W.a₂ = f (W.a₁ ^ 2 + 4 * W.a₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ -C.r * ↑C.u⁻¹ ^ 2 * ↑C.u ^ 2 + C.r = 0

pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0

Tactic:
· linear_combination -C.r * pow_mul_pow_eq_one 2 C.u.inv_mul

Goal state after:
case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case h₂
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ D₁ n ≤ D₂ n

Tactic:
· exact hD _ n.lt_succ_self

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (C.u ^ 12)⁻¹⁻¹ * W.Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹

Tactic:
inv_inv

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ C.u ^ 12 * W.Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
    -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
by
  rw [addPolynomial_eq, neg_inj, Cubic.prod_X_sub_C_eq, Cubic.toPoly_injective]
  by_cases hx : x₁ = x₂
  · have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
    rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
    rw [equation_iff] at h₁ h₂
    rw [slope_of_Y_ne rfl hy]
    rw [negY, ← sub_ne_zero] at hy
    replace hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0 := by convert! hy using 1; ring
    ext
    · rfl
    · simp only [addX]
      ring1
    · simp [field]
      ring1
    · linear_combination (norm := (simp [field]; ring1)) -h₁
  · rw [equation_iff] at h₁ h₂
    rw [slope_of_X_ne hx]
    simp only [addX]
    grind

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx : eval (W'.addX x₁ x₂ ℓ) (derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0
⊢ W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

Tactic:
rw [Nonsingular, and_iff_right hx', negAddY, polynomialX, polynomialY]
  eval_simp
  contrapose! hx
  rw [addPolynomial, linePolynomial, polynomial]
  eval_simp
  derivative_simp
  simp only [zero_add, add_zero, sub_zero, zero_mul, mul_one]
  eval_simp
  linear_combination (norm := (norm_num1; ring1)) hx.left + ℓ * hx.right

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
      (span
            {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))),
              (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span {XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
← span_pair_add_left_mul _ _ <| -(XClass W <| W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂),

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
      (span
            {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))),
              (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
                (mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  -XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span {XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        (span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)}) *
            span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
← Ideal.sup_mul

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        (span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)})) *
          span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ preNormEDS (b ^ 4) c d k * complEDS₂ b c d k = preNormEDS (b ^ 4) c d (2 * k) * if Even k then 1 else b

Tactic:
by
  rw [complEDS₂, preNormEDS_even]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ C ((Algebra.norm R[X]) (p • 1 + q • (mk W') Y)) - (C p + C q * Y) * (C p + C q * (-Y - C (C W'.a₁ * X + C W'.a₃))) =
    W'.polynomial * C q ^ 2

Tactic:
simp only [norm_smul_basis, polynomial]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ C (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - C (C W'.a₁ * X + C W'.a₃))) =
    (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) * C q ^ 2
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
U : c.pt.Opens
hU : IsAffineOpen U
⊢ ∃ i V, IsAffineOpen V ∧ c.π.app i ⁻¹ᵁ V = U

Tactic:
obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact

Goal state after:
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₁) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)

Tactic:
simp only [add_some hxy]
      exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, Quotient.exact.comp <| congrArg _⟩
  rintro ⟨u, rfl⟩
  simp only [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors hQz).mp <| one_mul (Q z) ▸ hz]
  rw [one_smul]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialZ =
    W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
      (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)

Tactic:
rw [polynomialZ_eq]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P)
      (C W'.a₁ * X * Y + C (3 * W'.a₃) * Y * Z ^ 2 -
        (C (2 * W'.a₂) * X ^ 2 * Z + C (4 * W'.a₄) * X * Z ^ 3 + C (6 * W'.a₆) * Z ^ 5)) =
    W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
      (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
hm : n.natAbs = 0
⊢ W.ΨSq n ≠ 0

Tactic:
push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
⊢ W.ΨSq n ≠ 0

Tactic:
· rcases hm : n.natAbs with _ | m
    · push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h
    · rcases Int.natAbs_eq_iff.mp hm with rfl | rfl <;>
        rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn <;>
        push_cast [hn, ΨSq_neg, ΨSq_one] <;>
        exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

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
u : R
⊢ W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

Tactic:
by
  simp only [dblZ, negY_smul, smul_fin3_ext]
  ring1

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
H : Type u_2
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding ⇑f
U : Set H
hU : U ∈ 𝓝 1
⊢ ⇑f ⁻¹' U ∈ 𝓝 1

Tactic:
apply emb.continuous.tendsto
        rwa [f.map_one]

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 ↦ x1 * x2) a b = v
hy : v ∈ U
⊢ v ∈ ↑U

Tactic:
rw [SetLike.mem_coe]

Goal state after:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 ↦ x1 * x2) a b = v
hy : v ∈ U
⊢ v ∈ U
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
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]

Goal state after:
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 * ↑u * ↑w
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
grw [veq_mul_right_comm (x := s)] at this

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.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case some
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
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ (fromAffine (Affine.Point.some x✝ y✝ h✝)).toAffineLift = Affine.Point.some x✝ y✝ h✝

Tactic:
fromAffine_some,

Goal state after:
case some
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
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ { point := ⟦![x✝, y✝, 1]⟧, nonsingular := ⋯ }.toAffineLift = Affine.Point.some x✝ y✝ h✝
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:
by grw [veq_mul_comm z, veq_mul_mul_mul_comm, mul_assoc]

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 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:
by grw [veq_mul_comm z, veq_mul_mul_mul_comm, mul_assoc]

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

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a b : K
hb : b ≠ 0
⊢ a / b ≤ᵥ 1 ↔ a ≤ᵥ b

Tactic:
by
  simp [div_vle_iff hb]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
inst✝ : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1✝ : γ ≠ 1
h1 : 1 < γ
⊢ ∃ γ, 0 < γ ∧ γ < 1

Tactic:
exact ⟨γ⁻¹, by simpa [zero_lt_iff], by simp [inv_lt_one_iff₀, h0, h1]⟩

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑x + ↑y = ↑y + ↑x

Tactic:
change (x : Completion α) + ↑y = ↑y + ↑x

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑x + ↑y = ↑y + ↑x
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
⊢ W.toAffine.negY (![W.addX P Q, W.negAddY P Q, addZ P Q] x / ![W.addX P Q, W.negAddY P Q, addZ P Q] z ^ 2)
      (![W.addX P Q, W.negAddY P Q, addZ P Q] y / ![W.addX P Q, W.negAddY P Q, addZ P 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:
addX_of_Z_ne_zero hP hQ hPz hQz hx,

Goal state after:
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
⊢ W.toAffine.negY
      (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.addX P Q, W.negAddY P Q, addZ P Q] y / ![W.addX P Q, W.negAddY P Q, addZ P 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))
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
⊢ ∃ ia, ∀ (x_1 : R), Valued.v.restrict x_1 < ↑ia → Valued.v.restrict x_1 < ↑x

Tactic:
have hy₀_ne_zero : y₀ ≠ 0 := by simp [hy₀_def]

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
⊢ ∃ ia, ∀ (x_1 : R), Valued.v.restrict x_1 < ↑ia → Valued.v.restrict x_1 < ↑x