mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors 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
hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3
⊢ P y ≠ W'.negY P

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ P ≈ Q

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ (fun a ↦ a * Q z ^ 3) (P y) = (fun a ↦ a * Q z ^ 3) (W'.negY P)

Tactic:
by

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

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

Tactic:
by

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)
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
by

Goal state after:
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
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q

Tactic:
by

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
⊢ W'.dblU P = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomial = (MvPolynomial.map f) W'.polynomial

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (W'.map f).Equation (⇑f ∘ P)

Tactic:
by

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
hPz : P z = 0
⊢ W'.dblU P = -3 * P x ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (W'.map f).Equation (⇑f ∘ P) ↔ W'.Equation P

Tactic:
by

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✝
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 ⋙ Over.forget S).obj i)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialX = (MvPolynomial.map f) W'.polynomialX

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialY = (MvPolynomial.map f) W'.polynomialY

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialZ = (MvPolynomial.map f) W'.polynomialZ

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (W'.map f).Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

Tactic:
by

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

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomial = (MvPolynomial.map ↑f) (W'⁄A).polynomial

Tactic:
by

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
hPz : P z = 0
⊢ W'.dblZ P = 0

Tactic:
by

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✝
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 ⋙ Over.forget S).obj i)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ (W'⁄B).Equation (⇑f ∘ P)

Tactic:
by

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✝
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 ((D ⋙ Over.forget S).map f)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblZ P = 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Equation (⇑f ∘ P) ↔ (W'⁄A).Equation P

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialX = (MvPolynomial.map ↑f) (W'⁄A).polynomialX

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialY = (MvPolynomial.map ↑f) (W'⁄A).polynomialY

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialZ = (MvPolynomial.map ↑f) (W'⁄A).polynomialZ

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
by

Goal state after:
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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * 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) = -W.dblU P / W.dblZ P

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.neg P ≈ W'.neg Q

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.neg P = ![P x, -P y, 0]

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ Odd 3

Tactic:
by

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'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]

Tactic:
by

Goal state after:
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
⊢ W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ W.Nonsingular (W.neg P)

Tactic:
by

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
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P = (P x ^ 2) ^ 2

Tactic:
by

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✝
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
⊢ ((Over.forget S).mapCone c.unop).π ≫ { app := fun x ↦ (D.obj x).hom, naturality := ⋯ } =
    (Functor.const I).map (Over.Hom.left g ≫ X.hom)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblX P = W'.dblU P ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1

Tactic:
by

Goal state after:
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'.addX P (W'.neg P) = W'.dblZ P ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.Φ n).natDegree ≤ n.natAbs ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.Φ n).coeff (n.natAbs ^ 2) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : n ≠ 0
⊢ 0 < (W.Φ n).natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
⊢ (W.Φ n).leadingCoeff = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
⊢ W.Φ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
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)
⊢ Function.Surjective
    ((D.op ⋙ yoneda.obj X).descColimitType ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)))

Tactic:
intro g
      obtain ⟨k, u, h, h'⟩ := Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation
        (D ⋙ Over.forget _) (.mk (fun _ ↦ (D.obj _).hom)) X.hom _ (isLimitOfPreserves _ hc.unop)
        g.left (by ext; simp)
      use Functor.ιColimitType _ (.op k) (Over.homMk u)
      cat_disch

Goal state after:
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
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
⊢ (if hx : 1 = 0 then 0 else e ^ toAdd (unzero hx)) = 1

Tactic:
by

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✝
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
⊢ Nonempty (IsColimit ((yoneda.obj X).mapCocone c))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
⊢ (if hx : x * y = 0 then 0 else e ^ toAdd (unzero hx)) =
    (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) * if hx : y = 0 then 0 else e ^ toAdd (unzero hx)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
x : WithZero (Multiplicative ℤ)
hx : x = 0
⊢ (toNNReal he) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
⊢ (toNNReal he) x = e ^ toAdd (unzero hx)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : e ≠ 0
hm : m ≠ 0
⊢ (toNNReal he) m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : e ≠ 0
hm : m ≠ 0
⊢ (toNNReal he) m ≠ 0

Tactic:
by
  simp only [ne_eq, map_eq_zero, hm, not_false_eq_true]

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

Goal state before:
pp: 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)
⊢ (↑(f.lift h)).toFun 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : 1 < e
⊢ StrictMono ⇑(toNNReal ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
⊢ (toNNReal ⋯) m < 1 ↔ m < 1

Tactic:
by

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

Goal state before:
pp: 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)
x y : B
⊢ ∃ a b s, f.mk' a s = x ∧ f.mk' b s = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
⊢ (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1

Tactic:
by

Goal state after:
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.dblX P / W.dblZ P ^ 2 =
    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))

Tactic:
by

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'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P

Tactic:
by

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
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negDblY P = -(P x ^ 2) ^ 3

Tactic:
by

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

Goal state before:
pp: 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)
x y : B
⊢ (↑(f.lift h)).toFun (x + y) ≤ max ((↑(f.lift h)).toFun x) ((↑(f.lift h)).toFun y)

Tactic:
by

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

Goal state before:
pp: 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
x : A
y : ↥S
⊢ ↑v.toMonoidWithZeroHom x * ↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom).domRestrict S) ⋯) y)⁻¹ = v x * (v ↑y)⁻¹

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.negDblY P = (-W'.dblU P) ^ 3

Tactic:
by

Goal state after: