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

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
⊢ (inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E)) =
    (inclLeft A E).whiskerLeft
      ((mapCompLeft E (F ⋙ G) H).hom ≫
        Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
          ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
            (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv)

Tactic:
ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
x✝ : A
⊢ ((inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclLeft A E).whiskerLeft
          ((mapCompLeft E (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
              ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
                (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
⊢ (inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E)) =
    (inclRight A E).whiskerLeft
      ((mapCompLeft E (F ⋙ G) H).hom ≫
        Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
          ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
            (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv)

Tactic:
ext

Goal state after:
case h₂
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
x✝ : E
⊢ ((inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclRight A E).whiskerLeft
          ((mapCompLeft E (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
              ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
                (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)

Tactic:
ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)

Tactic:
ext

Goal state after:
case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)

Tactic:
ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)

Tactic:
ext

Goal state after:
case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)

Tactic:
ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)

Tactic:
ext

Goal state after:
case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)

Tactic:
ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)

Tactic:
ext

Goal state after:
case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
⊢ { f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝ =
    x✝¹.proj x✝

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝² : Fan fun x ↦ U
x✝¹ : α
x✝ : x✝².pt.I
⊢ ({ f := fun i a ↦ (x✝².proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝².proj a).φ i } ≫ (U.powerFan α).proj x✝¹).f x✝ =
    (x✝².proj x✝¹).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
i✝ : x✝¹.pt.I
⊢ ({ f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝).φ i✝ ≫
      eqToHom ⋯ =
    (x✝¹.proj x✝).φ i✝
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
⊢ ((monoFactorisation f).I.map g ≫
      ↾fun x ↦
        match x with
        | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx)) =
    (↾fun x ↦
        match x with
        | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
      H.I.map g

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x✝ : (monoFactorisation f).I.obj X
⊢ (ConcreteCategory.hom
          ((monoFactorisation f).I.map g ≫
            ↾fun x ↦
              match x with
              | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx))).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              match x with
              | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
            H.I.map g)).toFun
      x✝
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
⊢ {
        app := fun X ↦
          ↾fun x ↦
            match x with
            | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx),
        naturality := ⋯ } ≫
      H.m =
    (monoFactorisation f).m

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
x✝¹ : C
x✝ : (monoFactorisation f).I.obj x✝¹
⊢ (ConcreteCategory.hom
          (({
                  app := fun X ↦
                    ↾fun x ↦
                      match x with
                      | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx),
                  naturality := ⋯ } ≫
                H.m).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom ((monoFactorisation f).m.app x✝¹)).toFun x✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
⊢ powerMap (f ≫ g) α = powerMap f α ≫ powerMap g α

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
x✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).f x✝ = (powerMap f α ≫ powerMap g α).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).φ i✝ ≫ eqToHom ⋯ = (powerMap f α ≫ powerMap g α).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (Pi.map fun a ↦ f.φ (i✝ a) ≫ g.φ (f.f (i✝ a))) ≫ 𝟙 (∏ᶜ W.obj ∘ (f ≫ g).f ∘ i✝) =
    (Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.map fun a ↦ g.φ (f.f (i✝ a))

Tactic:
ext

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
b✝ : α
⊢ ((Pi.map fun a ↦ f.φ (i✝ a) ≫ g.φ (f.f (i✝ a))) ≫ 𝟙 (∏ᶜ W.obj ∘ (f ≫ g).f ∘ i✝)) ≫ Pi.π (W.obj ∘ g.f ∘ f.f ∘ i✝) b✝ =
    ((Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.map fun a ↦ g.φ (f.f (i✝ a))) ≫ Pi.π (W.obj ∘ g.f ∘ f.f ∘ i✝) b✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
⊢ U.mapPower (g ∘ f) = U.mapPower g ≫ U.mapPower f

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
x✝ : (U.power γ).I
⊢ (U.mapPower (g ∘ f)).f x✝ = (U.mapPower g ≫ U.mapPower f).f x✝

case h₂
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
i✝ : (U.power γ).I
⊢ (U.mapPower (g ∘ f)).φ i✝ ≫ eqToHom ⋯ = (U.mapPower g ≫ U.mapPower f).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
i✝ : (U.power γ).I
⊢ (Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g (f x))) ≫ 𝟙 (∏ᶜ U.obj ∘ i✝ ∘ g ∘ f) =
    (Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g x)) ≫ Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝ ∘ g) (f x)

Tactic:
ext

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
i✝ : (U.power γ).I
b✝ : α
⊢ ((Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g (f x))) ≫ 𝟙 (∏ᶜ U.obj ∘ i✝ ∘ g ∘ f)) ≫ Pi.π (U.obj ∘ (i✝ ∘ g) ∘ f) b✝ =
    ((Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g x)) ≫ Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝ ∘ g) (f x)) ≫
      Pi.π (U.obj ∘ (i✝ ∘ g) ∘ f) b✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
⊢ U.mapPower g ≫ powerMap f α = powerMap f β ≫ V.mapPower g

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
x✝ : (U.power β).I
⊢ (U.mapPower g ≫ powerMap f α).f x✝ = (powerMap f β ≫ V.mapPower g).f x✝

case h₂
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
i✝ : (U.power β).I
⊢ (U.mapPower g ≫ powerMap f α).φ i✝ ≫ eqToHom ⋯ = (powerMap f β ≫ V.mapPower g).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
i✝ : (U.power β).I
⊢ ((Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g x)) ≫ Pi.map fun a ↦ f.φ (i✝ (g a))) ≫ 𝟙 (∏ᶜ V.obj ∘ f.f ∘ i✝ ∘ g) =
    (Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.lift fun x ↦ Pi.π (V.obj ∘ f.f ∘ i✝) (g x)

Tactic:
ext

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
i✝ : (U.power β).I
b✝ : α
⊢ (((Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g x)) ≫ Pi.map fun a ↦ f.φ (i✝ (g a))) ≫ 𝟙 (∏ᶜ V.obj ∘ f.f ∘ i✝ ∘ g)) ≫
      Pi.π (V.obj ∘ (f.f ∘ i✝) ∘ g) b✝ =
    ((Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.lift fun x ↦ Pi.π (V.obj ∘ f.f ∘ i✝) (g x)) ≫ Pi.π (V.obj ∘ (f.f ∘ i✝) ∘ g) b✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
⊢ U.mapPower f ≫ U.powerπ a = U.powerπ (f a)

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
x✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).f x✝ = (U.powerπ (f a)).f x✝

case h₂
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
i✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).φ i✝ ≫ eqToHom ⋯ = (U.powerπ (f a)).φ i✝
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : HasZeroMorphisms C₂
inst✝³ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝² : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
⊢ coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) =
    0

Tactic:
ext

Goal state after:
case h₁
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : HasZeroMorphisms C₂
inst✝³ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝² : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
⊢ coprod.inl ≫
      coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫
        (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) =
    coprod.inl ≫ 0

case h₂
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : HasZeroMorphisms C₂
inst✝³ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝² : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
⊢ coprod.inr ≫
      coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫
        (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) =
    coprod.inr ≫ 0
Module: Mathlib.CategoryTheory.Join.Basic

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 ⥤ E
Fᵣ Gᵣ : D ⥤ E'
αₗ : Fₗ ⟶ Gₗ
αᵣ : Fᵣ ⟶ Gᵣ
⊢ mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ = mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ

Tactic:
ext

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' : Type u₄
inst✝ : Category.{v₄, u₄} E'
Fₗ Gₗ : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
αₗ : Fₗ ⟶ Gₗ
αᵣ : Fᵣ ⟶ Gᵣ
x✝ : C ⋆ D
⊢ (mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ).app x✝ = (mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ).app x✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
⊢ { f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } = 𝟙 X

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).f x✝ =
    (𝟙 X).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 X).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
⊢ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom } = 𝟙 Y

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).f x✝ =
    (𝟙 Y).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 Y).φ i✝