mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)

Tactic:
rw [whisker_exchange]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ 𝟙 (F.map f₀₁ ≫ F.map f₁₃) =
    (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫
      (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
          (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv

Tactic:
simp [mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ ((F.mapComp' (𝟙 X₁) f f ⋯).symm ≪≫ (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom

Tactic:
mapComp'_id_comp

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (((λ_ (F.map f)).symm ≪≫ (F.mapId X₁).symm ▷ᵢ F.map f).symm ≪≫
        (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).symm ≪≫ F.mapComp' (𝟙 X₁) f f ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom

Tactic:
mapComp'_id_comp

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).symm ≪≫
        (λ_ (F.map f)).symm ≪≫ (F.mapId X₁).symm ▷ᵢ F.map f).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ Category.{?u.8, u + 1} (KleisliCat m)

Tactic:
refine { id_comp := ?_, comp_id := ?_, assoc := ?_ }

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f

case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f

case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
Module: Mathlib.Data.PFun

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

Tactic:
exact e ▸ h₃

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
⊢ (f.comp g).Dom = g.preimage f.Dom

Tactic:
by
  ext
  simp
  grind

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
this :
  Functor.whiskerRight ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom (map (𝟙 X)) ≫
      (mapPullbackAdj (𝟙 X)).counit =
    (mapPullbackAdj (𝟙 X)).counit
⊢ Functor.whiskerRight ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom (map (𝟙 X)) ≫
      (mapPullbackAdj (𝟙 X)).counit =
    (mapPullbackAdj (𝟙 X)).counit

Tactic:
Adjunction.rightAdjointUniq_hom_counit

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
this :
  Functor.whiskerRight ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom (map (𝟙 X)) ≫
      (mapPullbackAdj (𝟙 X)).counit =
    (mapPullbackAdj (𝟙 X)).counit
⊢ (mapPullbackAdj (𝟙 X)).counit = (mapPullbackAdj (𝟙 X)).counit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ Functor.whiskerRight ((mapPullbackAdj (f ≫ g)).rightAdjointUniq (mapPullbackAdj (f ≫ g))).hom (map (f ≫ g)) ≫
      (mapPullbackAdj (f ≫ g)).counit =
    (mapPullbackAdj (f ≫ g)).counit

Tactic:
Adjunction.rightAdjointUniq_hom_counit

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ (mapPullbackAdj (f ≫ g)).counit = (mapPullbackAdj (f ≫ g)).counit
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: 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₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
i₁ : X₁ ≅ Y₁
i₂ : X₂ ≅ Y₂
i₃ : X₃ ≅ Y₃
⊢ ((i₁.hom ⊗ₘ i₂.hom) ⊗ₘ i₃.hom) ≫ (α_ Y₁ Y₂ Y₃).hom ≫ (i₁.inv ⊗ₘ i₂.inv ⊗ₘ i₃.inv) = (α_ X₁ X₂ X₃).hom

Tactic:
by
  simp only [associator_naturality_assoc, ← tensor_comp, Iso.hom_inv_id, id_tensorHom,
    whiskerLeft_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_2} D
inst✝² : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
this : LF.IsRightKanExtension α
⊢ F.HasLeftDerivedFunctor W

Tactic:
simpa only [hasLeftDerivedFunctor_iff F L W] using HasRightKanExtension.mk LF α

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

Goal state before:
pp: G : Type u
inst✝ : Group G
⊢ PreservesFiniteLimits (forget (Action FintypeCat G))

Tactic:
change PreservesFiniteLimits (Action.forget FintypeCat _ ⋙ FintypeCat.incl)
  apply comp_preservesFiniteLimits

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 Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (F.map prod.fst)) ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x

Tactic:
simp only [fiberBinaryProductEquiv]
  change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.fst) _ = _
  erw [PreservesLimitPair.iso_inv_fst, Types.binaryProductIso_inv_comp_fst]
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X✝ : C
inst✝ : IsConnected X✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom (FintypeCat.uSwitch.map (F.map f)))
        ((FintypeCat.equivEquivIso.symm (Iso.app g' X)) ((F.obj X).uSwitchEquiv.symm x)))

Tactic:
← Functor.comp_map

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X✝ : C
inst✝ : IsConnected X✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom ((F ⋙ FintypeCat.uSwitch).map f))
        ((FintypeCat.equivEquivIso.symm (Iso.app g' X)) ((F.obj X).uSwitchEquiv.symm x)))
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
have : Nonempty (CostructuredArrow (parallelPair f g) Z) :=
      ⟨mk (Y := zero) (h₁ Z).some⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ 2 ≤ #(X ⟶ Y)

Tactic:
rw [Cardinal.two_le_iff]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ x y, x ≠ y
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
left : ψ.left ≅ ψ'.left
right : ψ.right ≅ ψ'.right
base : ψ.base ≅ ψ'.base
left_coherence :
  (CatCommSq.iso F ψ.left ψ.base F').hom ≫ Functor.whiskerRight left.hom F' =
    F.whiskerLeft base.hom ≫ (CatCommSq.iso F ψ'.left ψ'.base F').hom
right_coherence :
  (CatCommSq.iso G ψ.right ψ.base G').hom ≫ Functor.whiskerRight right.hom G' =
    G.whiskerLeft base.hom ≫ (CatCommSq.iso G ψ'.right ψ'.base G').hom
⊢ (CatCommSq.iso G ψ'.right ψ'.base G').hom ≫ Functor.whiskerRight right.inv G' =
    G.whiskerLeft base.inv ≫ (CatCommSq.iso G ψ.right ψ.base G').hom

Tactic:
by
        simpa using ψ'.squareRight.iso.hom ≫=
          IsIso.inv_eq_inv.mpr right_coherence =≫
          ψ.squareRight.iso.hom

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ Functor.whiskerRight ((pullbackPushforwardAdj (𝟙 I)).rightAdjointUniq (pullbackPushforwardAdj (𝟙 I))).hom
        (pullback (𝟙 I)) ≫
      (pullbackPushforwardAdj (𝟙 I)).counit =
    (pullbackPushforwardAdj (𝟙 I)).counit

Tactic:
Adjunction.rightAdjointUniq_hom_counit

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).counit = (pullbackPushforwardAdj (𝟙 I)).counit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ Functor.whiskerRight ((pullbackPushforwardAdj (f ≫ g)).rightAdjointUniq (pullbackPushforwardAdj (f ≫ g))).hom
        (pullback (f ≫ g)) ≫
      (pullbackPushforwardAdj (f ≫ g)).counit =
    (pullbackPushforwardAdj (f ≫ g)).counit

Tactic:
Adjunction.rightAdjointUniq_hom_counit

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).counit = (pullbackPushforwardAdj (f ≫ g)).counit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenPullbacks C
X : C
Y : Over X
m : Y ⟶ Over.mk (𝟙 X)
⊢ Over.Hom.left m = Over.Hom.left (Over.homMk Y.hom ⋯)

Tactic:
simpa using m.w

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ A.a ≫ ((comparisonAdjunction adj).unit.app A).f = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition,
    adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ adj.unit.app (adj.toMonad.obj A.A) ≫
      G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop d'✝ ⟶ unop d✝
g : unop c'✝ ⟶ unop c✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ᵣ unop c✝).op ≫ (unop d'✝ ⊴ᵣ Quiver.Hom.unop (op g)).op

Tactic:
apply Quiver.Hom.unop_inj
        simpa [MonoidalRightAction.action_exchange] using
          MonoidalRightAction.actionHom_def f g

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (R.X ⊗ P.X) ◁ Q.actLeft ≫ P.actLeft ▷ Q.X

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X P.X (S.X ⊗ Q.X)).inv

Tactic:
rw [whisker_exchange]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ (S.X ⊗ Q.X) ≫ P.X ◁ Q.actLeft

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X P.X (S.X ⊗ Q.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
    η ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q

Tactic:
rw [whisker_exchange]

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| η ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
    μ ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q

Tactic:
rw [whisker_exchange]

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| μ ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ M.actRight ▷ N₁.X ≫ M.X ◁ f.hom = (M.X ⊗ Y.X) ◁ f.hom ≫ M.actRight ▷ N₂.X

Tactic:
rw [whisker_exchange]

Goal state after: