awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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 γ))
h : (↑(Over.Hom.left (fst G G) ⁻¹ᵁ U) : Set ↥(G ⊗ G).left).Nonempty
⊢ Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
have h₁ : ∀ x ∈ (↑(Over.Hom.left (fst G G) ⁻¹ᵁ U) : Set ↥(G ⊗ G).left),
  IsClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) {x} →
    Eq (α := ↥G.left) ((Over.Hom.left (GrpObj.commutator G)) x : ↥G.left)
      ((Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)) x : ↥G.left)
Tactic: refine ext_of_apply_eq G.hom _
    ((fst G G).left ⁻¹ᵁ U).isOpen.isLocallyClosed
    (((fst G G).left ⁻¹ᵁ U).isOpen.dense ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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 γ))
h : (↑(Over.Hom.left (fst G G) ⁻¹ᵁ U) : Set ↥(G ⊗ G).left).Nonempty
h₁ :
  ∀ x ∈ (↑(Over.Hom.left (fst G G) ⁻¹ᵁ U) : Set ↥(G ⊗ G).left),
    IsClosed (X := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) {x} →
      Eq (α := ↥G.left) ((Over.Hom.left (GrpObj.commutator G)) x : ↥G.left)
        ((Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)) x : ↥G.left)
⊢ Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
have h₂ : Over.Hom.left (GrpObj.commutator G) ≫ G.hom = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η) ≫ G.hom
Tactic: refine ext_of_apply_eq G.hom _
    ((fst G G).left ⁻¹ᵁ U).isOpen.isLocallyClosed
    (((fst G G).left ⁻¹ᵁ U).isOpen.dense ?_) ?_ ?_
-- 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 γ)
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}
⊢ Eq (α := ↥G.left) ((Over.Hom.left (GrpObj.commutator G)) y : ↥G.left)
    ((Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)) y : ↥G.left)
have hx : IsClosed (X := ↥G.left) (singleton (α := ↥G.left) ((Over.Hom.left (fst G G)) y : ↥G.left))
Tactic: have hx : IsClosed {(fst G G).left y} := by simpa using (fst G G).left.isClosedMap _ hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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
⊢ IsProper G'.hom
have dsimp : IsProper (X := pullback G.hom f) (pullback.snd G.hom f)
Tactic: dsimp [G']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
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
⊢ IsCommMonObj G
have this : IsProper G'.hom
Tactic: have : IsProper G'.hom := by dsimp [G']; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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 : IsProper G'.hom
⊢ IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
have dsimp : IsIntegral.{u} (pullback (X := pullback G.hom f) (Y := pullback G.hom f) (pullback.snd G.hom f) (pullback.snd G.hom f))
Tactic: dsimp [G']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
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 : IsProper G'.hom
⊢ IsCommMonObj G
have this₁ : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G' G').left
Tactic: have : IsIntegral (G' ⊗ G').left := by dsimp [G']; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
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 : GrpObj G' := Functor.grpObjObj
⊢ IsCommMonObj G
have this₁ : IsCommMonObj G'
Tactic: have := isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed G'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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'
⊢ IsCommMonObj G
have rw : ∀ (this : GrpObj.commutator G' = toUnit (tensorObj (𝒞 := instCategoryOver) G' G') ≫ η),
  GrpObj.commutator G = toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η
Tactic: rw [isCommMonObj_iff_commutator_eq_toUnit_η] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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') ≫ η
⊢ GrpObj.commutator G = toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η
have a : (Over.pullback f).map (GrpObj.commutator G) = (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
Tactic: apply (Over.pullback f).map_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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') ≫ η
⊢ (Over.pullback f).map (GrpObj.commutator G) =
    (Over.pullback f).map (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
have 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) ≫ η)
Tactic: rw [← cancel_epi (Functor.Monoidal.μIso (Over.pullback f) G G).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
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') ≫ η
⊢ 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) ≫ η)
have 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) ≫ η)
Tactic: dsimp [GrpObj.commutator] at this ⊢
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (hypothesis)
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
⊢ Smooth f
have this : JacobsonSpace.{u} ↥G
Tactic: have := LocallyOfFiniteType.jacobsonSpace f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (hypothesis)
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
⊢ Smooth f
have this₁ : Nonempty.{u + 1} ↥G
Tactic: have : Nonempty G := ⟨η[Over.mk f].1 (IsLocalRing.closedPoint _)⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
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
⊢ Smooth f
have rw : ¬(↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
Tactic: rw [← Scheme.Hom.smoothLocus_eq_top_iff, ← TopologicalSpace.Opens.coe_eq_univ,
    ← not_ne_iff, ← Set.nonempty_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
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
⊢ False
have obtain : ∀ (x : ↥G) (hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ) (hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x),
  False
Tactic: obtain ⟨x, hx, hxc⟩ :=
    nonempty_inter_closedPoints H f.smoothLocus.2.isClosed_compl.isLocallyClosed
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
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
⊢ False
have obtain : ∀ (y : ↥G) (hy : y ∈ Scheme.Hom.smoothLocus f) (hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y), False
Tactic: obtain ⟨y, hy : y ∈ f.smoothLocus, hyc⟩ := nonempty_inter_closedPoints
    f.dense_smoothLocus_of_perfectField.nonempty f.smoothLocus.2.isLocallyClosed
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
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'
have dsimp : x' ≫ (GrpObj.mulRight x').inv ≫ (GrpObj.mulRight y').hom = y'
Tactic: dsimp only [Iso.trans_hom, Iso.symm_hom, α]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
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 ≫ (GrpObj.mulRight y').hom = y'
have rw : x' ≫ (GrpObj.mulRight x').inv = y' ≫ (GrpObj.mulRight y').inv
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (hypothesis)
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'
⊢ False
have hα : 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]