awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this_2 :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
this :
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ S)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
preservesLimit_of_reflects_of_preserves _ (Under.forget _ ⊤ S)

Premises used: CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CategoryTheory.MorphismProperty.Under.forget, Top.top
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this_2 :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
this :
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ S)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
exact preservesLimit_of_reflects_of_preserves _ (Under.forget _ ⊤ S)

Premises used: CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CategoryTheory.MorphismProperty.Under.forget, Top.top
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
⊢ PreservesFiniteLimits (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
have := hPp.preservesFiniteProducts_pushout hPi f
  have := hPse.preservesEqualizers_pushout hPi hPe f
  have := CommRingCat.Under.hasFiniteLimits hPi hPp hPe
  preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts _

Premises used: CommRingCat.Under.hasFiniteLimits, RingHom.HasFiniteProducts.preservesFiniteProducts_pushout, RingHom.HasStableEqualizers.preservesEqualizers_pushout, CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts, CategoryTheory.MorphismProperty.Under.pushout, RingHom.toMorphismProperty, Top.top
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X : MagmaCat
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y Z : MagmaCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
            carrier) g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
            carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : MagmaCat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
              carrier) f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
              carrier) g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M : Type u
inst : Mul M
⊢ (↑(of M) : Type u) = M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M : MagmaCat
⊢ Hom.hom (𝟙 M) = MulHom.id (↑M : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M : MagmaCat
x : (↑M : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 M) :
        (a : (↑M : Type u_1)) → (↑M : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N T : MagmaCat
f : M ⟶ N
g : N ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N T : MagmaCat
f : M ⟶ N
g : N ⟶ T
x : (↑M : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑M : Type u_1)) → (↑T : Type u_1))
        x :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
            g :
          (a : (↑N : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
                carrier) f :
              (a : (↑M : Type u_1)) → (↑N : Type u_1))
            x :
          (↑N : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N : MagmaCat
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: MagmaCat.Hom.ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N : Type u
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N : MagmaCat
f : M ⟶ N
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M : Type u
inst : Mul M
⊢ ofHom (MulHom.id M) = 𝟙 (of M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N P : Type u
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
f : M →ₙ* N
g : N →ₙ* P
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Type u
inst : Mul X
inst_1 : Mul Y
f : X →ₙ* Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N : MagmaCat
e : M ≅ N
x : (↑M : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑N : Type u_1)) → (↑M : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
              carrier) e.hom :
            (a : (↑M : Type u_1)) → (↑N : Type u_1))
          x :
        (↑N : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
M N : MagmaCat
e : M ≅ N
s : (↑N : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑M : Type u_1)) → (↑N : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
              carrier) e.inv :
            (a : (↑N : Type u_1)) → (↑M : Type u_1))
          s :
        (↑M : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Type u_1
inst : Mul X
inst_1 : Mul Y
e : X ≃* Y
⊢ Hom.hom (ofHom (↑e : X →ₙ* Y)) = (↑e : (↑(of X) : Type u_1) →ₙ* (↑(of Y) : Type u_1))

Tactic:
rfl

Premises used: MulHomClass.toMulHom, rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X : Semigrp
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y Z : Semigrp
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
            carrier) g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
            carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Semigrp
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
              f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
              g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
R : Type u
inst : Semigroup R
⊢ (↑(of R) : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X : Semigrp
⊢ Hom.hom (𝟙 X) = MulHom.id (↑X : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X : Semigrp
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y T : Semigrp
f : X ⟶ Y
g : Y ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y T : Semigrp
f : X ⟶ Y
g : Y ⟶ T
x : (↑X : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑T : Type u_1))
        x :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
            g :
          (a : (↑Y : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC :=
                carrier) f :
              (a : (↑X : Type u_1)) → (↑Y : Type u_1))
            x :
          (↑Y : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Semigrp
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: Semigrp.Hom.ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Type u
inst : Semigroup X
inst_1 : Semigroup Y
f : X →ₙ* Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Semigrp
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X : Type u
inst : Semigroup X
⊢ ofHom (MulHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y Z : Type u
inst : Semigroup X
inst_1 : Semigroup Y
inst_2 : Semigroup Z
f : X →ₙ* Y
g : Y →ₙ* Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Type u
inst : Semigroup X
inst_1 : Semigroup Y
f : X →ₙ* Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Semigrp
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
              e.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Semigrp
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := carrier)
              e.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          s :
        (↑X : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Type u_1
inst : Semigroup X
inst_1 : Semigroup Y
e : X ≃* Y
⊢ Hom.hom (ofHom (↑e : X →ₙ* Y)) = (↑e : (↑(of X) : Type u_1) →ₙ* (↑(of Y) : Type u_1))

Tactic:
rfl

Premises used: MulHomClass.toMulHom, rfl
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
i : X ≅ Y
h :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑X : Type u_1))
      (((MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
        (↑X : Type u_1))
      ((MulHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ (MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) = MulHom.id (↑X : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    (((MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
      (↑X : Type u_1))
    ((MulHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
i : X ≅ Y
h :
  ∀ (x : (↑Y : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      (((MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
        (↑Y : Type u_1))
      ((MulHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
⊢ (MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) = MulHom.id (↑Y : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ Eq (α := (↑Y : Type u_1))
    (((MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
      (↑Y : Type u_1))
    ((MulHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
i : X ≅ Y
h :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑X : Type u_1))
      (((Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
        (↑X : Type u_1))
      ((MulHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ (Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) = MulHom.id (↑X : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    (((Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
      (↑X : Type u_1))
    ((MulHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
i : X ≅ Y
h :
  ∀ (x : (↑Y : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      (((Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
        (↑Y : Type u_1))
      ((MulHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
⊢ (Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) = MulHom.id (↑Y : Type u_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ Eq (α := (↑Y : Type u_1))
    (((Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
      (↑Y : Type u_1))
    ((MulHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    X ≅
  Functor.obj (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := __src.toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
e.toMagmaCatIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, MulEquiv.toMagmaCatIso
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    X ≅
  Functor.obj (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget MagmaCat (FC := fun (x1 x2 : MagmaCat.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := __src.toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toMagmaCatIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, MulEquiv.toMagmaCatIso
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    X ≅
  Functor.obj (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := __src.toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
e.toSemigrpIso.isIso_hom

Premises used: MulEquiv.toSemigrpIso, CategoryTheory.Iso.isIso_hom