awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α β : X ⟶ Y
h : α = β
x : (↑(↑X : TopCat) : Type v)
rw :
  Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x)
    (Hom.stalkMap α x) (Hom.stalkMap α x ≫ eqToHom ⋯)
rw₁ : Hom.stalkMap α x = Hom.stalkMap α x ≫ 𝟙 (X.presheaf.stalk x)
rw₂ rw₃ :
  Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x)
    (Hom.stalkMap α x) (Hom.stalkMap α x)
⊢ Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x)
    (Hom.stalkMap α x) (eqToHom ⋯ ≫ Hom.stalkMap β x)

Tactic:
rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.congr, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, rfl
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
x x' : (↑(↑X : TopCat) : Type v)
h : x = x'
rw rw₁ : X.presheaf.stalk x' = X.presheaf.stalk x'
⊢ X.presheaf.stalk x = X.presheaf.stalk x'

Tactic:
rw [h]
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
x x' : (↑(↑X : TopCat) : Type v)
h : x = x'
rw rw₁ :
  Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x') =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x')
⊢ Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x) =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x')

Tactic:
rw [h]
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
x x' : (↑(↑X : TopCat) : Type v)
h : x = x'
rw rw₁ :
  Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x')
    (eqToHom ⋯ ≫ Hom.stalkMap α x') (eqToHom ⋯ ≫ Hom.stalkMap α x')
⊢ Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x')
    (Hom.stalkMap α x ≫ eqToHom ⋯) (eqToHom ⋯ ≫ Hom.stalkMap α x')

Tactic:
rw [stalkMap.congr α α rfl x x' h]

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.congr, rfl
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
rw :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Hom.base (𝟙 X)) :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
rw₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (𝟙 (↑X : TopCat)) :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
rw₂ rw₃ : x = x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x

Tactic:
rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]

Premises used: TopCat.id_app, AlgebraicGeometry.PresheafedSpace.id_base, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x

Tactic:
have h_eq : (α ≫ β).base x = x := by rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
h_eq :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
rw rw₁ : X.presheaf.stalk x = X.presheaf.stalk x
⊢ X.presheaf.stalk x =
    X.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (α ≫ β).base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
        x)

Tactic:
rw [h_eq]
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
h_eq :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
refine_1 :
  Hom.stalkMap α x ≫
      eqToHom ⋯ ≫
        Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x) =
    𝟙
      (Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
refine_2 :
  (eqToHom ⋯ ≫
        Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x)) ≫
      Hom.stalkMap α x =
    𝟙 (X.presheaf.stalk x)
⊢ ∃ (inv :
    X.presheaf.stalk x ⟶
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)),
    Hom.stalkMap α x ≫ inv =
        𝟙
          (Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) α.base :
                (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
              x)) ∧
      inv ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
refine
      ⟨eqToHom (show X.presheaf.stalk x = X.presheaf.stalk ((α ≫ β).base x) by rw [h_eq]) ≫
          (β.stalkMap (α.base x) :),
        ?_, ?_⟩
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
h_eq :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
refine_1 :
  eqToHom ⋯ ≫
      Hom.stalkMap α
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (α ≫ β).base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
            x) ≫
        Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x) =
    𝟙
      (Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
⊢ Hom.stalkMap α x ≫
      eqToHom ⋯ ≫
        Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x) =
    𝟙
      (Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))

Tactic:
rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, Eq.symm, DFunLike.coe, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
h_eq :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
refine_1 :
  eqToHom ⋯ ≫
      Hom.stalkMap (β ≫ α)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) =
    𝟙
      (Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
⊢ eqToHom ⋯ ≫
      Hom.stalkMap α
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (α ≫ β).base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
            x) ≫
        Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x) =
    𝟙
      (Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))

Tactic:
erw [← stalkMap.comp β α (α.base x)]

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
inst_2 : IsIso α
x : (↑(↑X : TopCat) : Type v)
β : Y ⟶ X := CategoryTheory.inv α
h_eq :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (α ≫ β).base :
        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
      x =
    x
refine_2 :
  eqToHom ⋯ ≫
      Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x) ≫
        Hom.stalkMap α x =
    𝟙 (X.presheaf.stalk x)
refine_2₁ : eqToHom ⋯ ≫ Hom.stalkMap (α ≫ β) x = 𝟙 (X.presheaf.stalk x)
refine_2₂ :
  CategoryStruct.comp (Y :=
      X.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (α ≫ β).base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
          x))
      (eqToHom ⋯) (eqToHom ⋯ ≫ Hom.stalkMap (𝟙 X) x) =
    𝟙 (X.presheaf.stalk x)
