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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : C
⊢ α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D ⥤ E
e : F ≅ G
X₁ : C
X₂ : D
⊢ (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 ((F.obj X₁).obj X₂)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D ⥤ E
e : F ≅ G
X₁ : C
X₂ : D
⊢ (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 ((G.obj X₁).obj X₂)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ E ⥤ E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 (((F.obj X₁).obj X₂).obj X₃)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ E ⥤ E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 (((G.obj X₁).obj X₂).obj X₃)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (α.app Y)
⊢ α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : IsIso α
X : C
⊢ (inv α).app X = inv (α.app X)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
⊢ Function.LeftInverse hF.preimageIso F.mapIso

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
⊢ Function.RightInverse hF.preimageIso F.mapIso

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
app' : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f
X : C
⊢ (ofComponents app' naturality).app X = app' X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X) ∧
    (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Tactic:
· cases hq

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil

pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
· cases hq

Goal state after:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
by
    rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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 Z : C
p : X = Y
q : Y = Z
⊢ F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom ⋯)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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 Z : C
p : X = Y
q : Y = Z
⊢ F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso ⋯)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ f = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
simp only [Category.id_comp, eqToHom_refl, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Const

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : C ⥤ D
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (F ⋙ const J).map f ≫ (NatIso.ofComponents (fun x ↦ Iso.refl (((F ⋙ const J).obj Y).obj x)) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ Iso.refl (((F ⋙ const J).obj X).obj x)) ⋯).hom ≫
        (const J ⋙ (whiskeringRight J C D).obj F).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C × D
f : x ⟶ y
⊢ f = (𝟙 x.1 ×ₘ f.2) ≫ (f.1 ×ₘ 𝟙 y.2)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C × D
f : x ⟶ y
⊢ f = (f.1 ×ₘ 𝟙 x.2) ≫ (𝟙 y.1 ×ₘ f.2)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : B ⥤ C
⊢ F.associator (𝟭 B) G ≪≫ F.isoWhiskerLeft G.leftUnitor = isoWhiskerRight F.rightUnitor G

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ isoWhiskerRight (F.associator G H) K ≪≫ F.associator (G ⋙ H) K ≪≫ F.isoWhiskerLeft (G.associator H K) =
    (F ⋙ G).associator H K ≪≫ F.associator G (H ⋙ K)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : B ⥤ C
⊢ (F.associator (𝟭 B) G).hom ≫ F.whiskerLeft G.leftUnitor.hom = whiskerRight F.rightUnitor.hom G

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (F.associator G H).hom K ≫ (F.associator (G ⋙ H) K).hom ≫ F.whiskerLeft (G.associator H K).hom =
    ((F ⋙ G).associator H K).hom ≫ (F.associator G (H ⋙ K)).hom

Tactic:
by cat_disch

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

Goal state before:
pp: α : Type u₁
⊢ Function.LeftInverse Discrete.mk Discrete.as

Tactic:
by cat_disch

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

Goal state before:
pp: α : Type u₁
⊢ Function.RightInverse Discrete.mk Discrete.as

Tactic:
by cat_disch

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

Goal state before:
pp: α : Type u₁
inst✝ : Subsingleton α
⊢ ∀ (a b : Discrete α), a = b

Tactic:
by cat_disch

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

Goal state before:
pp: α : Type u₁
X Y : Discrete α
h : X.as = Y.as
⊢ X = Y

Tactic:
by cat_disch

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
i j : Discrete I
f : i ⟶ j
⊢ f ≫ Discrete.eqToHom ⋯ = 𝟙 i ∧ Discrete.eqToHom ⋯ ≫ f = 𝟙 j

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : Discrete I
f : i ⟶ i
⊢ (functor F).map f = 𝟙 (F i.as)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
i : Discrete I
⊢ (natIso f).app i = f i

Tactic:
by cat_disch

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ (f ≫ fun i ↦ inv (f i)) = 𝟙 X

Tactic:
by cat_disch

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ (fun i ↦ inv (f i)) ≫ f = 𝟙 Y

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Discrete J ⥤ C} (f : X ⟶ Y),
    ({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as, map_id := ⋯,
                map_comp := ⋯ }).map
          f ≫
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                            map_id := ⋯, map_comp := ⋯ }).obj
                      Y).obj
                  x))
            ⋯).hom =
      (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                            map_id := ⋯, map_comp := ⋯ }).obj
                      X).obj
                  x))
            ⋯).hom ≫
        (𝟭 (Discrete J ⥤ C)).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
