mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : (coconeQuotientDiag h u hUinV).pt ⟶ s.pt
hf : ∀ (j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)), (coconeQuotientDiag h u hUinV).ι.app j ≫ f = s.ι.app j
σ : Aut F
⊢ (ConcreteCategory.hom f.hom) ⟦σ⟧ = (ConcreteCategory.hom (coconeQuotientDiagDesc h u hUinV s).hom) ⟦σ⟧

Tactic:
| _ σ
     => 

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : (coconeQuotientDiag h u hUinV).pt ⟶ s.pt
hf : ∀ (j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)), (coconeQuotientDiag h u hUinV).ι.app j ≫ f = s.ι.app j
σ : Aut F
⊢ (ConcreteCategory.hom f.hom) ⟦σ⟧ = (ConcreteCategory.hom (coconeQuotientDiagDesc h u hUinV s).hom) ⟦σ⟧
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case e'_2
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath) =
    inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)

pp: case e'_3
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Tactic:
<;>

Goal state after:
case e'_2
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath) =
    inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)

case e'_3
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Groupoid C
S✝ : Subgroupoid C
s : Set (Subgroupoid C)
S : Subgroupoid C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ F ∈ sInf s → F ∈ S

pp: case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
T : Subgroupoid C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
⊢ F ∈ sInf s

Tactic:
<;>

Goal state after:
case refine_1
C : Type u
inst✝ : Groupoid C
S✝ : Subgroupoid C
s : Set (Subgroupoid C)
S : Subgroupoid C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ F ∈ sInf s → F ∈ S

case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
T : Subgroupoid C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
⊢ F ∈ sInf s
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp.mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs → x ∈ univ

pp: case mp.mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ univ → x ∈ S.objs

Tactic:
<;>

Goal state after:
case mp.mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs → x ∈ univ

case mp.mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ univ → x ∈ S.objs
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map p✝ ∈ S.arrows (φ.obj c✝) (φ.obj d✝)

pp: case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map q✝ ∈ S.arrows (φ.obj d✝) (φ.obj e✝)

Tactic:
<;>

Goal state after:
case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map p✝ ∈ S.arrows (φ.obj c✝) (φ.obj d✝)

case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map q✝ ∈ S.arrows (φ.obj d✝) (φ.obj e✝)
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ f.functor ⋙ f.inverse ⋙ e.inverse

Tactic:
← Functor.assoc f.functor,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ (f.functor ⋙ f.inverse) ⋙ e.inverse
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 ≫ q ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}

Tactic:
gq,

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 ⋯
⊢ φ.map f ≫ eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯ ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}
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 e : D} {p : c ⟶ d},
    p ∈ {x | Map.Arrows φ hφ S c d x} →
      ∀ {q : d ⟶ e}, q ∈ {x | Map.Arrows φ hφ S d e x} → p ≫ q ∈ {x | Map.Arrows φ hφ S c e x}

Tactic:
by
    rintro _ _ _ _ ⟨f, hf⟩ q hq
    obtain ⟨c₃, c₄, g, he, rfl, hg, gq⟩ := (Map.arrows_iff φ hφ S q).mp hq
    cases hφ he; rw [gq, ← eq_conj_eqToHom, ← φ.map_comp]
    constructor; exact S.mul hf hg

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: 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

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

Tactic:
<;>

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

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

Tactic:
<;>

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.Join.Sum

Goal state before:
pp: case inl
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
h' : (Sum.inl_ C D).obj x✝ ⟶ (Sum.inl_ C D).obj y✝
heq : (fromSum C D).map ((Sum.inl_ C D).map f✝) = (fromSum C D).map h'
⊢ (Sum.inl_ C D).map f✝ = h'

pp: case inr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : D
f✝ : x✝ ⟶ y✝
h' : (Sum.inr_ C D).obj x✝ ⟶ (Sum.inr_ C D).obj y✝
heq : (fromSum C D).map ((Sum.inr_ C D).map f✝) = (fromSum C D).map h'
⊢ (Sum.inr_ C D).map f✝ = h'

Tactic:
<;>

Goal state after:
case inl
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
h' : (Sum.inl_ C D).obj x✝ ⟶ (Sum.inl_ C D).obj y✝
heq : (fromSum C D).map ((Sum.inl_ C D).map f✝) = (fromSum C D).map h'
⊢ (Sum.inl_ C D).map f✝ = h'

case inr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : D
f✝ : x✝ ⟶ y✝
h' : (Sum.inr_ C D).obj x✝ ⟶ (Sum.inr_ C D).obj y✝
heq : (fromSum C D).map ((Sum.inr_ C D).map f✝) = (fromSum C D).map h'
⊢ (Sum.inr_ C D).map f✝ = h'
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)

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

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
⊢ (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)

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)
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
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✝

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
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✝

Tactic:
<;>

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✝

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)

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

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
⊢ (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)

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)
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
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✝

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
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✝

Tactic:
<;>

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✝

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)

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

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
⊢ (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)

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)
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
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✝

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
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✝

Tactic:
<;>

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✝

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✝