awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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))
⊢ 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 η η))

Tactic:
have : IsClosedImmersion (lift η[G] η[G]).left := .of_comp _ (g := (fst G 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_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 :
  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)
⊢ IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))

Tactic:
simpa [γ]
-- 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 :
  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)
⊢ IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))

Tactic:
have : IsProper (γ.left ≫ (fst G G).left) := by simpa [γ]
-- 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 : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
⊢ IsProper (Over.Hom.left γ)

Tactic:
have : IsProper γ.left := .of_comp _ (fst G 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_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 γ)
rw : GrpObj.commutator G = toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η
⊢ IsCommMonObj G

Tactic:
rw [isCommMonObj_iff_commutator_eq_toUnit_η]

Premises used: CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η
-- 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 : Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
⊢ GrpObj.commutator G = toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η

Tactic:
ext1
-- 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 γ)
rw :
  ¬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)))
⊢ 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:
rw [Set.image_subset_iff, ← Set.diff_eq_empty, ← Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty, Set.image_subset_iff, Set.diff_eq_empty
-- 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 :
  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)))
rw :
  IsLocallyClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    ((Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
          (Set.image (α := ↥S) ⇑(Over.Hom.left (lift η η)) {point}))ᶜ ∩
      Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G))) (Set.image (α := ↥S) ⇑(Over.Hom.left η) {point}))
⊢ IsLocallyClosed (X := ↥(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)))

Tactic:
rw [Set.diff_eq_compl_inter, ← Set.image_singleton, ← Set.image_singleton]

Premises used: Set.image_singleton, Set.diff_eq_compl_inter
-- 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 :
  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)))
⊢ IsLocallyClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    ((Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
          (Set.image (α := ↥S) ⇑(Over.Hom.left (lift η η)) {point}))ᶜ ∩
      Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G))) (Set.image (α := ↥S) ⇑(Over.Hom.left η) {point}))

Tactic:
(IsOpen.isLocallyClosed ?_).inter (IsClosed.isLocallyClosed ?_)

Premises used: IsLocallyClosed.inter, IsOpen.isLocallyClosed, IsClosed.isLocallyClosed
-- 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 :
  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)))
refine_1 :
  IsOpen (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
        (Set.image (α := ↥S) ⇑(Over.Hom.left (lift η η)) {point}))ᶜ
refine_2 :
  IsClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G))) (Set.image (α := ↥S) ⇑(Over.Hom.left η) {point}))
⊢ IsLocallyClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    ((Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
          (Set.image (α := ↥S) ⇑(Over.Hom.left (lift η η)) {point}))ᶜ ∩
      Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G))) (Set.image (α := ↥S) ⇑(Over.Hom.left η) {point}))

Tactic:
refine (IsOpen.isLocallyClosed ?_).inter (IsClosed.isLocallyClosed ?_)

Premises used: IsLocallyClosed.inter, IsOpen.isLocallyClosed, IsClosed.isLocallyClosed
-- 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 :
  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)))
⊢ IsOpen (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
        (Set.image (α := ↥S) ⇑(Over.Hom.left (lift η η)) {point}))ᶜ

Tactic:
(((lift η[G] η[G]).left.isClosedMap _ hpoint).preimage γ.left.continuous).isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf