mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝⁴ : HasCoproduct X
inst✝³ : EffectiveEpi (Sigma.desc π)
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W✝ : C
x✝² : (a : α) → X a ⟶ W✝
x✝¹ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), π a ≫ x✝ = x✝² a
⊢ x✝ = EffectiveEpi.desc (Sigma.desc π) (Sigma.desc x✝²) ⋯

Tactic:
apply EffectiveEpi.uniq (Sigma.desc π)
    ext
    simpa using hm _

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

Goal state before:
pp: case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom

Tactic:
rw [← cancel_mono e₁.inv, assoc, assoc, assoc, Iso.hom_inv_id, comp_id,
    ← rightUnitor_naturality, rightUnitor_hom_app,
    ← tensorHom_id, ← id_tensorHom, ← tensor_comp_assoc, comp_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: case fst
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).1 = (↑((ConcreteCategory.hom g).toFun y)).1

Tactic:
exact congr($h₁ y)

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a : Fib p S
⊢ p.obj ((ι S).obj a) = S

Tactic:
simp only [← comp_obj, comp_const, const_obj_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
⊢ ((α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
        enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄) ≫
      end_.π (diagram V F₁ F₄) j =
    (enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄) ≫ end_.π (diagram V F₁ F₄) j

Tactic:
conv_lhs =>
    rw [assoc, assoc, enrichedComp_π,
      tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
      comp_whiskerRight_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ← associator_inv_naturality_assoc]

Goal state after:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
⊢ (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      (α_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j) (((diagram V F₂ F₃).obj (Opposite.op j)).obj j)
            (((diagram V F₃ F₄).obj (Opposite.op j)).obj j)).inv ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
            ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) =
    (enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄) ≫ end_.π (diagram V F₁ F₄) j
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

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

Tactic:
dsimp [totalLeftDerived, totalLeftDerivedCounit]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
this : Mono S.f
⊢ Epi S.g

Tactic:
rw [hP.jointlyReflectEpimorphisms.epi_iff]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
this : Mono S.f
⊢ ∀ (i : I), Epi ((F i).map S.g)
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
hf : ∀ (i : I), IsIso (ShortComplex.homologyMap ((F i).mapShortComplex.map f))
⊢ ∀ (i : I), IsIso ((F i).map (ShortComplex.homologyMap f))

Tactic:
exact fun i ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (ShortComplex.homologyFunctorIso (F i))).app
      (Arrow.mk f))).1 (hf i)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FintypeCat

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Type u_1
inst✝ : ∀ (j : J), Finite (K.obj j)
this : Fintype ↑K.sections
⊢ Fintype (limit K)

Tactic:
exact Fintype.ofEquiv (sections K) (Types.limitEquivSections K).symm

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.snd f g))) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b

Tactic:
simp only [fiberPullbackEquiv, Functor.comp_map, Iso.toEquiv_symm_fun]
  change ((Types.pullbackIsoPullback _ _).inv ≫ _ ≫
    (F ⋙ FintypeCat.incl).map (pullback.snd f g)) _ = _
  erw [PreservesPullback.iso_inv_snd, Types.pullbackIsoPullback_inv_snd]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ autMap (f ≫ g) = autMap g ∘ autMap f

Tactic:
by
  refine funext fun σ ↦ autMap_unique _ σ _ ?_
  rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
m : s.pt ⟶ (mk bc.pt (c₁.combPairHoms c₂ bc)).pt
hm : ∀ (j : ι₁ ⊕ ι₂), m ≫ (mk bc.pt (c₁.combPairHoms c₂ bc)).proj j = s.proj j
⊢ m ≫ proj bc WalkingPair.right =
    (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      proj bc WalkingPair.right

Tactic:
refine Fan.IsLimit.hom_ext h₂ _ _ (fun a ↦ by aesop)

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F✝ : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F✝
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : ContAction FintypeCat (Aut F)
⊢ (functorToContAction F).essImage X

Tactic:
have : ContinuousSMul (Aut F) X.obj.V := X.2
    obtain ⟨A, ⟨i⟩⟩ := exists_lift_of_continuous (F := F) X
    exact ⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
i : ι
⊢ (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i

Tactic:
simp only [px, is₁, is₂, ← piComparison_comp_π, ← PreservesProduct.iso_hom,
      FintypeCat.comp_apply]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
i : ι
⊢ (ConcreteCategory.hom (Pi.π (fun b ↦ F.obj (X b)) i))
      ((ConcreteCategory.hom (PreservesProduct.iso F X).hom)
        ((ConcreteCategory.hom (PreservesProduct.iso F X).inv)
          ((FintypeCat.productEquiv fun i ↦ F.obj (X i)).symm x))) =
    x i
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.fst =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.fst

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.snd =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.snd

Tactic:
· simpa [← Functor.map_comp, P] using Over.w Q.hom.left

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.snd =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.snd
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 ≫ biprod.inr = 0

Tactic:
← assoc

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) ≫ biprod.inr = 0
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 ≫ biprod.inl = 0

Tactic:
← assoc

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) ≫ biprod.inl = 0
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: 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
⊢ mapWhiskerLeft (𝟭 A) (F.whiskerLeft η) =
    (mapCompRight A F G).hom ≫ (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F H).inv

Tactic:
apply natTrans_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
⊢ (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: 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
⊢ mapWhiskerRight (F.whiskerLeft η) (𝟭 D) =
    (mapCompLeft D F G).hom ≫ (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F H).inv

Tactic:
apply natTrans_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
⊢ (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: 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
⊢ mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H) =
    (mapCompRight A F H).hom ≫
      Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A G H).inv

Tactic:
apply natTrans_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
⊢ (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: 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
⊢ mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D) =
    (mapCompLeft D F H).hom ≫ Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv

Tactic:
apply natTrans_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
⊢ (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)

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)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: 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
⊢ mapWhiskerLeft (𝟭 A) (F.associator G H).hom =
    (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:
apply natTrans_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
⊢ (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)

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)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: 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
⊢ mapWhiskerRight (F.associator G H).hom (𝟭 E) =
    (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:
apply natTrans_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
⊢ (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)

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)