refine_2₃ :
  Eq.{v + 1} (α := X.presheaf.stalk x ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
      X.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (α ≫ β).base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
          x))
      (eqToHom ⋯) (eqToHom ⋯ ≫ 𝟙 (X.presheaf.stalk x)))
    (𝟙 (X.presheaf.stalk x))
refine_2₄ :
  Eq.{v + 1} (α := X.presheaf.stalk x ⟶ X.presheaf.stalk x) (eqToHom ⋯ ≫ 𝟙 (X.presheaf.stalk x))
    (𝟙 (X.presheaf.stalk x))
refine_2₅ :
  Eq.{v + 1} (α := X.presheaf.stalk x ⟶ X.presheaf.stalk x) (𝟙 (X.presheaf.stalk x) ≫ 𝟙 (X.presheaf.stalk x))
    (𝟙 (X.presheaf.stalk x))
refine_2₆ refine_2₇ :
  Eq.{v + 1} (α := X.presheaf.stalk x ⟶ X.presheaf.stalk x) (𝟙 (X.presheaf.stalk x)) (𝟙 (X.presheaf.stalk x))
⊢ (eqToHom ⋯ ≫
        Hom.stalkMap β
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x)) ≫
      Hom.stalkMap α x =
    𝟙 (X.presheaf.stalk x)

Tactic:
rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id,
        eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_refl, AlgebraicGeometry.PresheafedSpace.stalkMap.id, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
f : X ⟶ Y
x y : (↑(↑X : TopCat) : Type v)
h : x ⤳ y
j :
  OpenNhds (X := (↑Y : TopCat))
    ((TopCat.Hom.hom f.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) y)
⊢ Eq (α :=
    Y.presheaf.obj
        (op
          (obj
            (OpenNhds.inclusion
              ((TopCat.Hom.hom f.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) y))
            j)) ⟶
      X.presheaf.stalk x)
    (f.c.app
        (obj (C :=
          (OpenNhds (X := (↑Y : TopCat))
              ((TopCat.Hom.hom f.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x))ᵒᵖ)
          (Functor.op
            (OpenNhds.inclusion
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                x)))
          (op
            (Subtype.mk (p := fun (U : Opens (↑(↑Y : TopCat) : Type v)) ↦
              Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
                ((TopCat.Hom.hom f.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
                  (↑(↑Y : TopCat) : Type v)))
              (↑j : Opens (↑(↑Y : TopCat) : Type v)) ⋯))) ≫
      X.presheaf.map
          (𝟙
            ((OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op.obj
              (op
                (Subtype.mk (p := fun (U : Opens (↑(↑Y : TopCat) : Type v)) ↦
                  Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
                    ((TopCat.Hom.hom f.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
                      (↑(↑Y : TopCat) : Type v)))
                  (↑j : Opens (↑(↑Y : TopCat) : Type v)) ⋯)))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
          ((OpenNhds.map f.base x).op.obj
            (op
              (Subtype.mk (p := fun (U : Opens (↑(↑Y : TopCat) : Type v)) ↦
                Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
                  ((TopCat.Hom.hom f.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
                    (↑(↑Y : TopCat) : Type v)))
                (↑j : Opens (↑(↑Y : TopCat) : Type v)) ⋯))))
    (f.c.app
        (obj
          (Functor.op
            (OpenNhds.inclusion
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                y)))
          (op j)) ≫
      X.presheaf.map (𝟙 ((OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op.obj (op j))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
          (op
            (Subtype.mk (p := fun (U : Opens (↑(↑X : TopCat) : Type v)) ↦ x ∈ U)
              (↑(unop ((OpenNhds.map f.base y).op.obj (op j))) : Opens (↑(↑X : TopCat) : Type v)) ⋯)))

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
x y : Abelianization G
a b : G
⊢ ⁅b⁻¹, a⁻¹⁆ = HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) a b)⁻¹ ((fun (x1 x2 : G) ↦ x1 * x2) b a)

Tactic:
simp [commutatorElement_def, mul_assoc]

Premises used: commutatorElement_def, mul_assoc
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
a : G
⊢ Eq (α := Quot (α := G) (⇑(QuotientGroup.leftRel (commutator G)) : G → G → Prop))
    (Quot.mk (⇑(QuotientGroup.leftRel (commutator G)) : G → G → Prop) a) ((of : (a : G) → Abelianization G) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
⊢ Eq (α := Subgroup G) (MonoidHom.ker of) (commutator G)

Tactic:
QuotientGroup.ker_mk' (commutator G)

Premises used: MonoidHom.mk', commutator, Abelianization.of, QuotientGroup.mk', QuotientGroup.ker_mk', Abelianization
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : CommGroup A
f : G →* A
rw : commutatorSet G ⊆ (↑f.ker : Set G)
⊢ commutator G ≤ f.ker

Tactic:
rw [commutator_eq_closure, Subgroup.closure_le]

Premises used: commutator_eq_closure, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ (↑f.ker : Set G)

Tactic:
simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]

Premises used: commutatorElement_def, MonoidHom.mem_ker, mul_right_comm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : CommGroup A
f : G →* A
x : G
⊢ Eq.{v + 1} (α := A)
    ((((lift : (a : G →* A) → Abelianization G →* A) f : MonoidHom.{u, v} (Abelianization G) A) :
          (a : Abelianization G) → A)
        ((of : (a : G) → Abelianization G) x : Abelianization G) :
      A)
    ((f : (a : G) → A) x : A)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : CommGroup A
⊢ Eq (α := (a : MonoidHom.{u, v} (Abelianization G) A) → G →* A)
    (⇑(Equiv.symm lift) : (a : Abelianization G →* A) → G →* A) fun (x : MonoidHom.{u, v} (Abelianization G) A) ↦
    x.comp of

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : CommGroup A
f : MonoidHom.{u, v} (Abelianization G) A
⊢ (Equiv.symm lift : (a : Abelianization G →* A) → G →* A) f = f.comp of

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : CommGroup A
f : G →* A
φ : MonoidHom.{u, v} (Abelianization G) A
hφ :
  ∀ (x : G),
    Eq.{v + 1} (α := A) ((φ : (a : Abelianization G) → A) ((of : (a : G) → Abelianization G) x : Abelianization G) : A)
      ((f : (a : G) → A) x : A)
x : Abelianization G
⊢ Eq.{v + 1} (α := A) ((φ : (a : Abelianization G) → A) x : A)
    ((((lift : (a : G →* A) → Abelianization G →* A) f : MonoidHom.{u, v} (Abelianization G) A) :
          (a : Abelianization G) → A)
        x :
      A)

Tactic:
QuotientGroup.induction_on x hφ

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
⊢ Eq.{u + 1} (α := Abelianization G →* Abelianization G)
    ((lift : (a : G →* Abelianization G) → Abelianization G →* Abelianization G) of :
      Abelianization G →* Abelianization G)
    (MonoidHom.id (Abelianization G) : Abelianization G →* Abelianization G)

Tactic:
lift.apply_symm_apply <| MonoidHom.id _

Premises used: Equiv.apply_symm_apply, Abelianization.lift, Abelianization.of, MonoidHom.id
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
A : Type v
inst_1 : Monoid A
φ ψ : MonoidHom.{u, v} (Abelianization G) A
h : φ.comp of = ψ.comp of
⊢ φ = ψ

Tactic:
MonoidHom.ext fun x => QuotientGroup.induction_on x <| DFunLike.congr_fun h

Premises used: MonoidHom.ext, QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
f : G →* H
⊢ (lift : (a : G →* Abelianization H) → Abelianization G →* Abelianization H) (MonoidHom.comp of f) = map f

Tactic:
rfl

Premises used: Abelianization.map, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
f : G →* H
x : G
⊢ Eq (α := Abelianization H)
    ((map f : (a : Abelianization G) → Abelianization H) ((of : (a : G) → Abelianization G) x) : Abelianization H)
    ((of : (a : H) → Abelianization H) ((f : (a : G) → H) x) : Abelianization H)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
⊢ Eq (α := Abelianization G →* Abelianization G) (map (MonoidHom.id G)) (MonoidHom.id (Abelianization G))

Tactic:
hom_ext _ _ rfl

Premises used: Abelianization.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
f : G →* H
I : Type w
inst_2 : Group I
g : H →* I
⊢ (map g).comp (map f) = map (g.comp f)

Tactic:
hom_ext _ _ rfl

Premises used: Abelianization.hom_ext, rfl