X Y : C
f : X ⟶ Y
⊢ f ≫ eqToHom ⋯ = 𝟙 X ∧ eqToHom ⋯ ≫ f = 𝟙 Y

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ e.changeFunctor (Iso.refl e.functor) = e

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
G G' : C ⥤ D
iso₁ : e.functor ≅ G
iso₂ : G ≅ G'
⊢ (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map (e.unitIso.hom.app X) ≫ e.counitIso.hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X)

Tactic:
functor_unit_comp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 (e.functor.obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ⊤ f

Tactic:
by
  simp only [top_eq]

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

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso (Hom.left ff)
inst✝ : IsIso (Hom.right ff)
⊢ ff ≫ homMk (inv (Hom.left ff)) (inv (Hom.right ff)) ⋯ = 𝟙 f ∧
    homMk (inv (Hom.left ff)) (inv (Hom.right ff)) ⋯ ≫ ff = 𝟙 g

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse unop op

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse unop op

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse op unop

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse op unop

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P.inverseImage F f
⊢ P.inverseImage F (f ≫ e)

Tactic:
simpa [MorphismProperty.inverseImage, cancel_right_of_respectsIso] using hf

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D} (x : F ≅ G), P.map F ≤ P.map G

Tactic:
intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut X
⊢ (fun y ↦ { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ((fun x ↦ { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }) x✝) =
    x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut Y
⊢ (fun x ↦ { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ((fun y ↦ { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) x✝) =
    x✝

Tactic:
by cat_disch

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
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'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ (map α β).map { left := F₁.preimage φ.left, right := F₂.preimage φ.right, w := ⋯ } = φ

Tactic:
by cat_disch

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 cat_disch

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 cat_disch

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 cat_disch

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:
simpa using CategoryTheory.congr_fun w 1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
i : r ≅ t
⊢ Function.LeftInverse (fun h ↦ h.ofIsoLimit i.symm) fun h ↦ h.ofIsoLimit i

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
i : r ≅ t
⊢ Function.RightInverse (fun h ↦ h.ofIsoLimit i.symm) fun h ↦ h.ofIsoLimit i

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cone G ≌ Cone F
c : Cone G
⊢ Function.LeftInverse (ofRightAdjoint h.symm.toAdjunction) fun P ↦
    (ofRightAdjoint h.toAdjunction P).ofIsoLimit (h.unitIso.symm.app c)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cone G ≌ Cone F
c : Cone G
⊢ Function.RightInverse (ofRightAdjoint h.symm.toAdjunction) fun P ↦
    (ofRightAdjoint h.toAdjunction P).ofIsoLimit (h.unitIso.symm.app c)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cocone G ≌ Cocone F
c : Cocone G
⊢ Function.LeftInverse (IsColimit.ofLeftAdjoint h.toAdjunction) fun P ↦
    (IsColimit.ofLeftAdjoint h.symm.toAdjunction P).ofIsoColimit (h.unitIso.symm.app c)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cocone G ≌ Cocone F
c : Cocone G
⊢ Function.RightInverse (IsColimit.ofLeftAdjoint h.toAdjunction) fun P ↦
    (IsColimit.ofLeftAdjoint h.symm.toAdjunction P).ofIsoColimit (h.unitIso.symm.app c)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t s : Cone F
e : K ≌ J
⊢ Function.LeftInverse (ofWhiskerEquivalence e) fun h ↦ h.whiskerEquivalence e

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t s : Cone F
e : K ≌ J
⊢ Function.RightInverse (ofWhiskerEquivalence e) fun h ↦ h.whiskerEquivalence e

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
π : (const J).obj W ⟶ F
⊢ (fun f ↦ (t.extend f).π) ((fun π ↦ h.lift { pt := W, π := π }) π) = π

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = s

Tactic:
by
  rw [← coneOfHom_homOfCone h s]
  conv_lhs => simp only [homOfCone_coneOfHom]
  apply (coneOfHom_fac _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ (fun x ↦ x ≫ f) (f ≫ g) = (fun x ↦ x ≫ f) (𝟙 X)

Tactic:
by cat_disch

Goal state after: