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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
g : c ⟶ x
⊢ (Sigma.ι (fun x ↦ d) g ≫ Sigma.desc fun h ↦ (Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    Sigma.ι (fun x ↦ d) g ≫ f.app x

Tactic:
simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ← f.naturality,
              evaluationLeftAdjoint_obj_map, colimit.ι_desc_assoc,
              Discrete.functor_obj, Cofan.mk_pt, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a : FreeBicategory B
⊢ ∀ {b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
b

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
⊢ ∀ {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a : FreeBicategory B
⊢ ∀ {b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
b

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
⊢ ∀ {c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).hom = F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom

Tactic:
simp [← IsIso.inv_comp_eq, ← G.map₂_inv η.inv]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).inv =
    α.app a ◁ (G.mapComp f g).hom ≫
      (α_ (α.app a) (G.map f) (G.map g)).inv ≫
        (α.naturality f).inv ▷ G.map g ≫
          (α_ (F.map f) (α.app b) (G.map g)).hom ≫
            F.map f ◁ (α.naturality g).inv ≫ (α_ (F.map f) (F.map g) (α.app c)).inv ≫ (F.mapComp f g).inv ▷ α.app c

Tactic:
simp [naturality_comp_iso α f g]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a : B
⊢ ∀ {b : B} (f : a ⟶ b),
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
b

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
⊢ ∀ (f : a ⟶ b),
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a : B
⊢ ∀ {b : B} (f : a ⟶ b),
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
b

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
⊢ ∀ (f : a ⟶ b),
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a : B
⊢ ∀ {b : B} (f : a ⟶ b),
    F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f

Tactic:
b

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
⊢ ∀ (f : a ⟶ b),
    F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x✝ : ∫ F
⊢ (map (𝟙 F)).obj x✝ = (𝟭 (∫ F)).obj x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ F
⊢ (map (α ≫ β)).obj x✝ = (map α ⋙ map β).obj x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x✝ : ∫ᶜ F
⊢ (map (𝟙 F)).obj x✝ = (𝟭 (∫ᶜ F)).obj x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ᶜ F
⊢ (map (α ≫ β)).obj x✝ = (map α ⋙ map β).obj x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ ∀ (X : Core C), (F.core ⋙ Core.inclusion D).obj X = (Core.inclusion C ⋙ F).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
G : Type u₂
inst✝¹ : Groupoid G
G' : Type u₃
inst✝ : Groupoid G'
H : G ⥤ C
F : G' ⥤ G
⊢ ∀ (X : G'), (functorToCore (F ⋙ H)).obj X = (F ⋙ functorToCore H).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
G : Type u₂
inst✝¹ : Groupoid G
C' : Type u₄
inst✝ : Category.{v₄, u₄} C'
H : G ⥤ C
F : C ⥤ C'
⊢ ∀ (X : G), (functorToCore (H ⋙ F)).obj X = (functorToCore H ⋙ F.core).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: G : Type u₂
inst✝ : Groupoid G
⊢ ∀ (X : Core G), (inclusion G ⋙ functorToCore (𝟭 G)).obj X = (𝟭 (Core G)).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ (X : Core C), (functorToCore (inclusion C)).obj X = (𝟭 (Core C)).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ f₀₁ ≫ f₁₃ = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ f₀₁ ≫ f₁₃ = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a

Tactic:
· intro h
    rw [PFun.mem_fix_iff]
    exact Or.inr ⟨a', ha', h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ ∀ (j : J✝),
    (limit.cone (F ⋙ objects)).π.app j =
      (Iso.refl (limit.cone (F ⋙ objects)).pt).hom ≫ (objects.mapCone (HasLimits.limitCone F)).π.app j

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₁₂ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
D₁₂ : Type u_9
D₂₃ : Type u_10
C : Type u_11
D : Type u_12
E : Type u_13
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_3} C₃
inst✝¹⁷ : Category.{v_4, u_6} D₁
inst✝¹⁶ : Category.{v_5, u_7} D₂
inst✝¹⁵ : Category.{v_6, u_8} D₃
inst✝¹⁴ : Category.{v_7, u_4} C₁₂
inst✝¹³ : Category.{v_8, u_5} C₂₃
inst✝¹² : Category.{v_9, u_9} D₁₂
inst✝¹¹ : Category.{v_10, u_10} D₂₃
inst✝¹⁰ : Category.{v_11, u_11} C
inst✝⁹ : Category.{v_12, u_12} D
inst✝⁸ : Category.{v_13, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
    (((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e.hom ≫ lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₁ F₂' F₁' e.inv).app
                (L₁.obj X₁)).app
            (L₂.obj X₂)).app
        (L₃.obj X₃) =
      (((𝟙 F₁').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₁₂ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
D₁₂ : Type u_9
D₂₃ : Type u_10
C : Type u_11
D : Type u_12
E : Type u_13
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_3} C₃
inst✝¹⁷ : Category.{v_4, u_6} D₁
inst✝¹⁶ : Category.{v_5, u_7} D₂
inst✝¹⁵ : Category.{v_6, u_8} D₃
inst✝¹⁴ : Category.{v_7, u_4} C₁₂
inst✝¹³ : Category.{v_8, u_5} C₂₃
inst✝¹² : Category.{v_9, u_9} D₁₂
inst✝¹¹ : Category.{v_10, u_10} D₂₃
inst✝¹⁰ : Category.{v_11, u_11} C
inst✝⁹ : Category.{v_12, u_12} D
inst✝⁸ : Category.{v_13, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
    (((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₁ F₂' F₁' e.inv ≫ lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e.hom).app
                (L₁.obj X₁)).app
            (L₂.obj X₂)).app
        (L₃.obj X₃) =
      (((𝟙 F₂').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
⊢ ∀ (s : PullbackCone f g), lift s.fst s.snd ⋯ ≫ fst f g = s.fst

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
⊢ ∀ (s : PullbackCone f g), lift s.fst s.snd ⋯ ≫ snd f g = s.snd

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ pullbackObj f g),
    m ≫ fst f g = s.fst → m ≫ snd f g = s.snd → m = lift s.fst s.snd ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
⊢ f₁ ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ f₁ ▷ (X₂ ⊗ X₃)

Tactic:
simp only [← tensorHom_id, associator_naturality, id_tensorHom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
i : X₁ ≅ Y₁
⊢ i.hom ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom ≫ i.inv ▷ (X₂ ⊗ X₃) = (α_ X₁ X₂ X₃).hom

Tactic:
simp only [associator_naturality₁_assoc, ← whiskerRight_comp,
    Iso.hom_inv_id, whiskerRight_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
by cat_disch

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

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
F : A ⥤ C
G : B ⥤ C
x y z : A ⊕ B
f : x ⟶ y
g : y ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (f ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) f ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

Tactic:
by
    cases f <;> cases g <;> simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (α_ X (𝟙_ (Dial C)) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (X.braiding Y).hom ≫ (Y.braiding X).hom = 𝟙 (X ⊗ Y)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
f : Y ⟶ Z
⊢ (𝟙 X ⊗ₘ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ (f ⊗ₘ 𝟙 X)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
Z : Dial C
⊢ (f ⊗ₘ 𝟙 Z) ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ₘ f)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ (α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    ((X.braiding Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ₘ (X.braiding Z).hom)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    (𝟙 X ⊗ₘ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ⊗ₘ 𝟙 Y)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.EnrichedCat

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u₁
inst✝¹ : EnrichedCategory V D
E : Type u₂
inst✝ : EnrichedCategory V E
F G : EnrichedFunctor V C D
H I : EnrichedFunctor V D E
α : F ⟶ G
β : H ⟶ I
X : C
⊢ β.out.app (ForgetEnrichment.of V (F.obj («to» V X))) ≫
      homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to» V X)) (G.obj («to» V X))) =
    homOf V (homTo V (α.out.app X) ≫ H.map (F.obj («to» V X)) (G.obj («to» V X))) ≫
      β.out.app (ForgetEnrichment.of V (G.obj («to» V X)))

Tactic:
exact (β.out.naturality (α.out.app (ForgetEnrichment.of V X))).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
c : Wedge F
hc : IsLimit c
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift hc f hf ≫ Multifork.ι c j = f j

Tactic:
by
  apply IsLimit.fac

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
W₁ W₂ : Cowedge F
e : W₁.pt ≅ W₂.pt
he : ∀ (j : J), Multicofork.π W₁ j ≫ e.hom = Multicofork.π W₂ j
j : WalkingMultispan (multispanShapeCoend J)
f : (multispanShapeCoend J).L
⊢ W₁.ι.app (WalkingMultispan.left f) ≫ e.hom = W₂.ι.app (WalkingMultispan.left f)

Tactic:
simpa using! _ ≫= (he f.left)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift f hf ≫ π F j = f j

Tactic:
by
  apply IsLimit.fac

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F
⊢ map (𝟙 F) = 𝟙 (end_ F)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasCoend F
⊢ map (𝟙 F) = 𝟙 (coend F)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A₀

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 A₁

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 V₀

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 V₁

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ Z✝ : C ≌ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mkHom ((conjugateEquiv Z✝.toAdjunction X✝.toAdjunction) (asNatTrans (x✝¹ ≫ x✝)))).op.unop =
    ((mkHom ((conjugateEquiv Y✝.toAdjunction X✝.toAdjunction) (asNatTrans x✝¹))).op ≫
        (mkHom ((conjugateEquiv Z✝.toAdjunction Y✝.toAdjunction) (asNatTrans x✝))).op).unop

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ Z✝ : D ≌ C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mkHom ((conjugateEquiv X✝.symm.toAdjunction Z✝.symm.toAdjunction).invFun (asNatTrans (x✝¹ ≫ x✝)))).op.unop =
    ((mkHom ((conjugateEquiv X✝.symm.toAdjunction Y✝.symm.toAdjunction).invFun (asNatTrans x✝¹))).op ≫
        (mkHom ((conjugateEquiv Y✝.symm.toAdjunction Z✝.symm.toAdjunction).invFun (asNatTrans x✝))).op).unop

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
⊢ ∀ {a'_1 : 𝒳} (φ'_1 : a'_1 ⟶ b) [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = φ'_1

Tactic:
intro c ψ hψ
    use IsCartesian.map p f φ ψ ≫ φ'.inv
    refine ⟨⟨inferInstance, by simp⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    rw [Iso.eq_comp_inv]
    apply map_uniq
    simp only [assoc, hτ₂]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (g ≫ f) τ
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) y → y = τ ≫ φ.inv

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
⊢ ∀ (y : b ⟶ b'), (fun χ ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) y → y = φ.inv ≫ τ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₁ F₁
⊢ (λ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedId V F₁ ▷ functorEnrichedHom V F₁ F₂ ≫ functorEnrichedComp V F₁ F₁ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₂ F₂
⊢ (ρ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedHom V F₁ F₂ ◁ functorEnrichedId V F₂ ≫ functorEnrichedComp V F₁ F₂ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
by cat_disch

Goal state after: