mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ ∀ {X Y : Comma L R} (f : X ⟶ Y),
    (map α β ⋙ fst L' R').map f ≫ (Iso.refl ((map α β ⋙ fst L' R').obj Y)).hom =
      (Iso.refl ((map α β ⋙ fst L' R').obj X)).hom ≫ (fst L R ⋙ F₁).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
A' : Type u₄
inst✝³ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝² : Category.{v₅, u₅} B'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝ : Category.{v₄, u₄} C
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma (F ⋙ L) R
f : X✝ ⟶ Y✝
⊢ L.map (F.map f.left) ≫ { left := F.obj Y✝.left, right := Y✝.right, hom := Y✝.hom }.hom =
    { left := F.obj X✝.left, right := X✝.right, hom := X✝.hom }.hom ≫ R.map f.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
A' : Type u₄
inst✝³ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝² : Category.{v₅, u₅} B'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝ : Category.{v₄, u₄} C
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X : Comma (F ⋙ L) R
⊢ L.map (Iso.refl ((preLeft F L R).obj X).left).hom ≫
      ((map (F ⋙ L).rightUnitor.inv (R.rightUnitor.hom ≫ R.leftUnitor.inv)).obj X).hom =
    ((preLeft F L R).obj X).hom ≫ R.map (Iso.refl ((preLeft F L R).obj X).right).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
A' : Type u₄
inst✝³ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝² : Category.{v₅, u₅} B'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝ : Category.{v₄, u₄} C
L : A ⥤ T
R : B ⥤ T
F : T ⥤ C
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (L ⋙ F).map f.left ≫ { left := Y✝.left, right := Y✝.right, hom := F.map Y✝.hom }.hom =
    { left := X✝.left, right := X✝.right, hom := F.map X✝.hom }.hom ≫ (R ⋙ F).map f.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (R.op.map (op f.right) ≫ (unop (op { left := op X✝.right, right := op X✝.left, hom := op X✝.hom })).hom).unop =
    ((unop (op { left := op Y✝.right, right := op Y✝.left, hom := op Y✝.hom })).hom ≫ L.op.map (op f.left)).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma L.op R.op
f : X✝ ⟶ Y✝
⊢ (R.map f.right.unop ≫ (unop (op { left := unop X✝.right, right := unop X✝.left, hom := X✝.hom.unop })).hom).op =
    ((unop (op { left := unop Y✝.right, right := unop Y✝.left, hom := Y✝.hom.unop })).hom ≫ L.map f.left.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (α.homCongr γ) (f ≫ g) = (α.homCongr β) f ≫ (β.homCongr γ) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ((refl X).homCongr (refl Y)) f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ ((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ≅ X₂
g : Y₁ ≅ Y₂
⊢ Function.LeftInverse (fun h ↦ f ≪≫ h ≪≫ g.symm) fun h ↦ f.symm ≪≫ h ≪≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ≅ X₂
g : Y₁ ≅ Y₂
⊢ Function.RightInverse (fun h ↦ f ≪≫ h ≪≫ g.symm) fun h ↦ f.symm ≪≫ h ≪≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
⊢ (refl X).conj f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ α.symm.conj (α.conj f) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
⊢ α.conjAut f = α.symm ≪≫ f ≪≫ α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
Z : C
β : Y ≅ Z
f : Aut X
⊢ (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M : MonCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N T : MonCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : MonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : MonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X : MonCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X Y Z : MonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M : CommMonCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N T : CommMonCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : CommMonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : CommMonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X : CommMonCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : GrpCat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y T : GrpCat
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
⊢ Function.Injective fun f ↦ ofHom f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: R S : GrpCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ (ConcreteCategory.hom i) r = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : GrpCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : CommGrpCat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y T : CommGrpCat
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
⊢ Function.Injective fun f ↦ ofHom f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: R S : CommGrpCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ (ConcreteCategory.hom i) r = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : CommGrpCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y Z : CommGrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G : AddCommGrpCat
h k : ↑G
w : asHom h = asHom k
⊢ h = k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
⊢ (GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
⊢ (GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
⊢ (CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
⊢ (CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: α : Type u
⊢ Iso.toEquiv 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: α : Type u
⊢ ∀ (x y : Aut α), Iso.toEquiv (x * y) = Iso.toEquiv x * Iso.toEquiv y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: α : Type u
⊢ Equiv.toIso 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: α : Type u
⊢ ∀ (x y : Equiv.Perm α), Equiv.toIso (x * y) = Equiv.toIso x * Equiv.toIso y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
f : X ⟶ Y
x✝ : IsIso ((forget GrpCat).map f)
i : (forget GrpCat).obj X ≅ (forget GrpCat).obj Y := asIso ((forget GrpCat).map f)
⊢ ∀ (x y : ↑X), i.toEquiv.toFun (x * y) = i.toEquiv.toFun x * i.toEquiv.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
f : X ⟶ Y
x✝ : IsIso ((forget GrpCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGrpCat).map f)
i : (forget CommGrpCat).obj X ≅ (forget CommGrpCat).obj Y := asIso ((forget CommGrpCat).map f)
⊢ ∀ (x y : ↑X), i.toEquiv.toFun (x * y) = i.toEquiv.toFun x * i.toEquiv.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGrpCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : SemiRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : SemiRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : RingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : RingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : CommSemiRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : CommSemiRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : CommRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g ↦ F.map g ≫ adj.counit.app Y) ((fun f ↦ adj.unit.app X ≫ G.map f) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (fun f ↦ adj.unit.app X ≫ G.map f) ((fun g ↦ F.map g ≫ adj.counit.app Y) g) = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
h' : adj.counit = adj'.counit
⊢ adj = adj'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj = adj'

Tactic:
by

Goal state after: