mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }

Tactic:
· intro m hm
      ext
      dsimp only
      rw [← hm]
      apply (X.unit_assoc _).symm

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ (𝟙_ (Action W G)).ρ g ≫ ε F = ε F ≫ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g

Tactic:
by
        dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
        rw [Category.id_comp, F.map_id, Category.comp_id]

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
x✝¹ x✝ : Action V G
⊢ δ (F.mapAction G) x✝¹ x✝ ≫ μ (F.mapAction G) x✝¹ x✝ = 𝟙 ((F.mapAction G).obj (x✝¹ ⊗ x✝))

Tactic:
ext; dsimp; rw [δ_μ]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
⊢ B ⥤ A

Tactic:
by
  refine Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ h Y X) ?_
  intro X Y Y' g h
  rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]
  dsimp
  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
  erw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural]
  erw [adj₂.homEquiv_naturality_right]
  simp_rw [Functor.comp_map]
  -- This used to be `simp`, but we need `cat_disch` after https://github.com/leanprover/lean4/pull/2644
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝² : G.Full
inst✝¹ : G.Faithful
inst✝ : H.PreservesEpimorphisms
X : C
x✝ : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
⊢ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)

Tactic:
rw [← map_rightToLeft_app]; exact G.map_epi _

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
rw [← leftToRight_app_obj]; exact h _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
x : B
h : x ⟶ c
X✝ Y✝ : RightLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ η.left) ▷ f ≫ (α_ h Y✝.lift f).hom ≫ h ◁ Y✝.counit = (α_ h X✝.lift f).hom ≫ h ◁ X✝.counit

Tactic:
← RightLift.w η

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
x : B
h : x ⟶ c
X✝ Y✝ : RightLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ η.left) ▷ f ≫ (α_ h Y✝.lift f).hom ≫ h ◁ Y✝.counit = (α_ h X✝.lift f).hom ≫ h ◁ (η.left ▷ f ≫ Y✝.counit)
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ ((LeftExtension.mk u adj.unit).whisker h).unit ≫
      f ◁ (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
by
          dsimp only [whisker_extension, StructuredArrow.mk_right, whisker_unit,
            StructuredArrow.mk_hom_eq_self]
          bicategory

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
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
simp [mapComp'_id_comp]

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
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).inv = (F.mapId b₀).hom ▷ F.map f ≫ (λ_ (F.map f)).hom

Tactic:
simp [mapComp'_id_comp]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
h₃ :
  b ∈
    match e : (f a).get h₂ with
    | Sum.inl b => Part.some b
    | Sum.inr a' =>
      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' ⋯
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
split at h₃

Goal state after:
case h_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
heq✝ : (f a).get h₂ = Sum.inl b✝
h₃ : b ∈ Part.some b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

case h_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : (f a).get h₂ = Sum.inr 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'✝ ⋯
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ C a'

Tactic:
apply hbase
    convert! e
    exact Part.mem_unique h (fix_stop e)

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝¹ : α
x✝ : γ
⊢ x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ (↑g).comp (↑f) x✝¹

Tactic:
simp only [coe_val, comp_apply, Function.comp, Part.bind_some]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
eq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ⊗ₘ g)

Tactic:
by
  rw [tensorHom_def]
  exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)

Goal state after:
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ≫
          (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
            L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷
        L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
whiskerRight_comp,

Goal state after:
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
        ((μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
            L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷
          L'.obj X₄) ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
        ((μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
            L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷
          L'.obj X₄) ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
whiskerRight_comp,

Goal state after:
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
        (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
          (L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄) ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
        (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
          (L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄) ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
whiskerRight_comp,

Goal state after:
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
        (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
          L'.map (α_ X₁ X₂ X₃).hom ▷ L'.obj X₄ ≫
            ((μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄) ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ (μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
        L'.map (α_ X₁ X₂ X₃).hom ▷ L'.obj X₄ ≫
          ((μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
            (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
              L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
                L'.obj X₁ ◁
                  ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
                    L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
whiskerRight_comp,

Goal state after:
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ (μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
        L'.map (α_ X₁ X₂ X₃).hom ▷ L'.obj X₄ ≫
          ((μ L W ε X₁ (X₂ ⊗ X₃)).inv ▷ L'.obj X₄ ≫ (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄) ≫
            (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
              L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
                L'.obj X₁ ◁
                  ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
                    L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasCoend F
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasCoend F'
f : F ⟶ F'
j : J
⊢ ι F j ≫ map f = (f.app (op j)).app j ≫ ι F' j

Tactic:
by
  simp [coend.map]

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
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i) ≫ ((diagram V F₁ F₂).obj (Opposite.op i)).map f = (eHomEquiv V) (τ.app i ≫ F₂.map f)

Tactic:
dsimp
      simp only [eHomEquiv_comp, tensorHom_def_assoc, MonoidalCategory.whiskerRight_id,
        ← unitors_equal, assoc, Iso.inv_hom_id_assoc, eHomWhiskerLeft]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : ReflexiveRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.r ≫ F.map p₁ = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : ReflexiveRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.r ≫ F.map p₂ = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.s ≫ F.map p₁ = F.map p₂

Tactic:
simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.s ≫ F.map p₂ = F.map p₁

Tactic:
simp [← F.map_comp]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ 𝒴.p.IsHomLift f (F.map φ)

Tactic:
apply of_fac 𝒴.p f (F.map φ) (Eq.trans (F.w_obj a) (domain_eq 𝒳.p f φ))
    (Eq.trans (F.w_obj b) (codomain_eq 𝒳.p f φ))
  rw [← Functor.comp_map, congr_hom F.w]
  simpa using (fac 𝒳.p f φ)

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

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
rw [← hasPointwiseRightKanExtensionAt_iff_of_equivalence W.Q L F
    (Localization.uniq W.Q L W) (Localization.compUniqFunctor W.Q L W) (W.Q.obj X) (L.obj X)
    ((Localization.compUniqFunctor W.Q L W).app X)]
  exact ⟨fun h ↦ h.hasLimit', fun h ↦ ⟨h⟩⟩

Goal state after: