mathlib-initiative/mathlib-tactics huggingface dataset:
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 b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ eqToHom ⋯ ≫
      { base := (f ≫ g).base,
          fiber :=
            (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.fiber =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).fiber

Tactic:
simp only [Cat.Hom.comp_toFunctor, comp_obj, categoryStruct_comp_base, Quiver.Hom.comp_toLoc,
        categoryStruct_comp_fiber, eqToHom_refl, map_comp, ← Cat.Hom.comp_map, assoc,
        NatTrans.naturality_assoc]

Goal state after:
case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((G.map (f.base.toLoc ≫ g.base.toLoc)).toFunctor.obj ((α.app { as := a.base }).toFunctor.obj a.fiber)) ≫
      (α.naturality (f.base.toLoc ≫ g.base.toLoc)).inv.toNatTrans.app a.fiber ≫
        (α.app { as := c.base }).toFunctor.map ((F.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app a.fiber) ≫
          ((F.map g.base.toLoc).toFunctor ⋙ (α.app { as := c.base }).toFunctor).map f.fiber ≫
            (α.app { as := c.base }).toFunctor.map g.fiber =
    (G.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app ((α.app { as := a.base }).toFunctor.obj a.fiber) ≫
      (G.map g.base.toLoc).toFunctor.map ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber) ≫
        (α.naturality g.base.toLoc).inv.toNatTrans.app ((F.map f.base.toLoc).toFunctor.obj a.fiber) ≫
          ((F.map g.base.toLoc).toFunctor ⋙ (α.app { as := c.base }).toFunctor).map f.fiber ≫
            (α.app { as := c.base }).toFunctor.map g.fiber
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:
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:
cat_disch

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

Goal state before:
pp: case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).toFunctor.obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Tactic:
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
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 } =
    𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }

Tactic:
ext1
    · dsimp
    · 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.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:
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:
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:
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G H : D ⥤ E
η : G ≅ H
⊢ (F.isoWhiskerLeft η).core = F.coreComp G ≪≫ F.core.isoWhiskerLeft η.core ≪≫ (F.coreComp H).symm

Tactic:
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
η : F ≅ G
H : D ⥤ E
⊢ (isoWhiskerRight η H).core = F.coreComp H ≪≫ isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm

Tactic:
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
⊢ F.leftUnitor.core = (𝟭 C).coreComp F ≪≫ isoWhiskerRight (Functor.coreId C) F.core ≪≫ F.core.leftUnitor

Tactic:
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
⊢ F.rightUnitor.core = F.coreComp (𝟭 D) ≪≫ F.core.isoWhiskerLeft (Functor.coreId D) ≪≫ F.core.rightUnitor

Tactic:
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
G : D ⥤ E
H : E ⥤ E'
⊢ (F.associator G H).core =
    (F ⋙ G).coreComp H ≪≫
      isoWhiskerRight (F.coreComp G) H.core ≪≫
        F.core.associator G.core H.core ≪≫ (F.core.isoWhiskerLeft (G.coreComp H)).symm ≪≫ (F.coreComp (G ⋙ H)).symm

Tactic:
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:
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:
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:
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:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
by
          rw [← whisker_exchange]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
⊢ ∀ (s : LeftExtension f (𝟙 a ≫ h)) (τ : (LeftExtension.mk u adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯

Tactic:
intro s τ₀

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
⊢ τ₀ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
by
          rw [← whisker_exchange]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
⊢ ∀ (s : LeftLift u (h ≫ 𝟙 a)) (τ : (LeftLift.mk f adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯

Tactic:
intro s τ₀

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
⊢ τ₀ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯
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:
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:
cat_disch

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

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
as✝ : objects.obj x✝²
f : { as := as✝ } ⟶ { as := { as := as✝ }.as }
⊢ ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
    (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f

Tactic:
cat_disch

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

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
xcc : (typeToCat ⋙ connectedComponents).obj x✝²
x : ↑(typeToCat.obj x✝²)
h : ⟦x⟧ = xcc
⊢ (ConcreteCategory.hom
          ((typeToCat ⋙ connectedComponents).map x✝ ≫
            ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝¹)) (𝟙 typeToCat.obj x✝¹).toFunctor)).toFun
      xcc =
    (ConcreteCategory.hom
          (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝²)) (𝟙 typeToCat.obj x✝²).toFunctor ≫
            (𝟭 (Type u)).map x✝)).toFun
      xcc

Tactic:
cat_disch

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

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
G : C ⟶ typeToCat.obj X
cc : connectedComponents.obj C
w✝ : ↑C
h✝ : ⟦w✝⟧ = cc
⊢ (ConcreteCategory.hom
          ((TypeCat.homEquiv.trans
                ((ConnectedComponents.typeToCatHomEquiv (↑C) X).trans (Functor.equivCatHom (↑C) (Discrete X)))).symm
            G)).toFun
      cc =
    (ConcreteCategory.hom
          (connectedComponents.map G ≫
            { app := fun X ↦ ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X)) (𝟙 typeToCat.obj X).toFunctor,
                  naturality := ⋯ }.app
              X)).toFun
      cc

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
      · injection Part.mem_unique ⟨h₁, h₂⟩ h'
      · rw [WellFounded.fixF_eq]
        -- Porting note: used to be simp [h₁, h₂]
        apply Part.mem_assert h₁
        split
        next e =>
          injection h₂.symm.trans e with h; simp [h]
        next e =>
          injection h₂.symm.trans e

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:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Subobject.pullback_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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:
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:
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
⊢ pullbackMap f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (pullbackObj f g)

Tactic:
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
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
comm₁' : f'' ≫ δ₃ = δ₁ ≫ f'
comm₂' : g'' ≫ δ₃ = δ₂ ≫ g'
⊢ pullbackMap f' g' f'' g'' δ₁ δ₂ δ₃ comm₁' comm₂' ≫ pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂ =
    pullbackMap f g f'' g'' (δ₁ ≫ γ₁) (δ₂ ≫ γ₂) (δ₃ ≫ γ₃) ⋯ ⋯

Tactic:
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:
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:
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:
cat_disch

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Subobject.pullback_comp

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Subobject.pullback_comp

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Subobject.pullback_comp

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Subobject.pullback_comp

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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₂ : Dial C
⊢ 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
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₁ 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:
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 (𝟙_ (Dial C)) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y

Tactic:
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:
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:
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:
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:
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:
cat_disch

Goal state after: