awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
this :
  (glueData F).ι i ≫ eqToHom ⋯ =
    CategoryStruct.comp (Y := (glueData F).U ((equivShrink J : (a : J) → Shrink.{u, w} J) (↓i : J))) (eqToHom ⋯)
      ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) (↓i : J)))
⊢ CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F ↓i)
      (Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) =
    (glueData F).ι i

Tactic:
simp [cocone, Functor.const_obj_obj, eqToHom_map, ← this]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.cocone, CategoryTheory.eqToHom_map, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F_1 : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F_1.map f)
inst_2 : (F_1 ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
F : CategoryTheory.Functor.{w, u, w, u + 1} (WidePushoutShape J) Scheme
inst_5 : ∀ {i j : WidePushoutShape J} (f : i ⟶ j), IsOpenImmersion (F.map f)
⊢ (F ⋙ forget).IsLocallyDirected

Tactic:
have (i : _) : Mono ((F ⋙ forget).map (.init i)) :=
    (mono_iff_injective _).mpr (F.map _).isOpenEmbedding.injective
  inferInstance

Premises used: Iff.mpr, Topology.IsOpenEmbedding.toIsEmbedding, CategoryTheory.mono_iff_injective, AlgebraicGeometry.Scheme.forget, CategoryTheory.Limits.WidePushoutShape.Hom.init, CategoryTheory.Functor.comp, inferInstance, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Functor.map, Topology.IsEmbedding.injective
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
x : PUnit.{u + 1}
⊢ D.f i₁ i₂ ≫ D.ι i₁ = (D.t i₁ i₂ ≫ D.f i₂ i₁) ≫ D.ι i₂

Tactic:
simp only [Category.assoc, Scheme.GlueData.glue_condition]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.GlueData.glue_condition
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
⊢ Membership.mem (γ := Set (Sieve D.glued)) ((zariskiTopology : (a : Scheme) → Set (Sieve a)) D.glued)
    { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.sieve₀

Tactic:
zariskiTopology.superset_covering ?_ D.openCover.mem_grothendieckTopology

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, AlgebraicGeometry.Scheme.zariskiTopology, AlgebraicGeometry.Scheme.GlueData.openCover, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
refine : Sieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀
⊢ Membership.mem (γ := Set (Sieve D.glued)) ((zariskiTopology : (a : Scheme) → Set (Sieve a)) D.glued)
    { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.sieve₀

Tactic:
refine zariskiTopology.superset_covering ?_ D.openCover.mem_grothendieckTopology

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, AlgebraicGeometry.Scheme.zariskiTopology, AlgebraicGeometry.Scheme.GlueData.openCover, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
rw : Presieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀.arrows
⊢ Sieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀

Tactic:
rw [Sieve.generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
Y : Scheme
i : D.openCover.I₀
simp : D.ι i = D.openCover.f i
⊢ 𝟙 (D.openCover.X i) ≫ { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i = D.openCover.f i

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
Y : Scheme
i : D.openCover.I₀
⊢ D.ι i = D.openCover.f i

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

Tactic:
exact ⟨_, 𝟙 _, _, ⟨i⟩, by simp; rfl⟩
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
⊢ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
          Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
          p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
          p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
          PreOneHypercover D.glued }.sieve₁
      p₁ p₂ ∈
    (zariskiTopology : (a : Scheme) → Set (Sieve a)) W

Tactic:
zariskiTopology.superset_covering (fun T g _ ↦ ?_) (zariskiTopology.top_mem _)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, AlgebraicGeometry.Scheme.zariskiTopology, CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
refine :
  ∀ (T : Scheme.{u}) (g : T ⟶ W),
    Sieve.arrows ⊤ g →
      ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
                Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
                p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
                p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
                PreOneHypercover D.glued }.sieve₁
            p₁ p₂).arrows
        g
⊢ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
          Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
          p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
          p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
          PreOneHypercover D.glued }.sieve₁
      p₁ p₂ ∈
    (zariskiTopology : (a : Scheme) → Set (Sieve a)) W

Tactic:
refine zariskiTopology.superset_covering (fun T g _ ↦ ?_) (zariskiTopology.top_mem _)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, AlgebraicGeometry.Scheme.zariskiTopology, CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
h : Sieve.arrows ⊤ g
⊢ (g ≫ p₁) ≫ D.ι i₁ = (g ≫ p₂) ≫ D.ι i₂

Tactic:
simpa using g ≫= fac
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
h : Sieve.arrows ⊤ g
have :
  ∀ (φ : T ⟶ (D.vPullbackCone i₁ i₂).pt) (h₁ : φ ≫ (D.vPullbackCone i₁ i₂).fst = g ≫ p₁)
    (h₂ : φ ≫ (D.vPullbackCone i₁ i₂).snd = g ≫ p₂),
    ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
              Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
              p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
              p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
              PreOneHypercover D.glued }.sieve₁
          p₁ p₂).arrows
      g
⊢ ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
            Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
            p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
            p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
            PreOneHypercover D.glued }.sieve₁
        p₁ p₂).arrows
    g

Tactic:
have ⟨φ, h₁, h₂⟩ := PullbackCone.IsLimit.lift' (D.vPullbackConeIsLimit i₁ i₂)
      (g ≫ p₁) (g ≫ p₂) (by simpa using g ≫= fac)
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
h : Sieve.arrows ⊤ g
φ : T ⟶ (D.vPullbackCone i₁ i₂).pt
h₁ : φ ≫ (D.vPullbackCone i₁ i₂).fst = g ≫ p₁
h₂ : φ ≫ (D.vPullbackCone i₁ i₂).snd = g ≫ p₂
⊢ ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
            Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
            p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
            p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
            PreOneHypercover D.glued }.sieve₁
        p₁ p₂).arrows
    g

Tactic:
⟨⟨⟩, φ, h₁.symm, h₂.symm⟩

Premises used: And.intro, Exists.intro, PUnit.unit, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
h : Sieve.arrows ⊤ g
φ : T ⟶ (D.vPullbackCone i₁ i₂).pt
h₁ : φ ≫ (D.vPullbackCone i₁ i₂).fst = g ≫ p₁
h₂ : φ ≫ (D.vPullbackCone i₁ i₂).snd = g ≫ p₂
⊢ ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
            Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
            p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
            p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
            PreOneHypercover D.glued }.sieve₁
        p₁ p₂).arrows
    g

Tactic:
exact ⟨⟨⟩, φ, h₁.symm, h₂.symm⟩
-- Module: Mathlib.AlgebraicGeometry.GluingOneHypercover
Goal:
D : GlueData
F : Sheaf zariskiTopology (Type v)
s : (j : D.J) → F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (D.U j))
h :
  ∀ (i j : D.J),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (D.V (i, j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (D.f i j).op) :
            (a : (fun (X : Type v) ↦ X) (F.obj.obj (op (D.U i)))) →
              (fun (X : Type v) ↦ X) (F.obj.obj (op (D.V (i, j)))))
          (s i) :
        (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (D.V (i, j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.obj (P := Presheaf.IsSheaf zariskiTopology).map ((D.f j i).op ≫ (D.t i j).op)) :
            (a : (fun (X : Type v) ↦ X) (F.obj.obj (op (D.U j)))) →
              (fun (X : Type v) ↦ X) (F.obj.obj (op (D.V (i, j)))))
          (s j) :
        (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (D.V (i, j)))))
j : D.J
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (D.ι j).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj.obj (op D.glued))) → (fun (X : Type v) ↦ X) (F.obj.obj (op (D.U j))))
      (D.sheafValGluedMk s h) =
    s j

Tactic:
Multifork.IsLimit.sectionsEquiv_apply_val (D.oneHypercover.isLimitMultifork F) _ _

Premises used: CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val, CategoryTheory.GlueData.ι, CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork, AlgebraicGeometry.Scheme.GlueData.oneHypercover, AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
X : Scheme
G : Over (Spec (CommRingCat.of K))
inst_1 : GrpObj G
⊢ Over.Hom.left η ≫ G.hom = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
⊢ IsClosed (X := ↥S) {point}

Tactic:
have hpoint : IsClosed {point} := isClosed_discrete _
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
⊢ Nonempty.{u + 1} ↥G.left

Tactic:
have : Nonempty G.left := ⟨η[G].left point⟩
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this : Nonempty.{u + 1} ↥G.left
dsimp : IsProper (X := pullback G.hom G.hom) (pullback.fst G.hom G.hom ≫ G.hom)
⊢ IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this : Nonempty.{u + 1} ↥G.left
⊢ IsProper (X := pullback G.hom G.hom) (pullback.fst G.hom G.hom ≫ G.hom)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this : Nonempty.{u + 1} ↥G.left
⊢ IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom

Tactic:
have : IsProper (G ⊗ G).hom := by dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
⊢ JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left

Tactic:
have : JacobsonSpace (G ⊗ G).left := LocallyOfFiniteType.jacobsonSpace (Y := Spec _) (G ⊗ G).hom
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
⊢ Surjective G.hom

Tactic:
have : Surjective G.hom := ⟨Function.surjective_to_subsingleton (α := G.left) (β := Spec _) _⟩
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this : Surjective G.hom
⊢ IsProper (X := pullback G.hom G.hom) (pullback.fst G.hom G.hom)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this : Surjective G.hom
⊢ IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))

Tactic:
have : IsProper (fst G G).left := by dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
⊢ Surjective (X := pullback G.hom G.hom) (pullback.fst G.hom G.hom)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
⊢ Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))

Tactic:
have : Surjective (fst G G).left := by dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this_5 : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this : Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
rw : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
⊢ IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)

Tactic:
rw [Over.w]

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this_5 : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this : Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
⊢ IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this_5 : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this : Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
⊢ IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)

Tactic:
have : IsProper ((GrpObj.commutator G).left ≫ G.hom) := by rw [Over.w]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this_5 : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this_6 : Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
⊢ IsClosedImmersion (X :=
    Over.left (X := Spec (CommRingCat.of K)) ((𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver)))
    (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))

Tactic:
simpa using inferInstanceAs (IsClosedImmersion η[G].left)
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this_5 : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this_6 : Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
this : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
⊢ IsClosedImmersion (X :=
    Over.left (X := Spec (CommRingCat.of K)) ((𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver)))
    (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))

Tactic:
have : IsClosedImmersion ((lift η[G] η[G]).left ≫ (fst G G).left) := by
    simpa using inferInstanceAs (IsClosedImmersion η[G].left)