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

Goal state before:
pp: case pos
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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂)
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
· rw [add_of_Y_eq hxy.left hxy.right,
        add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]

Goal state after:
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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂)
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 6 +
        (W.a₁ * P x * P y / P z ^ 5 * 1 + W.a₃ * P y / P z ^ 3 * 1 + W.a₂ * P x ^ 2 / P z ^ 4 * (P z ^ 2 / P z ^ 2) +
            W.a₄ * P x / P z ^ 2 * (P z ^ 4 / P z ^ 4) +
          W.a₆ * (P z ^ 6 / P z ^ 6)) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomial +
        (W.a₁ * P x * P y / P z ^ 5 * (P z / P z) + W.a₃ * P y / P z ^ 3 * (P z ^ 3 / P z ^ 3) +
              W.a₂ * P x ^ 2 / P z ^ 4 * 1 +
            W.a₄ * P x / P z ^ 2 * 1 +
          W.a₆ * 1)) =
    0

Tactic:
rw [eval_polynomial, Affine.evalEval_polynomial]

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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 +
        (W.a₁ * P x * P y / P z ^ 5 * 1 + W.a₃ * P y / P z ^ 3 * 1 + W.a₂ * P x ^ 2 / P z ^ 4 * (P z ^ 2 / P z ^ 2) +
            W.a₄ * P x / P z ^ 2 * (P z ^ 4 / P z ^ 4) +
          W.a₆ * (P z ^ 6 / P z ^ 6)) -
      ((P y / P z ^ 3) ^ 2 + W.toAffine.a₁ * (P x / P z ^ 2) * (P y / P z ^ 3) + W.toAffine.a₃ * (P y / P z ^ 3) -
          ((P x / P z ^ 2) ^ 3 + W.toAffine.a₂ * (P x / P z ^ 2) ^ 2 + W.toAffine.a₄ * (P x / P z ^ 2) +
            W.toAffine.a₆) +
        (W.a₁ * P x * P y / P z ^ 5 * (P z / P z) + W.a₃ * P y / P z ^ 3 * (P z ^ 3 / P z ^ 3) +
              W.a₂ * P x ^ 2 / P z ^ 4 * 1 +
            W.a₄ * P x / P z ^ 2 * 1 +
          W.a₆ * 1)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₄
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (E.a₄ - 0 * E.a₃ + 2 * r * 0 - (0 + r * 0) * 0 + 3 * r ^ 2 - 2 * 0 * 0) = E'.a₄

Tactic:
a₃_of_isShortNF,

Goal state after:
case h.a₄
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * r * 0 - (0 + r * 0) * 0 + 3 * r ^ 2 - 2 * 0 * 0) = E'.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₆
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 6 * (E.a₆ + r * E.a₄ + r ^ 2 * 0 + r ^ 3 - 0 * E.a₃ - 0 ^ 2 - r * 0 * 0) = E'.a₆

Tactic:
a₃_of_isShortNF,

Goal state after:
case h.a₆
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 6 * (E.a₆ + r * E.a₄ + r ^ 2 * 0 + r ^ 3 - 0 * 0 - 0 ^ 2 - r * 0 * 0) = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₆
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 6 * (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * E.a₃ - 0 ^ 2 - 0 * 0 * 0) = E'.a₆

Tactic:
a₃_of_isShortNF,

Goal state after:
case h.a₆
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 6 * (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.preΨ n).natDegree ≤ (n.natAbs ^ 2 - if Even n then 4 else 1) / 2

Tactic:
by
  induction n using Int.negInduction with
  | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
  | neg ih => simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg, ih]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
l : ↥s → ↥s → I
flk : (j₁ j₂ : ↥s) → l j₁ j₂ ⟶ k
hflk :
  ∀ (j₁ j₂ : ↥s),
    (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
l' : I
fl'k : l' ⟶ k
fl'l : (x : ↥s × ↥s) → l' ⟶ l x.1 x.2
hl' : ∀ (x : ↥s × ↥s), fl'l x ≫ flk x.1 x.2 = fl'k
j₁ j₂ : ↥s
⊢ (D.map fl'k ≫ D.map fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) ≤ (D.map (fl'l (j₁, j₂)) ≫ D.map (flk j₁ j₂) ≫ D.map fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂)

Tactic:
simp only [← Functor.map_comp, reassoc_of% hl']

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
l : ↥s → ↥s → I
flk : (j₁ j₂ : ↥s) → l j₁ j₂ ⟶ k
hflk :
  ∀ (j₁ j₂ : ↥s),
    (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
l' : I
fl'k : l' ⟶ k
fl'l : (x : ↥s × ↥s) → l' ⟶ l x.1 x.2
hl' : ∀ (x : ↥s × ↥s), fl'l x ≫ flk x.1 x.2 = fl'k
j₁ j₂ : ↥s
⊢ D.map (fl'k ≫ fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) ≤ D.map (fl'k ≫ fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₄
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (E.a₄ - 0 * E.a₃ + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄

Tactic:
a₃_of_isShortNF,

Goal state after:
case h.a₄
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₄
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (E.a₄ - 0 * E.a₃ + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄

Tactic:
a₃_of_isShortNF,

Goal state after:
case h.a₄
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₆
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 6 * (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * E.a₃ - 0 ^ 2 - 0 * 0 * 0) = E'.a₆

Tactic:
a₃_of_isShortNF,

Goal state after:
case h.a₆
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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 6 * (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case succ.succ.left
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
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3) ((n + 1 + 1) ^ 2)

Tactic:
hd'

Goal state after:
case succ.succ.left
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
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3)
      (expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
by
  rw [neg, negY_smul]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: case e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ (f.mk' a s + f.mk' b s) * (algebraMap A B) ↑s = (algebraMap A B) (a + b)

Tactic:
add_mul,

Goal state after:
case e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ f.mk' a s * (algebraMap A B) ↑s + f.mk' b s * (algebraMap A B) ↑s = (algebraMap A B) (a + b)
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: case convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ v (a + b) * ↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom).domRestrict S) h) s)⁻¹ ≤
    max (v a) (v b) * ↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom).domRestrict S) h) s)⁻¹

Tactic:
v.map_add a b

Goal state after:
case convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a b : A
s : ↥S
⊢ max (v a) (v b) * ↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom).domRestrict S) h) s)⁻¹ ≤
    max (v a) (v b) * ↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom).domRestrict S) h) s)⁻¹
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
hx : P x * Q z ^ 2 = Q x * P 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 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Tactic:
addZ_of_X_eq hx

Goal state after:
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
⊢ (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 * 0 -
          W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
        P x * Q z ^ 2 * 0 ^ 2 -
      Q x * P z ^ 2 * 0 ^ 2 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
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
H : ∀ {s : Set R} {x : R}, s ∈ 𝓝 x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
s : Set R
x : R
x✝ : ∃ γ, (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ} ⊆ s
γ : (ValueGroupWithZero R)ˣ
hγ : (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ} ⊆ s
⊢ {z | v.restrict (z - x) < ↑(Units.mk0 ((orderMonoidIso v) ↑γ) ⋯)} ⊆ (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ}

Tactic:
simp [neg_add_eq_sub]

Goal state after: