-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
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 γ)
⊢ Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
have H : 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))
Tactic: have H : γ.left '' ((fst G G).left ⁻¹' {η[G].left point}) ⊆ {(lift η[G] η[G]).left point} := by
    rw [Set.image_subset_iff, ← Set.diff_eq_empty, ← Set.not_nonempty_iff_eq_empty]
    intro H
    obtain ⟨c₀, ⟨hc₁, hc₂⟩, hc₃⟩ := nonempty_inter_closedPoints H <| by
      rw [Set.diff_eq_compl_inter, ← Set.image_singleton, ← Set.image_singleton];
      refine (IsOpen.isLocallyClosed ?_).inter (IsClosed.isLocallyClosed ?_)
      · exact (((lift η[G] η[G]).left.isClosedMap _ hpoint).preimage γ.left.continuous).isOpen_compl
      · exact (η[G].left.isClosedMap _ hpoint).preimage (fst G G).left.continuous
    obtain ⟨⟨c, hc⟩, e⟩ := (pointEquivClosedPoint (G ⊗ G).hom).surjective ⟨c₀, hc₃⟩
    obtain rfl : c point = c₀ := congr(($e).1)
    let fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 _) (Over.homMk c hc ≫ snd G G)
    have : c ≫ pullback.fst G.hom G.hom = η[G].left :=
      ext_of_apply_closedPoint_eq G.hom (by simpa) (by simp) (by simpa)
    have H₁ : c = fc.left ≫ (η[G] ▷ G).left := by dsimp; ext <;> simp [fc, S, this]
    have H₂ : fc ≫ η ▷ G ≫ γ = lift η η := by ext1 <;> simp [fc, γ, S]
    exact hc₂ <| by simp [H₁, H₂, ← Scheme.Hom.comp_apply, Category.assoc, ← Over.comp_left]