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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2) / P z ^ 2 +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (2 * (P y / P z) + W.toAffine.a₁ * (P x / P z) + W.toAffine.a₃ +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) + W.a₃ * (P z ^ 2 / P z ^ 2))) =
    0

Tactic:
;

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2) / P z ^ 2 +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (2 * (P y / P z) + W.toAffine.a₁ * (P x / P z) + W.toAffine.a₃ +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) + W.a₃ * (P z ^ 2 / P z ^ 2))) =
    0
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₁'
⊢ pullback.fst (E.f a.fst.1) (E.f a.fst.2) ≫ c.inj a.fst.1 =
    c'.inj a ≫ pullback.fst ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
;

Goal state after:
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₁'
⊢ pullback.fst (E.f a.fst.1) (E.f a.fst.2) ≫ c.inj a.fst.1 =
    c'.inj a ≫ pullback.fst ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)
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₁'
⊢ pullback.snd (E.f a.fst.1) (E.f a.fst.2) ≫ c.inj a.fst.2 =
    c'.inj a ≫ pullback.snd ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
;

Goal state after:
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₁'
⊢ pullback.snd (E.f a.fst.1) (E.f a.fst.2) ≫ c.inj a.fst.2 =
    c'.inj a ≫ pullback.snd ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)
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
  let c' : Cofan E.toPreOneHypercover.Y' :=
    Cofan.mk
      ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := ⟨⟩) (i₂ := ⟨⟩) ⟨⟩)
      fun b ↦ pullback.map _ _ _ _ (c.inj _) (c.inj _) (𝟙 _) (by simp) (by simp)
  let equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ :=
    Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
  have hc' : IsColimit c' := by
    refine (c'.isColimitEquivOfEquiv equiv.symm).symm (Nonempty.some ?_)
    exact IsUniversalColimit.nonempty_isColimit_prod_of_isPullback
      huniv huniv E.f E.f ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
      (fun i j ↦ .of_hasPullback _ _) (.of_hasPullback _ _) (.refl _) (by simp) (by simp)
      (by simp [c', equiv, Equiv.sigmaPUnit]) (by simp [c', equiv, Equiv.sigmaPUnit])
  refine .trans ?_ (E.toPreOneHypercover.isLimitSigmaOfIsColimitEquiv hc hc' F)
  apply PreOneHypercover.isLimitEquivOfIso
  refine PreOneHypercover.isoMk (.refl _) (fun _ ↦ .refl _) (fun _ _ ↦ .refl _)
      (fun _ _ _ ↦ Iso.refl _) (by cat_disch) ?_ ?_
  · intro ⟨⟩ ⟨⟩ k
    refine Cofan.IsColimit.hom_ext hc' _ _ fun k ↦ ?_
    congr 1
    exact Cofan.IsColimit.hom_ext hc' _ _ fun a ↦ by simp; simp [c']
  · intro ⟨⟩ ⟨⟩ k
    exact Cofan.IsColimit.hom_ext hc' _ _ fun a ↦ by simp; simp [c']

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 (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)

Tactic:
;

Goal state after:
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 (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)
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) (Cofan.IsColimit.desc hc E.f)

Tactic:
;

Goal state after:
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) (Cofan.IsColimit.desc hc E.f)
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 (X i)) F

Tactic:
;

Goal state after:
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 (X i)) F
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
t : F.obj (op I)
h :
  (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : F.obj (op I)), (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj (op I)
x✝ : Y
⊢ (ConcreteCategory.hom a).toFun x✝ = (ConcreteCategory.hom default).toFun x✝

Tactic:
;

Goal state after:
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
t : F.obj (op I)
h :
  (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : F.obj (op I)), (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj (op I)
x✝ : Y
⊢ (ConcreteCategory.hom a).toFun x✝ = (ConcreteCategory.hom default).toFun x✝
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
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (↑hu.unit⁻¹ • u • P)

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

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

Goal state before:
pp: case mk
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)

Tactic:
;

Goal state after:
case mk
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: case neg
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)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
⊢ (ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a) =
    (ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)

Tactic:
have := preservesTerminal_of_isSheaf_for_empty F hF hI

Goal state after:
case neg
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)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
⊢ (ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a) =
    (ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

Tactic:
;

Goal state after:
case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x * Q z) = f (Q x * P z)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

Tactic:
;

Goal state after:
case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y * Q z) = f (Q y * P z)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ forgetToTop.IsContinuous (precoverage IsOpenImmersion).toGrothendieck TopCat.grothendieckTopology

Tactic:
apply Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy

Goal state after:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ precoverage IsOpenImmersion ≤ Precoverage.comap forgetToTop TopCat.precoverage
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
⊢ Presieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀.arrows

Tactic:
rintro W _ ⟨i⟩

Goal state after:
D : GlueData
Y : Scheme
i : D.openCover.I₀
⊢ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀.arrows (D.openCover.f i)
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
Y : Scheme
i : D.openCover.I₀
⊢ 𝟙 (D.openCover.X i) ≫ D.ι i = D.openCover.f i

Tactic:
;

Goal state after:
D : GlueData
Y : Scheme
i : D.openCover.I₀
⊢ 𝟙 (D.openCover.X i) ≫ D.ι i = D.openCover.f i
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: ⊢ uliftFunctor.IsContinuous grothendieckTopology grothendieckTopology

Tactic:
apply Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy

Goal state after:
⊢ precoverage ≤ Precoverage.comap uliftFunctor precoverage
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
hg : g.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.FormallyUnramified R S
algebraizeInst✝ : Algebra.FormallyUnramified S T
⊢ (g.comp f).FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.comp R S T

Goal state after:
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
    fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this : IsScalarTower R Rₓ Sₓ
⊢ Algebra.IsUnramifiedAt R x.asIdeal
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (smoothLocus R Af)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
rw [← smoothLocus_comap_of_isLocalization f] at this

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (comap (algebraMap A Af) ⁻¹' smoothLocus R A)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case g
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ A i →ₐ[R] ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2

Tactic:
apply AlgHom.ofLinearMap
      ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))

Goal state after:
case g.map_one
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

case g.map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ∀ (x y : A i),
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
        (x * y) =
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          x *
        ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          y