-- 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 : IsProper (Over.Hom.left γ)
H_1 :
  Subset (α := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.image (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
      (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
        (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left))))
    (singleton (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
      ((Over.Hom.left (lift η η)) point : ↥(tensorObj (𝒞 := instCategoryOver) G G).left))
U : G.left.Opens
hηU : Membership.mem (α := ↥G.left) U ((Over.Hom.left η) point : ↥G.left)
H_2 : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H :
  ∀ (x : ↥U),
    Set.Finite (α := ↥(pullback G.hom G.hom))
      (Set.preimage (β := ↥G.left) ⇑(pullback.fst G.hom G.hom) {(↑x : ↥G.left)} ∩
        Set.range («ι» := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) ⇑(Over.Hom.left γ))
y : ↥(tensorObj (𝒞 := instCategoryOver) G G).left
hyU : y ∈ (↑(Over.Hom.left (fst G G) ⁻¹ᵁ U) : Set ↥(G ⊗ G).left)
hy : IsClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) {y}
hx : IsClosed (X := ↥G.left) (singleton (α := ↥G.left) ((Over.Hom.left (fst G G)) y : ↥G.left))
x : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ G :=
  Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(tensorObj (𝒞 := instCategoryOver) G G).left := (Over.Hom.left (fst G G ≫ Iso.inv (ρ_ G) ≫ G ◁ η)) y
refine_1 :
  IsPreirreducible (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
      (singleton (α := ↥G.left) ((Over.Hom.left (fst G G)) y : ↥G.left)))
refine_2 :
  Membership.mem (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (γ :=
    Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.image (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
      (closure
        (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
          (singleton (α := ↥G.left) ((Over.Hom.left (fst G G)) y : ↥G.left)))))
    ((Over.Hom.left γ) y : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
refine_3 :
  Membership.mem (γ := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.image (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
      (closure
        (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
          (singleton (α := ↥G.left) ((Over.Hom.left (fst G G)) y : ↥G.left)))))
    xe
⊢ (Over.Hom.left γ) y = xe

Tactic:
refine subsingleton_image_closure_of_finite_of_isPreirreducible
        (hx.preimage (fst G G).left.continuous).isLocallyClosed ?_ γ.left.continuous
        γ.left.isClosedMap ((H ⟨_, hyU⟩).subset (Set.image_subset_iff.mpr fun _ ↦ by
          simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base, γ])) ?_ ?_

Premises used: Iff.mpr, CategoryTheory.Over.Hom.left, AlgebraicGeometry.Scheme.Hom.isClosedMap, subsingleton_image_closure_of_finite_of_isPreirreducible, Set.Finite.subset, Subtype.mk, AlgebraicGeometry.Scheme.Hom.continuous, IsClosed.preimage, IsClosed.isLocallyClosed, Set.image_subset_iff, CategoryTheory.SemiCartesianMonoidalCategory.fst