-- 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_7 : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this_8 :
  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))
this_9 :
  IsClosedImmersion.{u} (X :=
    Over.left (X := Spec (CommRingCat.of K)) ((𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver))) (Y :=
    (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (lift η η))
γ : tensorObj (𝒞 := instCategoryOver) G G ⟶ tensorObj (𝒞 := instCategoryOver) G G :=
  lift (fst G G) (GrpObj.commutator G)
this_10 : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this_11 : IsProper (Over.Hom.left γ)
H :
  Set.Nonempty (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
        (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left)) \
      Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
        (singleton (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
          ((Over.Hom.left (lift η η)) point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)))
c : Spec (CommRingCat.of K) ⟶ (tensorObj (𝒞 := instCategoryOver) G G).left
hc : c ≫ (tensorObj (𝒞 := instCategoryOver) G G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ :
  Membership.mem (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (γ :=
    Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (closedPoints ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (c point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
hc₁ :
  Membership.mem (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (γ :=
    Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
      (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left)))
    (c point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
hc₂ :
  (c point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left) ∉
    Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
      (singleton (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
        ((Over.Hom.left (lift η η)) point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left))
e :
  Eq (α := (↑(closedPoints ↥(tensorObj (𝒞 := instCategoryOver) G G).left) : Type u))
    ((pointEquivClosedPoint (tensorObj (𝒞 := instCategoryOver) G G).hom :
          (a : { p : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left // p ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K)) }) →
            (↑(closedPoints ↥(G ⊗ G).left) : Type u))
        (Subtype.mk (p := fun (p : Spec (CommRingCat.of K) ⟶ (tensorObj (𝒞 := instCategoryOver) G G).left) ↦
          p ≫ (tensorObj (𝒞 := instCategoryOver) G G).hom = 𝟙 (Spec (CommRingCat.of K))) c hc) :
      (↑(closedPoints ↥(tensorObj (𝒞 := instCategoryOver) G G).left) : Type u))
    (Subtype.mk (p := fun (x : ↥(tensorObj (𝒞 := instCategoryOver) G G).left) ↦
        Membership.mem (γ := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
          (closedPoints ↥(tensorObj (𝒞 := instCategoryOver) G G).left) x)
        (c point) hc₃ :
      { x : ↥(tensorObj (𝒞 := instCategoryOver) G G).left //
        Membership.mem (γ := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
          (closedPoints ↥(tensorObj (𝒞 := instCategoryOver) G G).left) x })
fc : (𝟙_ (Over S)) (𝒞 := instCategoryOver) ⟶
  tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over S)) (𝒞 := instCategoryOver)) G :=
  lift (𝟙 ((𝟙_ (Over S)) (𝒞 := instCategoryOver)))
    (CategoryStruct.comp (Y := tensorObj (𝒞 := instCategoryOver) G G) (Over.homMk c hc) (snd G G))
this : c ≫ pullback.fst G.hom G.hom = Over.Hom.left η
H₁ : c = Over.Hom.left fc ≫ Over.Hom.left (η ▷ G)
H₂ : fc ≫ η ▷ G ≫ γ = lift η η
⊢ Membership.mem (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (γ :=
    Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
      (singleton (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
        ((Over.Hom.left (lift η η)) point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)))
    (c point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)

Tactic:
simp [H₁, H₂, ← Scheme.Hom.comp_apply, Category.assoc, ← Over.comp_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.comp_left, AlgebraicGeometry.Scheme.Hom.comp_apply