mathlib-initiative/mathlib-tactics huggingface dataset:
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).c₄ = f W.c₄

Tactic:
simp only [c₄, map_b₂, map_b₄]
  map_simp

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ ↑W.Δ'⁻¹ * (W.a₁ ^ 4) ^ 3 = ↑W.Δ'⁻¹ * W.a₁ ^ 12

Tactic:
← pow_mul

Goal state after:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ ↑W.Δ'⁻¹ * W.a₁ ^ (4 * 3) = ↑W.Δ'⁻¹ * W.a₁ ^ 12
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ ↑W.Δ'⁻¹ * (W.b₂ ^ 2) ^ 3 = ↑W.Δ'⁻¹ * W.b₂ ^ 6

Tactic:
← pow_mul

Goal state after:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ ↑W.Δ'⁻¹ * W.b₂ ^ (2 * 3) = ↑W.Δ'⁻¹ * W.b₂ ^ 6
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x)) =
    (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i y)) (U y))) (t y))

Tactic:
ht,

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op)) ((s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯) =
    (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op)) ((s |_ c.π.app (i y) ⁻¹ᵁ U y) ⋯)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x : W'.CoordinateRing
h : (CoordinateRing.basis W').equivFun x 0 • 1 + (CoordinateRing.basis W').equivFun x 1 • (mk W') Y = x
⊢ ∃ p q, p • 1 + q • (mk W') Y = x

Tactic:
exact ⟨_, _, h⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case left.inr
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
i : Fin m →₀ ℕ
j : Fin n
⊢ (MvPolynomial.coeff i
        (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
          (Sum.inr j))).degrees ≤
    Finset.univ.val

Tactic:
simp only [MvPolynomial.algebraMap_eq, Sum.elim_inr, MvPolynomial.coeff_sub,
            MvPolynomial.coeff_C, MvPolynomial.coeff_map, σ]
          refine degrees_sub_le.trans ?_
          simp only [degrees_C, apply_ite, degrees_zero,
            Multiset.union_zero]
          split_ifs with h
          · refine (degrees_X' _).trans ?_
            simp
          · simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticNet W
x : R
p q r s : ℤ
⊢ x • W (p + q + s) * x • W (p - q) * x • W (r + s) * x • W r -
            x • W (p + r + s) * x • W (p - r) * x • W (q + s) * x • W q +
          x • W (q + r + s) * x • W (q - r) * x • W (p + s) * x • W p +
        x ^ 4 * 0 -
      (0 +
        x ^ 4 *
          (W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
            W (q + r + s) * W (q - r) * W (p + s) * W p)) =
    0

Tactic:
smul_eq_mul

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticNet W
x : R
p q r s : ℤ
⊢ x * W (p + q + s) * (x * W (p - q)) * (x * W (r + s)) * (x * W r) -
            x * W (p + r + s) * (x * W (p - r)) * (x * W (q + s)) * (x * W q) +
          x * W (q + r + s) * (x * W (q - r)) * (x * W (p + s)) * (x * W p) +
        x ^ 4 * 0 -
      (0 +
        x ^ 4 *
          (W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
            W (q + r + s) * W (q - r) * W (p + s) * W p)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p • 1 + q • 0) *
        (((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • if 0 = 1 then 1 else 0) +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • 1) -
      ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1 + (p - q * (C W'.a₁ * X + C W'.a₃)) • 0) *
        ((p • if 0 = 1 then 1 else 0) + q • 1) =
    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₆)

Tactic:
smul_eq_mul

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p * 1 + q * 0) *
        ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) * if 0 = 1 then 1 else 0) +
          (p - q * (C W'.a₁ * X + C W'.a₃)) * 1) -
      (q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) * 1 + (p - q * (C W'.a₁ * X + C W'.a₃)) * 0) *
        ((p * if 0 = 1 then 1 else 0) + q * 1) =
    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₆)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.ΨSq (2 * m + 1) =
    ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2

Tactic:
rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ preNormEDS ((mk W) W.ψ₂ ^ 4) ((mk W) (C W.Ψ₃)) ((mk W) (C W.preΨ₄)) n * (mk W) (if Even n then W.ψ₂ else 1) =
    preNormEDS (((mk W) W.ψ₂ ^ 2) ^ 2) ((mk W) (C W.Ψ₃)) ((mk W) (C W.preΨ₄)) n * (mk W) (if Even n then W.ψ₂ else 1)

Tactic:
← pow_mul

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 3 = C X * C W.Ψ₃ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 2

Tactic:
by
  simp [φ, mul_assoc, sq]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (W.toCharThreeNF • W).IsCharThreeJNeZeroNF

Tactic:
toCharThreeNF,

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (({ u := 1, r := (W.toShortNFOfCharThree • W).a₄ / (W.toShortNFOfCharThree • W).a₂, s := 0, t := 0 } *
        W.toShortNFOfCharThree) •
      W).IsCharThreeJNeZeroNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.toCharThreeNF • W).IsShortNF

Tactic:
toCharThreeNF,

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (({ u := 1, r := (W.toShortNFOfCharThree • W).a₄ / (W.toShortNFOfCharThree • W).a₂, s := 0, t := 0 } *
        W.toShortNFOfCharThree) •
      W).IsShortNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_eq_zero.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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJNeZeroNF
⊢ ∃ C, C • E = E'

pp: case of_j_eq_zero.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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'

Tactic:
· have h := (C' • E').j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
      rw [variableChange_j, ← heq, ← variableChange_j E C,
        j_of_isCharTwoJEqZeroNF_of_char_two] at h
      exact False.elim (h rfl)

Goal state after:
case of_j_eq_zero.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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
hQz : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m ↦ m • Q) u z = Q z
⊢ (fun m ↦ m • Q) u = Q

Tactic:
simp only [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors hQz).mp <| one_mul (Q z) ▸ hz]

Goal state after:
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
hQz : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m ↦ m • Q) u z = Q z
⊢ 1 • Q = Q
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
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, 0, 0, 0⟩

Goal state after:
case h
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
ha₄' : E'.a₄ = 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, 0, 0, 0⟩

Goal state after:
case h
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := ⋯
this : Invertible 3 := ⋯
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
ha₄' : E'.a₄ = 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
hu0 : u ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, 0, 0, 0⟩

Goal state after:
case h
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := ⋯
this : Invertible 3 := ⋯
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
hu0 : u ≠ 0
⊢ { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (↑(expCoeff (n + 1)) ^ 2 * if Even (n + 1) then 4 else 1) = ↑(↑(n + 1) ^ 2)

pp: case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ if Even (n + 1) then 3 else 0

Tactic:
hc

Goal state after:
case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (↑(expCoeff (n + 1)) ^ 2 * if Even (n + 1) then 4 else 1) = ↑(expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1)

case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ if Even (n + 1) then 3 else 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case neg
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, 0, 0, 0⟩

Goal state after:
case h
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := ⋯
this : Invertible 3 := ⋯
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

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:
· exact ne_zero_of_natDegree_gt <| W.natDegree_ΨSq_pos hn h

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: 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
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
| ↑1

Tactic:
hc

Goal state after:
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
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
| ↑((1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]

Tactic:
rw [addXYZ, addX_neg hP, addY_neg hP, addZ_neg, smul_fin3]
  simp +decide [fin3_def_ext, Odd.neg_pow]

Goal state after:
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
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)

Tactic:
· exact hk

Goal state after:
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
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) * ↑(B k) ⊆ ↑(B i)

Tactic:
· exact hk

Goal state after:
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
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)

Tactic:
· exact hk

Goal state after:
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
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)

Tactic:
· exact hk

Goal state after: