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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f ↔
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f →
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb) →
    Arrows φ hφ S c d f
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p, inl := P.decompId_i,
            inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.fst ≫
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inl +
      { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.snd ≫
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inr =
    𝟙
      { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
          inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
          inr_snd := ⋯ }.pt

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ ({ pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.fst ≫
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inl +
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.snd ≫
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inr).f =
    (𝟙
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.pt).f
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)

Tactic:
constructor

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ g ∈ S.arrows a b
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f✝ : c✝ ⟶ d✝
hf✝ : f✝ ∈ S.arrows c✝ d✝
⊢ φ.map (Groupoid.inv f✝) ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c✝) x}

Tactic:
constructor

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f✝ : c✝ ⟶ d✝
hf✝ : f✝ ∈ S.arrows c✝ d✝
⊢ Groupoid.inv f✝ ∈ S.arrows d✝ c✝
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.decompId_i ≫ P.complement.decompId_p = 0

Tactic:
ext

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (P.decompId_i ≫ P.complement.decompId_p).f = Hom.f 0
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f : c✝ ⟶ d✝
hf : f ∈ S.arrows c✝ d✝
c₄ : C
q : φ.obj d✝ ⟶ φ.obj c₄
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c₄) x}
g : d✝ ⟶ c₄
he : φ.obj d✝ = φ.obj d✝
hg : g ∈ S.arrows d✝ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ φ.map (f ≫ g) ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}

Tactic:
constructor

Goal state after:
case refl
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f : c✝ ⟶ d✝
hf : f ∈ S.arrows c✝ d✝
c₄ : C
q : φ.obj d✝ ⟶ φ.obj c₄
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c₄) x}
g : d✝ ⟶ c₄
he : φ.obj d✝ = φ.obj d✝
hg : g ∈ S.arrows d✝ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ f ≫ g ∈ S.arrows c✝ c₄
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.complement.decompId_i ≫ P.decompId_p = 0

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (P.complement.decompId_i ≫ P.decompId_p).f = Hom.f 0
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.lift P.decompId_p P.complement.decompId_p ≫ biprod.desc P.decompId_i P.complement.decompId_i =
    𝟙 ((toKaroubi C).obj P.X)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (biprod.lift P.decompId_p P.complement.decompId_p ≫ biprod.desc P.decompId_i P.complement.decompId_i).f =
    (𝟙 ((toKaroubi C).obj P.X)).f
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty ↔ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))

Tactic:
constructor

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ S.arrows c c
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl.refl.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))

Tactic:
constructor

Goal state after:
case refl.refl.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Groupoid.inv f ≫ γ ≫ f ∈ S.arrows c' c'
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d

case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
left✝ : c✝ ∈ D
right✝ : d✝ ∈ D
⊢ Groupoid.inv p✝ ∈ {_f | d✝ ∈ D ∧ c✝ ∈ D}

Tactic:
constructor

Goal state after:
case left
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
left✝ : c✝ ∈ D
right✝ : d✝ ∈ D
⊢ d✝ ∈ D

case right
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
left✝ : c✝ ∈ D
right✝ : d✝ ∈ D
⊢ c✝ ∈ D
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
left✝¹ : c✝ ∈ D
right✝¹ : d✝ ∈ D
q✝ : d✝ ⟶ e✝
left✝ : d✝ ∈ D
right✝ : e✝ ∈ D
⊢ p✝ ≫ q✝ ∈ {_f | c✝ ∈ D ∧ e✝ ∈ D}

Tactic:
constructor

Goal state after:
case left
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
left✝¹ : c✝ ∈ D
right✝¹ : d✝ ∈ D
q✝ : d✝ ⟶ e✝
left✝ : d✝ ∈ D
right✝ : e✝ ∈ D
⊢ c✝ ∈ D

case right
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
left✝¹ : c✝ ∈ D
right✝¹ : d✝ ∈ D
q✝ : d✝ ⟶ e✝
left✝ : d✝ ∈ D
right✝ : e✝ ∈ D
⊢ e✝ ∈ D
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
⊢ full ∅ = ⊥

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full ∅).arrows x✝² x✝¹ ↔ x✝ ∈ ⊥.arrows x✝² x✝¹
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
⊢ full univ = ⊤

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full univ).arrows x✝² x✝¹ ↔ x✝ ∈ ⊤.arrows x✝² 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
F : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A F G).hom ≫ (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F 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
F : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F G).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F 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
F : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A F G).hom ≫ (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F 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
F : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F G).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F 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
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
⊢ (inclLeft A D).whiskerLeft (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)) =
    (inclLeft A D).whiskerLeft
      ((mapCompLeft D F G).hom ≫ (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F 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
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
x✝ : A
⊢ ((inclLeft A D).whiskerLeft (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))).app x✝ =
    ((inclLeft A D).whiskerLeft
          ((mapCompLeft D F G).hom ≫
            (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F 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
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
⊢ (inclRight A D).whiskerLeft (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)) =
    (inclRight A D).whiskerLeft
      ((mapCompLeft D F G).hom ≫ (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F 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
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
x✝ : D
⊢ ((inclRight A D).whiskerLeft (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))).app x✝ =
    ((inclRight A D).whiskerLeft
          ((mapCompLeft D F G).hom ≫
            (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F 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
F G : B ⥤ C
η : F ⟶ G
H : C ⥤ D
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H)) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A F H).hom ≫
        Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A 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
F G : B ⥤ C
η : F ⟶ G
H : C ⥤ D
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F H).hom ≫
            Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A 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
F G : B ⥤ C
η : F ⟶ G
H : C ⥤ D
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H)) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A F H).hom ≫
        Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A 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
F G : B ⥤ C
η : F ⟶ G
H : C ⥤ D
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F H).hom ≫
            Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A 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
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
⊢ (inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)) =
    (inclLeft A D).whiskerLeft
      ((mapCompLeft D F H).hom ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D 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
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
x✝ : A
⊢ ((inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclLeft A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D 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
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
⊢ (inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)) =
    (inclRight A D).whiskerLeft
      ((mapCompLeft D F H).hom ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D 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
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
x✝ : D
⊢ ((inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclRight A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D 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 : B ⥤ C
G : C ⥤ D
H : D ⥤ E
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A (F ⋙ G) H).hom ≫
        Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
          ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A 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 : B ⥤ C
G : C ⥤ D
H : D ⥤ E
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
              ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
                (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A 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 : B ⥤ C
G : C ⥤ D
H : D ⥤ E
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A (F ⋙ G) H).hom ≫
        Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
          ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A 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 : B ⥤ C
G : C ⥤ D
H : D ⥤ E
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
              ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
                (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv)).app
      x✝