mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (2 * 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₃ * 1) -
      (2 * (P y / P z ^ 3) + W.toAffine.a₁ * (P x / P z ^ 2) + W.toAffine.a₃ +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0

Tactic:
;

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * 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₃ * 1) -
      (2 * (P y / P z ^ 3) + W.toAffine.a₁ * (P x / P z ^ 2) + W.toAffine.a₃ +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0
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 ≫ fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) ≤ D.map (fl'k ≫ fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂)

Tactic:
;

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.DivisionPolynomial.Degree

Goal state before:
pp: 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 : ℕ
⊢ (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0

Tactic:
push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast n.succ_ne_zero]

Goal state after:
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 : ℕ
⊢ ↑n ^ 2 + 2 * ↑n * 1 = (↑n ^ 2 + 2 * ↑n * 1 + 1 - if Even n.succ then 4 else 1) + if Even (n + 1) then 3 else 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: 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
⊢ ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1

Tactic:
push_cast [← @Int.cast_inj ℚ, expCoeff_cast]

Goal state after:
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
⊢ (↑n + 1) ^ 2 = (if Even (n + 1) then (↑n + 1) / 2 else ↑n + 1) ^ 2 * if Even (n + 1) then 4 else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (↑hu.unit⁻¹ • u • P)

Tactic:
rwa [smul_smul, hu.val_inv_mul, one_smul]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0
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
⊢ (-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)) -
      (-(P y / P z ^ 3) - W.toAffine.a₁ * (P x / P z ^ 2) - W.toAffine.a₃ +
        (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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 - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x * Q z ^ 2) = f (Q x * P z ^ 2)

Tactic:
;

Goal state after:
case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x * Q z ^ 2) = f (Q x * P z ^ 2)
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
⊢ 2 * 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)

Tactic:
;

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
⊢ 2 * 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)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y * Q z ^ 3) = f (Q y * P z ^ 3)

Tactic:
;

Goal state after:
case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y * Q z ^ 3) = f (Q y * P z ^ 3)
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
i : I
⊢ CompactSpace ↥(D.obj i).left

Tactic:
;

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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
i : I
⊢ CompactSpace ↥(D.obj i).left
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
i : I
⊢ QuasiSeparatedSpace ↥(D.obj i).left

Tactic:
;

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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
i : I
⊢ QuasiSeparatedSpace ↥(D.obj i).left
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
i j : I
f : i ⟶ j
⊢ IsAffineHom (Over.Hom.left (D.map f))

Tactic:
;

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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
i j : I
f : i ⟶ j
⊢ IsAffineHom (Over.Hom.left (D.map f))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * 0 * (P y - -P y) - W'.a₂ * 0 ^ 2 * (P y - -P y) ^ 2 -
          2 * P x * (P y - -P y) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0

Tactic:
;

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * 0 * (P y - -P y) - W'.a₂ * 0 ^ 2 * (P y - -P y) ^ 2 -
          2 * P x * (P y - -P y) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
g : ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).pt
x✝ : I
⊢ (((Over.forget S).mapCone c.unop).π ≫ { app := fun x ↦ (D.obj x).hom, naturality := ⋯ }).app x✝ =
    ((Functor.const I).map (Over.Hom.left g ≫ X.hom)).app x✝

Tactic:
;

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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
g : ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).pt
x✝ : I
⊢ (((Over.forget S).mapCone c.unop).π ≫ { app := fun x ↦ (D.obj x).hom, naturality := ⋯ }).app x✝ =
    ((Functor.const I).map (Over.Hom.left g ≫ X.hom)).app x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

Tactic:
;

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z +
                          P x ^ 2 * P x * P z ^ 2 -
                        W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      ((P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : toAdd (unzero hm) = 0
⊢ m = 1

Tactic:
toAdd_eq_zero

Goal state after:
case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ m = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * ((P x ^ 2) ^ 2 - P x * (P y - -P y) ^ 2) + P y * (P y - -P y) ^ 3 +
        (8 * P y ^ 2 - 4 * P x ^ 3) * P x ^ 3 -
      (-(P x ^ 2) ^ 3 + (8 * P y ^ 2 - 4 * P x ^ 3) * P y ^ 2) =
    0

Tactic:
;

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * ((P x ^ 2) ^ 2 - P x * (P y - -P y) ^ 2) + P y * (P y - -P y) ^ 3 +
        (8 * P y ^ 2 - 4 * P x ^ 3) * P x ^ 3 -
      (-(P x ^ 2) ^ 3 + (8 * P y ^ 2 - 4 * P x ^ 3) * P y ^ 2) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧ =
    ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧

Tactic:
smul_eq _ <| Ne.isUnit hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧ =
    ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
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
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![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.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)),
        1]⟧

Tactic:
rw [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hx]

Goal state after: