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

Goal state before:
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.397} 𝒰.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.397} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := ⋯
s : Cocone D
a : J
𝒲 : (a : J) → (D.obj a).left.OpenCover := ⋯
⊢ (d.gluedCocone.ι.app a ≫
        {
          toCommaMorphism :=
            𝒱.glueMorphismsOverOfLocallyDirected
              (fun i ↦
                ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                  pullback.fst s.pt.hom (𝒰.f i))
              ⋯ ⋯,
          prop_hom_left := trivial, prop_hom_right := trivial }).left =
    (s.ι.app a).left

Tactic:
refine (𝒲 a).hom_ext _ _ fun i ↦ ?_

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.411} 𝒰.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.411} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
a : J
𝒲 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
i : (𝒲 a).I₀
⊢ (𝒲 a).f i ≫
      (d.gluedCocone.ι.app a ≫
          {
            toCommaMorphism :=
              𝒱.glueMorphismsOverOfLocallyDirected
                (fun i ↦
                  ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                    pullback.fst s.pt.hom (𝒰.f i))
                ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial }).left =
    (𝒲 a).f i ≫ (s.ι.app a).left
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶ ↑↑(↑i).2 := IsOpenImmersion.lift (Opens.ι ↑(↑i).2) (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ fst π π
h2 :
  snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ snd π π
⊢ ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u

Tactic:
obtain ⟨u, hu⟩ := of_isAffine_target (pullback.snd π (𝒰.f i)) f' <| by
    simp only [← cancel_mono (Scheme.Opens.ι i.1.2.1),
      Category.assoc, IsOpenImmersion.lift_fac, f', reassoc_of% h1, reassoc_of% h2, hf]

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶ ↑↑(↑i).2 := IsOpenImmersion.lift (Opens.ι ↑(↑i).2) (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ fst π π
h2 :
  snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ snd π π
u : 𝒰.X i ⟶ ↑↑(↑i).2
hu : snd π (𝒰.f i) ≫ u = f'
⊢ ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f))) s = 0

Tactic:
obtain ⟨t, ht⟩ := CompactSpace.elim_nhds_subcover (U ·) (fun x ↦ (U x).2.mem_nhds (hxU x))

Goal state after:
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f))) s = 0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ ∃ j fjx fjy,
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯

Tactic:
obtain ⟨k, fkj, hk⟩ := exists_app_map_eq_zero_of_isLimit D c hc
      (((hU x).preimage (D.map fjx)).isCompact.inter_of_isOpen
        ((hU y).preimage (D.map fjy)).isCompact ((U x).2.preimage (D.map fjx).continuous)
        ((U y).2.preimage (D.map fjy).continuous))
      ((D.map fjx).app (U x) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y) -
        (D.map fjy).app (U y) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) (by
      dsimp +instances [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]
      simp only [map_sub, sub_eq_zero, ← ConcreteCategory.comp_apply,
        Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map, Scheme.Hom.appLE_comp_appLE,
        Cone.w]
      simp_rw [Scheme.Hom.appLE, ConcreteCategory.comp_apply, ht, TopCat.Presheaf.restrictOpen,
        TopCat.Presheaf.restrict, ← ConcreteCategory.comp_apply, ← Functor.map_comp]
      rfl)

Goal state after:
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
k : I
fkj : k ⟶ j
hk :
  (ConcreteCategory.hom (Scheme.Hom.app (D.map fkj) (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
      (((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ -
        ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))
          ⋯) =
    0
⊢ ∃ j fjx fjy,
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ (Y - C y).natDegree < 2

Tactic:
natDegree_X_sub_C

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ 1 < 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W')
          (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) +
            C (X - C (W'.addX x₁ x₂ ℓ)) * C (C (W'.a₁ + ℓ)))} =
    span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))), (mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)}

Tactic:
congr 4

Goal state after:
case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) +
      C (X - C (W'.addX x₁ x₂ ℓ)) * C (C (W'.a₁ + ℓ)) =
    C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ span {(mk W') (C (X - C x)), (mk W') (Y - C (C y) + C (X - C x) * C (C (-ℓ)))} =
    span {(mk W') (C (X - C x)), (mk W') (Y - C (C ℓ * (X - C x) + C y))}

Tactic:
congr 4

Goal state after:
case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ Y - C (C y) + C (X - C x) * C (C (-ℓ)) = Y - C (C ℓ * (X - C x) + C y)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ span
      {(mk W) (C (X - C x₂)),
        (mk W)
          (Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))) +
            C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)))} =
    span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))}

Tactic:
congr 4

Goal state after:
case e_a.e_6
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)) =
    Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: 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₂
⊢ f y₁ = (W.map f).negY (f x₂) (f y₂)

Tactic:
hy,

Goal state after:
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₂
⊢ f (W.negY x₂ y₂) = (W.map f).negY (f x₂) (f y₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * b₄ W)) *
                (X - C x₁)) +
          C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0

Tactic:
b₄,

Goal state after:
case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
show 2 * (m + 1) + 1 = 2 * m + 3 by rfl,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ complEDS' b c d k (2 * m + 3) =
    complEDS' b c d k (m + 1) ^ 2 * normEDS b c d ((↑m + 2) * k + 1) * normEDS b c d ((↑m + 2) * k - 1) -
      complEDS' b c d k (m + 2) ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro.refine_2
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k✝ : I
fkj : k✝ ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
k : J
⊢ U k = c.π.app k✝ ⁻¹ᵁ (fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x) k

Tactic:
← hVU,

Goal state after:
case intro.refine_2
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k✝ : I
fkj : k✝ ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
k : J
⊢ c.π.app (j k) ⁻¹ᵁ V k = c.π.app k✝ ⁻¹ᵁ (fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x) k
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) =
    W.toAffine.polynomialY ^ 2 - 4 * W.toAffine.polynomial

Tactic:
b₄,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C W.b₆) =
    W.toAffine.polynomialY ^ 2 - 4 * W.toAffine.polynomial
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    (Functor.const I).map (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
g : S ⟶ D.leftOp.obj i
hg : φ ≫ g = t.app i
hg' : ψ = g ≫ c'.ι.app i
⊢ (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app (Opposite.unop i) ≫ Spec.map g = Spec.map ψ

Tactic:
simpa using! congr(Spec.map $hg').symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₄ = 2 * W.a₄

Tactic:
b₄,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = 2 * W.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✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₄ = E'.a₄

pp: case h.a₆
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₆ = E'.a₆

Tactic:
· simp_rw [variableChange_a₄, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF,
      a₄_of_isCharTwoJNeZeroNF]
    ring1

Goal state after:
case h.a₆
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₆ = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₄ = 0

Tactic:
b₄,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₄ = 2 * W.a₄

Tactic:
b₄,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = 2 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ ?m.102 * ↑n ≠ 0

Tactic:
rwa [← Nat.cast_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).coeff (W.preΨ n).natDegree = ↑(if Even n then n / 2 else n)

Tactic:
W.natDegree_preΨ h,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (_ ^ 2 : ℤ)) two_pos, mul_add,
      expDegree_cast (n + 2).succ_ne_zero, expDegree_cast n.succ_ne_zero, Nat.even_add_one, ite_not]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
⊢ 2 * (↑n + 1 + 1) ^ 2 =
    ((↑n + 2 + 1) ^ 2 - if Even n then 1 else 4) + ((↑n + 1) ^ 2 - if Even n then 1 else 4) +
      2 * if Even n then 0 else 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : 0 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case pos
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
⊢ P ≈ Q

Tactic:
exact equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz

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
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ P y - W.negY P ≠ 0) ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
hy,

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
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ W.negY P - W.negY P ≠ 0) ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0