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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
⊢ (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
⊢ (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint

Tactic:
by
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
⊢ (X : (monadicAdjunction U).toMonad.Algebra) → RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)

Tactic:
by
    intro X
    simp only [Monad.adj_counit]
    exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this✝ : L'.IsLeftAdjoint
⊢ (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv).IsLeftAdjoint

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this✝ : L'.IsLeftAdjoint
⊢ (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv).IsLeftAdjoint

Tactic:
by
      infer_instance

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

Goal state before:
pp: case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      eqToHom ⋯

Tactic:
have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))

Goal state after:
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
this : (normalizeIso (normalizeAux p f✝) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g✝) h).hom ≫ eqToHom ⋯
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      eqToHom ⋯
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
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
rw [← whisker_exchange]
          bicategory

Goal state after:
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
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
rw [← whisker_exchange]
          bicategory

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
a b : B
f : a ⟶ b
⊢ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
rw [← whisker_exchange]
          bicategory

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

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).fiber ≫ eqToHom ⋯

Tactic:
· simp [Cat.Hom.comp_toFunctor, naturality_id_hom_app, Cat.Hom.id_toFunctor, ← Category.assoc,
        ← Functor.map_comp, ← Cat.Hom₂.comp_app]

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

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
⊢ IsLocallyGroupoid (Pith B)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case none
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
hb : none ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨none, hb⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨none, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩

pp: case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨some b, hb⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨some b, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩

Tactic:
· exact (hb rfl).elim

Goal state after:
case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨some b, hb⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨some b, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
⊢ opEquivalence.functor.IsEquivalence

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
⊢ opEquivalence.inverse.IsEquivalence

Tactic:
infer_instance

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y Z : limit (F ⋙ objects)
f : limit (homDiagram X Y)
g : limit (homDiagram Y Z)
j j' : J
h : j ⟶ j'
⊢ (hom ((homDiagram X Z).map h)) ((hom (limit.π (homDiagram X Y) j)) f ≫ (hom (limit.π (homDiagram Y Z) j)) g) =
    (hom (limit.π (homDiagram X Y) j')) f ≫ (hom (limit.π (homDiagram Y Z) j')) g

Tactic:
by
    simp [-homDiagram_obj, ← limit.w_apply (homDiagram X Y) h f,
      ← limit.w_apply (homDiagram Y Z) h g]

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
⊢ ∀ (X : ↑s.pt), (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.obj X = (s.π.app j).toFunctor.obj X

Tactic:
intro

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X✝ : ↑s.pt
⊢ (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.obj X✝ = (s.π.app j).toFunctor.obj X✝
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ m = limitConeLift F s

Tactic:
by
    symm
    ext1
    refine CategoryTheory.Functor.ext ?_ ?_
    · intro X
      apply Types.limit_ext.{v, v}
      intro j
      simp [← comp_apply, ← w j]
    · intro X Y f
      have (j : _) := Functor.congr_hom congr($((w j).symm).toFunctor) f
      simp [this, -homDiagram_obj, limit_π_homDiagram_eqToHom]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
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_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₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.hom.app F₁').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) ≫
      (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
              (uncurry₃.obj F₂') (uncurry₃.map τ)).app
          (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) ≫
        (((currying₃.unitIso.inv.app F₂').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃

Tactic:
simp only [currying₃_unitIso_hom_app_app_app_app, Functor.id_obj,
    currying₃_unitIso_inv_app_app_app_app, Functor.comp_obj,
    Category.comp_id, Category.id_comp]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
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_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₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
          (uncurry₃.obj F₂') (uncurry₃.map τ)).app
      (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃
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₁ Y₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
this✝ : IsIso (L'.map (f₁ ▷ Y₁))
this : IsIso (L'.map (X₂ ◁ f₂))
⊢ IsIso (L'.map (f₁ ▷ Y₁) ≫ L'.map (X₂ ◁ f₂))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X : C
⊢ PreservesColimitsOfShape (Discrete WalkingPair) (tensorLeft X)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ (equivalence C D).functor.IsEquivalence

Tactic:
infer_instance

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

Goal state before:
pp: case refine_1
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
          (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
            L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)

Tactic:
rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc,
        ← tensor_comp, ← associator_naturality, id_comp, ← comp_id e₁.hom,
        tensor_comp, ← associator_naturality_assoc, ← comp_id (𝟙 ((L').obj X₄)),
        ← tensor_comp_assoc, associator_naturality, comp_id, comp_id,
        ← tensor_comp_assoc, assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id,
        ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id, id_tensorHom_id, id_tensorHom_id, comp_id]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (p.map (𝟙 a)) (𝟙 a)

Tactic:
infer_instance

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

Goal state before:
pp: case refl
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)

Tactic:
infer_instance

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

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 φ
⊢ p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f

Tactic:
simp only [fac p f φ, eqToHom_trans_assoc, eqToHom_refl, id_comp]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
⊢ p.IsHomLift (p.map φ) φ

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p.map φ
⊢ p.IsHomLift (p.map φ) φ

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 S) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
T : 𝒮
ψ : b ⟶ c
f : R ⟶ T
inst✝ : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G H : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
β : BasedNatTrans G H
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a ≫ β.app a)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
inst✝ : IsIso α
⊢ IsIso ((forgetful 𝒳 𝒴).map α)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
X✝ Y✝ Z✝ : p.Fiber S
φ : { φ // p.IsHomLift (𝟙 S) φ }
ψ : { φ // p.IsHomLift (𝟙 S) φ }
this✝ : p.IsHomLift (𝟙 S) ↑φ
this : p.IsHomLift (𝟙 S) ↑ψ
⊢ p.IsHomLift (𝟙 S) (↑φ ≫ ↑ψ)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ p.IsHomLift g (τ' ≫ (domainUniqueUpToIso p (p.map φ) φ ψ).hom)

Tactic:
infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a b : Fib p S
φ : a ⟶ b
⊢ 𝟙 S = eqToHom ⋯ ≫ (ι S ⋙ p).map φ ≫ eqToHom ⋯

Tactic:
Functor.congr_hom (comp_const S)

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a b : Fib p S
φ : a ⟶ b
⊢ 𝟙 S = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ ((const (Fib p S)).obj S).map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : HasFibers p
inst✝ : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
⊢ p.IsCartesian f ((Fib.mkIsoSelf ⋯).hom ≫ IsPreFibered.pullbackMap ha f)

Tactic:
infer_instance

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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
⊢ ∀ {b' : 𝒳} (g_1 : T ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift ((f ≫ g) ≫ g_1) φ'],
    ∃! χ, p.IsHomLift g_1 χ ∧ (φ ≫ ψ) ≫ χ = φ'

Tactic:
intro c'

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
c' : 𝒳
⊢ ∀ (g_1 : T ⟶ p.obj c') (φ' : a ⟶ c') [p.IsHomLift ((f ≫ g) ≫ g_1) φ'], ∃! χ, p.IsHomLift g_1 χ ∧ (φ ≫ ψ) ≫ χ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
⊢ ∀ {b' : 𝒳} (g_1 : T ⟶ p.obj b') (φ' : b ⟶ b') [p.IsHomLift (g ≫ g_1) φ'], ∃! χ, p.IsHomLift g_1 χ ∧ ψ ≫ χ = φ'

Tactic:
intro c'

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
⊢ ∀ (g_1 : T ⟶ p.obj c') (φ' : b ⟶ c') [p.IsHomLift (g ≫ g_1) φ'], ∃! χ, p.IsHomLift g_1 χ ∧ ψ ≫ χ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S S' : 𝒮
a b b' : 𝒳
f : R ⟶ S
f' : R ⟶ S'
g : S ≅ S'
h : f' = f ≫ g.hom
φ : a ⟶ b
φ' : a ⟶ b'
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian f' φ'
⊢ p.IsHomLift f φ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseLeftDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ F.HasPointwiseLeftDerivedFunctorAt W (L.objPreimage Y)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
inst✝ : F.HasPointwiseLeftDerivedFunctor W
this : W.Q.HasPointwiseRightKanExtension F
⊢ W.Q.HasRightKanExtension F

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
C' : Type ?u.4
D : Type u_2
D' : Type ?u.8
H : Type u_3
H' : Type ?u.12
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, ?u.4} C'
inst✝⁵ : Category.{v_3, u_2} D
inst✝⁴ : Category.{v_4, ?u.8} D'
inst✝³ : Category.{v_5, u_3} H
inst✝² : Category.{v_6, ?u.12} H'
LF'' LF' LF : D ⥤ H
F F' F'' : C ⥤ H
e : F ≅ F'
L : C ⥤ D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
α'₂ : L ⋙ LF' ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasLeftDerivedFunctor W
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)

Tactic:
infer_instance

Goal state after: