awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
G : Over (Spec (CommRingCat.of K))
inst_1 : IsProper G.hom
inst_2 : GeometricallyIntegral G.hom
inst_3 : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this_1 : IsProper G'.hom
this_2 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
this_3 : GrpObj G' := Functor.grpObjObj
this : IsCommMonObj G'
rw :
  ∀ (this : GrpObj.commutator G' = toUnit (tensorObj (𝒞 := instCategoryOver) G' G') ≫ η),
    GrpObj.commutator G = toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η
⊢ IsCommMonObj G

Tactic:
rw [isCommMonObj_iff_commutator_eq_toUnit_η] at this ⊢

Premises used: CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
G : Over (Spec (CommRingCat.of K))
inst_1 : IsProper G.hom
inst_2 : GeometricallyIntegral G.hom
inst_3 : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this_1 : IsProper G'.hom
this_2 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
this_3 : GrpObj G' := Functor.grpObjObj
this : GrpObj.commutator G' = toUnit (tensorObj (𝒞 := instCategoryOver) G' G') ≫ η
a :
  (Over.pullback f).map (GrpObj.commutator G) =
    (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
⊢ GrpObj.commutator G = toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η

Tactic:
apply (Over.pullback f).map_injective

Premises used: CategoryTheory.Over.pullback, CategoryTheory.Functor.map_injective
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
G : Over (Spec (CommRingCat.of K))
inst_1 : IsProper G.hom
inst_2 : GeometricallyIntegral G.hom
inst_3 : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this_1 : IsProper G'.hom
this_2 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
this_3 : GrpObj G' := Functor.grpObjObj
this : GrpObj.commutator G' = toUnit (tensorObj (𝒞 := instCategoryOver) G' G') ≫ η
a :
  Iso.hom (Functor.Monoidal.μIso (Over.pullback f) G G) ≫ (Over.pullback f).map (GrpObj.commutator G) =
    Iso.hom (Functor.Monoidal.μIso (Over.pullback f) G G) ≫
      (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
⊢ (Over.pullback f).map (GrpObj.commutator G) =
    (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)

Tactic:
rw [← cancel_epi (Functor.Monoidal.μIso (Over.pullback f) G G).hom]

Premises used: CategoryTheory.Over.pullback, CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
G : Over (Spec (CommRingCat.of K))
inst_1 : IsProper G.hom
inst_2 : GeometricallyIntegral G.hom
inst_3 : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this_1 : IsProper G'.hom
this_2 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
this_3 : GrpObj G' := Functor.grpObjObj
this : GrpObj.commutator G' = toUnit (tensorObj (𝒞 := instCategoryOver) G' G') ≫ η
a :
  Functor.LaxMonoidal.μ (Over.pullback f) G G ≫ (Over.pullback f).map (fst G G * snd G G * (fst G G)⁻¹ * (snd G G)⁻¹) =
    Functor.LaxMonoidal.μ (Over.pullback f) G G ≫
      (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
⊢ Iso.hom (Functor.Monoidal.μIso (Over.pullback f) G G) ≫ (Over.pullback f).map (GrpObj.commutator G) =
    Iso.hom (Functor.Monoidal.μIso (Over.pullback f) G G) ≫
      (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)

Tactic:
dsimp [GrpObj.commutator] at this ⊢

Premises used: CategoryTheory.GrpObj.commutator
-- Module: Mathlib.AlgebraicGeometry.Group.Abelian
Goal:
K : Type u
inst : Field K
G : Over (Spec (CommRingCat.of K))
inst_1 : IsProper G.hom
inst_2 : GeometricallyIntegral G.hom
inst_3 : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this_1 : IsProper G'.hom
this_2 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
this_3 : GrpObj G' := Functor.grpObjObj
this :
  fst G' G' * snd G' G' * (fst G' G')⁻¹ * (snd G' G')⁻¹ =
    toUnit (tensorObj (𝒞 := instCategoryOver) G' G') ≫ Functor.LaxMonoidal.ε (Over.pullback f) ≫ (Over.pullback f).map η
⊢ Functor.LaxMonoidal.μ (Over.pullback f) G G ≫ (Over.pullback f).map (fst G G * snd G G * (fst G G)⁻¹ * (snd G G)⁻¹) =
    Functor.LaxMonoidal.μ (Over.pullback f) G G ≫
      (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)

Tactic:
simpa only [Functor.map_mul, one_eq_one, comp_one, Functor.map_one, Functor.map_inv',
    comp_mul, GrpObj.comp_inv, Functor.Monoidal.μ_fst, Functor.Monoidal.μ_snd]

Premises used: CategoryTheory.Functor.map_mul, CategoryTheory.Functor.map_inv', CategoryTheory.MonObj.comp_one, CategoryTheory.Functor.Monoidal.μ_fst, CategoryTheory.MonObj.comp_mul, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.GrpObj.comp_inv, CategoryTheory.MonObj.one_eq_one, CategoryTheory.Functor.map_one
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
⊢ JacobsonSpace.{u} ↥G

Tactic:
have := LocallyOfFiniteType.jacobsonSpace f
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this : JacobsonSpace.{u} ↥G
⊢ Nonempty.{u + 1} ↥G

Tactic:
have : Nonempty G := ⟨η[Over.mk f].1 (IsLocalRing.closedPoint _)⟩
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
rw : ¬(↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
⊢ Smooth f

Tactic:
rw [← Scheme.Hom.smoothLocus_eq_top_iff, ← TopologicalSpace.Opens.coe_eq_univ,
    ← not_ne_iff, ← Set.nonempty_compl]

Premises used: AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, not_ne_iff, Set.nonempty_compl, TopologicalSpace.Opens.coe_eq_univ
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
obtain :
  ∀ (x : ↥G) (hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ)
    (hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x), False
⊢ False

Tactic:
obtain ⟨x, hx, hxc⟩ :=
    nonempty_inter_closedPoints H f.smoothLocus.2.isClosed_compl.isLocallyClosed

Premises used: nonempty_inter_closedPoints, AlgebraicGeometry.Scheme.Hom.smoothLocus, IsOpen.isClosed_compl, IsClosed.isLocallyClosed, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
obtain : ∀ (y : ↥G) (hy : y ∈ Scheme.Hom.smoothLocus f) (hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y), False
⊢ False

Tactic:
obtain ⟨y, hy : y ∈ f.smoothLocus, hyc⟩ := nonempty_inter_closedPoints
    f.dense_smoothLocus_of_perfectField.nonempty f.smoothLocus.2.isLocallyClosed

Premises used: nonempty_inter_closedPoints, AlgebraicGeometry.Scheme.Hom.smoothLocus, Dense.nonempty, IsOpen.isLocallyClosed, AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
dsimp : x' ≫ (GrpObj.mulRight x').inv ≫ (GrpObj.mulRight y').hom = y'
⊢ x' ≫ α.hom = y'

Tactic:
dsimp only [Iso.trans_hom, Iso.symm_hom, α]

Premises used: CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.trans_hom
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
rw : x' ≫ (GrpObj.mulRight x').inv = y' ≫ (GrpObj.mulRight y').inv
⊢ x' ≫ (GrpObj.mulRight x').inv ≫ (GrpObj.mulRight y').hom = y'

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
⊢ x' ≫ (GrpObj.mulRight x').inv = y' ≫ (GrpObj.mulRight y').inv

Tactic:
simp [comp_lift_assoc]

Premises used: CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
⊢ x' ≫ α.hom = y'

Tactic:
have hα : x' ≫ α.hom = y' := by
    dsimp only [Iso.trans_hom, Iso.symm_hom, α]
    rw [← Category.assoc, ← Iso.eq_comp_inv]
    simp [comp_lift_assoc]
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
⊢ (Over.Hom.left α.hom) x = y

Tactic:
simpa [x', y', pointEquivClosedPoint] using congr(($hα).left (IsLocalRing.closedPoint K))

Premises used: AlgebraicGeometry.pointEquivClosedPoint
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
⊢ (Over.Hom.left α.hom) x = y

Tactic:
have hα' : α.hom.left x = y := by
    simpa [x', y', pointEquivClosedPoint] using congr(($hα).left (IsLocalRing.closedPoint K))
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
⊢ x' ≫ α.hom = y'

Tactic:
rw! [← hα', ← α.hom.left.mem_preimage, Scheme.Hom.preimage_smoothLocus_eq,
    show α.hom.left ≫ f = f from α.hom.w] at hy

Premises used: CategoryTheory.Over.Hom.left, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, CategoryTheory.Over.Hom.w, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
hα₁ : x' ≫ α.hom = y'
⊢ (Over.Hom.left α.hom) x = y

Tactic:
rw! [← hα', ← α.hom.left.mem_preimage, Scheme.Hom.preimage_smoothLocus_eq,
    show α.hom.left ≫ f = f from α.hom.w] at hy

Premises used: CategoryTheory.Over.Hom.left, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, CategoryTheory.Over.Hom.w, CategoryTheory.Iso.hom