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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective 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 ≠ Q x * P z
⊢ W.add P Q =
    W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
R : Presieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hf : Presieve.IsSeparated J F
⊢ Presieve.IsSeparatedFor F E.presieve₀

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hf : Presieve.IsSheaf J F
⊢ Presieve.IsSheafFor F E.presieve₀

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
S : Sieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
R : Presieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 2 = Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
b : E.toPreOneHypercover.I₁'
⊢ E.f b.fst.1 ≫ 𝟙 S = c.inj b.fst.1 ≫ (E.sigmaOfIsColimit hc).f PUnit.unit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
b : E.toPreOneHypercover.I₁'
⊢ E.f b.fst.2 ≫ 𝟙 S = c.inj b.fst.2 ≫ (E.sigmaOfIsColimit hc).f PUnit.unit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ ∀ (i : E.I₀), c.inj i ≫ (E.sigmaOfIsColimit hc).f PUnit.unit = E.f i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ ∀ (i j : E.I₀),
    (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).inj (i, j) ≫
        (Iso.refl (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).pt).hom ≫
          pullback.fst ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit) =
      pullback.fst (E.f (equiv.symm (i, j)).fst.1) (E.f (equiv.symm (i, j)).fst.2) ≫ c.inj i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ ∀ (i j : E.I₀),
    (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).inj (i, j) ≫
        (Iso.refl (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).pt).hom ≫
          pullback.snd ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit) =
      pullback.snd (E.f (equiv.symm (i, j)).fst.1) (E.f (equiv.symm (i, j)).fst.2) ≫ c.inj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ IsColimit c'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
⊢ ∀ (i : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X i)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').f
          ((Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) i) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.f i

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ W'.polynomialZ =
    Y ^ 2 + C W'.a₁ * X * Y + C (2 * W'.a₃) * Y * Z - (C W'.a₂ * X ^ 2 + C (2 * W'.a₄) * X * Z + C (3 * W'.a₆) * Z ^ 2)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialZ =
    P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k✝ : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
k a : E.toPreOneHypercover.I₁'
⊢ c'.inj a ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k✝)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k✝) =
    c'.inj a ≫
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k✝ ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 * (eval P) W'.polynomial =
    P x * (eval P) W'.polynomialX + P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
          P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠
            0)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
a : E.toPreOneHypercover.I₁'
⊢ c'.inj a ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₂
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k) =
    c'.inj a ≫
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₂ k ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
i j : (E.sigmaOfIsColimit hc).I₀
⊢ HasPullback ((E.sigmaOfIsColimit hc).f i) ((E.sigmaOfIsColimit hc).f j)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective 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₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W'.a₂ * (u * P x) * (u * P z) + W'.a₄ * (u * P z) ^ 2) = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : (E.sigmaOfIsColimit hc).HasPullbacks
i : E.I₀
⊢ HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this✝ : (E.sigmaOfIsColimit hc).HasPullbacks
this : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
⊢ PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective 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₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ 2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * (u * P z) ^ 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this✝¹ : (E.sigmaOfIsColimit hc).HasPullbacks
this✝ : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
this : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
⊢ PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective 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₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ (u * P y) ^ 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
      (W'.a₂ * (u * P x) ^ 2 + 2 * W'.a₄ * (u * P x) * (u * P z) + 3 * W'.a₆ * (u * P z) ^ 2) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
⊢ FamilyOfElements F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)

Tactic:
by

Goal state after: