mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.95} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.95} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ D.obj a ⟶ ((Functor.const J).obj d.glued).obj a

pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.95} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.95} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
⊢ D.map f ≫ ?refine_1 = ?refine_1 ≫ ((Functor.const J).obj d.glued).map f

Tactic:
· refine ⟨(𝒱 a).glueMorphismsOverOfLocallyDirected ?_ ?_ ?_, trivial, trivial⟩
    · intro i
      exact ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
    · intro i j hij
      conv_rhs => rw [← colimit.w d.relativeGluingData.functor hij]
      simp only [← Category.assoc]
      congr 1
      exact congr($(d.cocone_ι_transitionMap hij a).left).symm
    · intro
      simp [𝒱, pullback.condition, glued]

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
⊢ D.map f ≫
      {
        toCommaMorphism :=
          (𝒱 b).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    {
        toCommaMorphism :=
          (𝒱 a).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } ≫
      ((Functor.const J).obj d.glued).map f
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
⊢ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i = pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j

Tactic:
have : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) :=
      Flat.epi_of_flat_of_surjective _

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i = pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.twoTorsionPolynomial = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Tactic:
by
  rw [twoTorsionPolynomial]
  ext <;> dsimp
  · linear_combination 2 * CharP.cast_eq_zero R 2
  · linear_combination W.b₄ * CharP.cast_eq_zero R 2

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

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (3 * f x₁ ^ 2 + 2 * (W.map f).a₂ * f x₁ + (W.map f).a₄ - (W.map f).a₁ * f y₁) / (f y₁ - f (W.negY x₁ y₁)) =
    f (W.slope x₁ x₂ y₁ y₂)

Tactic:
slope_of_Y_ne hx hy

Goal state after:
case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (3 * f x₁ ^ 2 + 2 * (W.map f).a₂ * f x₁ + (W.map f).a₄ - (W.map f).a₁ * f y₁) / (f y₁ - f (W.negY x₁ y₁)) =
    f ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * (↑n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑n✝ + 1 + 1 + 2) * preNormEDS b c d (↑n✝ + 1 + 1) ^ 3 * if ¬¬Even ↑n✝ then b else 1) -
      preNormEDS b c d (↑n✝ + 1) * preNormEDS b c d (↑n✝ + 1 + 1 + 1) ^ 3 * if ¬¬Even ↑n✝ then 1 else b

Tactic:
not_not,

Goal state after:
case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * (↑n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑n✝ + 1 + 1 + 2) * preNormEDS b c d (↑n✝ + 1 + 1) ^ 3 * if Even ↑n✝ then b else 1) -
      preNormEDS b c d (↑n✝ + 1) * preNormEDS b c d (↑n✝ + 1 + 1 + 1) ^ 3 * if Even ↑n✝ then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d m * (complEDS₂ b c d m * b) =
    normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2

Tactic:
complEDS₂_mul_b

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d m *
      (normEDS b c d (m - 1) ^ 2 * normEDS b c d (m + 2) - normEDS b c d (m - 2) * normEDS b c d (m + 1) ^ 2) =
    normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
⊢ (q ^ 2).degree + (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆).degree = 2 • q.degree + 3

Tactic:
degree_pow,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
⊢ 2 • q.degree + (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆).degree = 2 • q.degree + 3
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS' b c d k 0 = 0

Tactic:
rw [complEDS']

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS' b c d k 1 = 1

Tactic:
rw [complEDS']

Goal state after:
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
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ 0 =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' ⋯) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)

Tactic:
exact (CoordinateRing.mk_XYIdeal'_neg_mul h₂).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
this :
  ∀ {X : Scheme} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ S, X = Spec S) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ S, X = Spec S
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
obtain ⟨i, f, hf⟩ := this (a ≫ X.isoSpec.hom) (X.isoSpec.inv ≫ f)
      (by simp [ha, -Functor.map_comp]) ⟨_, rfl⟩

Goal state after:
case inr
I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f✝ : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f✝
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f✝)
this :
  ∀ {X : Scheme} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ S, X = Spec S) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ S, X = Spec S
i : I
f : D.obj i ⟶ Spec Γ(X, ⊤)
hf : c.π.app i ≫ f = a ≫ X.isoSpec.hom ∧ f ≫ X.isoSpec.inv ≫ f✝ = t.app i
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f✝ = t.app i
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
by
  have h := W.Δ'.ne_zero
  rw [coe_Δ', Δ_of_isShortNF] at h
  rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isShortNF, Δ_of_isShortNF, div_eq_div_iff h (right_ne_zero_of_mul h)]
  ring1

Goal state after:
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 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'

Tactic:
have ha₃ := E.Δ'.ne_zero

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : ↑E.Δ' ≠ 0
⊢ ∃ C, C • E = E'
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
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
this : ∀ (j : ↥s), IsAffine ↑(↑(↑↑j).2).1
j : ↥s
⊢ (opensCone D c i' (𝒱' j)).π ≫ t𝒱 j =
    (Functor.const (Over i')).map
      (Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯ ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯)

Tactic:
ext k

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
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
this : ∀ (j : ↥s), IsAffine ↑(↑(↑↑j).2).1
j : ↥s
k : Over i'
⊢ ((opensCone D c i' (𝒱' j)).π ≫ t𝒱 j).app k =
    ((Functor.const (Over i')).map
          (Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯ ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯)).app
      k
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✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) ≠
      0 ∨
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 ≠ 0 ∨
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 -
          (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) ≠
        0
⊢ W'.Nonsingular P

Tactic:
refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) ≠
      0 ∨
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 ≠ 0 ∨
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 -
          (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) ≠
        0
⊢ W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
          (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠
        0
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:
rw [dblX, Y_eq_negY_of_Y_eq hQz hx hy hy']
  ring1

Goal state after:
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
⊢ W'.addX P (W'.neg P) + -2 * P z ^ 2 * 0 -
      (W'.dblZ P ^ 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:
(rw [addX, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1)

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦Q⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]
    exact Setoid.symm <| equiv_zero_of_Z_eq_zero hQ hQz

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
n : ℕ
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.mk x y ^ (n + 1) = ValueGroupWithZero.mk x y ^ n * ValueGroupWithZero.mk x y

Tactic:
simp_rw [HPow.hPow, Pow.pow]; simp [pow_succ]

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ ∀ x ∈ {a | a.2 < a.1}, {a | a.2 < a.1} ∈ 𝓝 x

Tactic:
rintro ⟨a, b⟩ (hab : b < a)

Goal state after:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.2 < a.1} ∈ 𝓝 (a, b)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔ F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (F.NeBot ∧ ∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a + b + c) = ↑(a + (b + c))

Tactic:
add_assoc

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a + (b + c)) = ↑(a + (b + c))
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 Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ DiscreteTopology R

Tactic:
simp only [discreteTopology_iff_isOpen_singleton_zero, isOpen_iff_mem_nhds, mem_singleton_iff,
    forall_eq, v.mem_nhds_zero_iff, subset_singleton_iff, mem_ofPred_eq]

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ ∃ γ, ∀ (y : R), v.restrict y < ↑γ → y = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hb
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

pp: case hd
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0

Tactic:
all_goals simp [ValueGroup₀.restrict₀]

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
⊢ ⋯.extend (⇑f) 0 = 0

Tactic:
convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0 <;>
    simp only [map_zero]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3

Tactic:
by
  rw [Affine.negAddY, toAffine_addX_of_ne hPz hQz hd]
  simp [field]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] = (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
addY_smul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, addZ (u • P) (v • Q)] =
    (u * v) ^ 2 • W'.addXYZ P Q
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
s : Set (WithVal v)
x : WithVal v
⊢ s ∈ nhds x ↔ ∃ γ, (fun x_1 ↦ x + x_1) '' {z | (ValuativeRel.valuation (WithVal v)) z < ↑γ} ⊆ s

Tactic:
simp only [Set.image_add_left, Set.preimage_ofPred_eq, Valued.mem_nhds]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
s : Set (WithVal v)
x : WithVal v
⊢ (∃ γ, {y | Valued.v.restrict (y - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (ValuativeRel.valuation (WithVal v)) (-x + a) < ↑γ} ⊆ s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
simp only [dblXYZ, map_dblX, map_dblY, map_dblZ, comp_fin3]

Goal state after: