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 :
  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)))
⊢ False
have obtain : ∀ (c₀ : ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
  (hc₃ :
    Membership.mem (γ := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
      (closedPoints ↥(tensorObj (𝒞 := instCategoryOver) G G).left) c₀)
  (hc₁ :
    Membership.mem (γ := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
      (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left (fst G G)))
        (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left)))
      c₀)
  (hc₂ :
    c₀ ∉
      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))),
  False
Tactic: 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
-- 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 :
  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))
⊢ Set.Finite (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.image (α := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) (⇑(Over.Hom.left γ))
      (Set.preimage (β := ↥G.left) (⇑(Over.Hom.left γ ≫ Over.Hom.left (fst G G)))
        (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left))))
have dsimp : Set.Finite (α := ↥(pullback G.hom G.hom))
  (Set.image (α := ↥(pullback G.hom G.hom))
    (⇑(pullback.lift (pullback.fst G.hom G.hom) (Over.Hom.left (GrpObj.commutator G)) sorry))
    (Set.preimage (β := ↥G.left)
      (⇑(CategoryStruct.comp (Y := pullback G.hom G.hom)
          (pullback.lift (pullback.fst G.hom G.hom) (Over.Hom.left (GrpObj.commutator G)) sorry)
          (pullback.fst G.hom G.hom)))
      (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left))))
Tactic: dsimp [-Scheme.Hom.comp_base, γ]
-- 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 :
  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))
⊢ Set.Finite (α := ↥(pullback G.hom G.hom))
    (Set.image (α := ↥(pullback G.hom G.hom))
      (⇑(pullback.lift (pullback.fst G.hom G.hom) (Over.Hom.left (GrpObj.commutator G)) ⋯))
      (Set.preimage (β := ↥G.left)
        (⇑(CategoryStruct.comp (Y := pullback G.hom G.hom)
            (pullback.lift (pullback.fst G.hom G.hom) (Over.Hom.left (GrpObj.commutator G)) ⋯)
            (pullback.fst G.hom G.hom)))
        (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left))))
have simp : Set.Finite (α := ↥(pullback G.hom G.hom))
  (Set.image (α := ↥(pullback G.hom G.hom))
    (⇑(pullback.lift (pullback.fst G.hom G.hom) (Over.Hom.left (GrpObj.commutator G)) sorry))
    (Set.preimage (β := ↥G.left) (⇑(pullback.fst G.hom G.hom))
      (singleton (α := ↥G.left) ((Over.Hom.left η) point : ↥G.left))))
Tactic: simp only [pullback.lift_fst]
-- 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 :
  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))
⊢ Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
have h : ∀ (U : G.left.Opens) (hηU : Membership.mem (α := ↥G.left) U ((Over.Hom.left η) point : ↥G.left))
  (H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)),
  Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
Tactic: obtain ⟨U, hηU, H⟩ := exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage
    γ.left (fst G G).left (η[G].left point) (by
      dsimp [-Scheme.Hom.comp_base, γ]
      simp only [pullback.lift_fst]
      exact (Set.finite_singleton _).subset H)
-- 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 : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
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 γ))
have refine : Subset (α := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
  (Set.preimage (β := ↥G.left) ⇑(pullback.fst G.hom G.hom) {(↑x : ↥G.left)} ∩
    Set.range («ι» := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) ⇑(Over.Hom.left γ))
  (Set.image (α := ↥(↑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U) : Scheme))
    (⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫ Scheme.Hom.imageι (Over.Hom.left γ)))
    (Set.preimage (β := ↥(↑U : Scheme)) ⇑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U) {x}))
Tactic: refine ((((γ.left.imageι ≫ (fst G G).left) ∣_ U).finite_preimage_singleton x).image
      (Scheme.Opens.ι _ ≫ γ.left.imageι)).subset ?_
-- 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 : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
⊢ Eq (α := Set ↥(↑U : Scheme)) (Set.preimage (β := ↥G.left) ⇑U.ι {(↑x : ↥G.left)}) {x}
have h : ∀ (x_1 : ↥(↑U : Scheme)),
  Membership.mem (γ := Set ↥(↑U : Scheme)) (Set.preimage (β := ↥G.left) ⇑U.ι {(↑x : ↥G.left)}) x_1 ↔
    Membership.mem (γ := Set ↥(↑U : Scheme)) {x} x_1
Tactic: ext
-- 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 : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
⊢ Subset (α := Set ↥(tensorObj (𝒞 := instCategoryOver) G G).left)
    (Set.preimage (β := ↥G.left) ⇑(pullback.fst G.hom G.hom) {(↑x : ↥G.left)} ∩
      Set.range («ι» := ↥(tensorObj (𝒞 := instCategoryOver) G G).left) ⇑(Over.Hom.left γ))
    (Set.image (α := ↥(↑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U) : Scheme))
      (⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)))
      (Set.preimage (β := ↥(↑U : Scheme)) ⇑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U) {x}))
have this₁ : Eq (α := Set ↥(↑U : Scheme)) (Set.preimage (β := ↥G.left) ⇑U.ι {(↑x : ↥G.left)}) {x}
Tactic: have : U.ι ⁻¹' {x.1} = {x} := by ext; simp
-- 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 γ))
⊢ Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (tensorObj (𝒞 := instCategoryOver) G G) ≫ η)
have h : (↑(Over.Hom.left (fst G G) ⁻¹ᵁ U) : Set ↥(G ⊗ G).left).Nonempty
Tactic: refine ext_of_apply_eq G.hom _
    ((fst G G).left ⁻¹ᵁ U).isOpen.isLocallyClosed
    (((fst G G).left ⁻¹ᵁ U).isOpen.dense ?_) ?_ ?_