mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ ∃ l, l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b

Tactic:
obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ :=
        h.exists_lift (a ≫ h₁₃.p₁) (b ≫ h₂₃.p₁) (a ≫ h₁₃.p₂) _ rfl
          (by simpa using w.symm =≫ f₃) (by simp)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
φ : x✝ ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₃.p₁
hφ₂ : φ ≫ h.p₂ = b ≫ h₂₃.p₁
hφ₃ : φ ≫ h.p₃ = a ≫ h₁₃.p₂
⊢ ∃ l, l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq 0 0 biprod.inl biprod.inr

Tactic:
by
  convert! of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)

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

Goal state before:
pp: case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯ ≫ homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
op_comp,

Goal state after:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯ ≫ homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯

Tactic:
op_comp,

Goal state after:
case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE hh ≫ homOfLE ⋯).op ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
op_comp,

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map ((homOfLE ⋯).op ≫ (homOfLE hh).op) ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m
Module: Mathlib.CategoryTheory.Localization.LocallySmall

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
this : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
⊢ W.HasLocalization

Tactic:
let L' : C ⥤ (InducedCategory _ L.obj) :=
    { obj X := X
      map f := InducedCategory.homMk (L.map f) }

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
this : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : C ⥤ InducedCategory D L.obj :=
  { obj := fun X ↦ X, map := fun {X Y} f ↦ InducedCategory.homMk (L.map f), map_id := ⋯, map_comp := ⋯ }
⊢ W.HasLocalization
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

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
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ (inv f).snd = inv f.snd

Tactic:
symm
  apply IsIso.inv_eq_of_hom_inv_id
  simp [← comp_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

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
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
⊢ whiskerRight
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj x))
            ⋯).hom
        F ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).iso.hom =
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).iso.hom ≫
      whiskerRight
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj x))
            ⋯).hom
        G

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by rintro _ _ _ ⟨_⟩ ⟨_⟩; rfl

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

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
⊢ (__Functor✝ ⋙ __Functor✝).map x✝ ≫ ↾joinM = ↾joinM ≫ __Functor✝.map x✝

Tactic:
ext _; exact joinM_map_map _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
h : J
⊢ { hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h = s.π.app h

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
w₃ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c))) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)))) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
w₄ :
  (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
⊢ (↾fun f ↦ R.map ((adj.homEquiv d (L.obj ((ihom d').obj (R.obj c)))).symm f)) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c))) =
    𝟙 ((coyoneda.obj (Opposite.op d)).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c))))

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
⊢ (fun f ↦ { app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯, naturality := ⋯ })
      ((fun g ↦
          {
            app := fun j ↦
              uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
            naturality := ⋯ })
        g) =
    g

Tactic:
ext j

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ ((fun f ↦ { app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯, naturality := ⋯ })
          ((fun g ↦
              {
                app := fun j ↦
                  uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
                naturality := ⋯ })
            g)).app
      j =
    g.app j
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ : J ⥤ C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ {
      app := fun j ↦
        uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
      naturality := ⋯ } =
    F₁ ◁ f₂ ≫
      { app := fun j ↦ uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ }

Tactic:
ext j

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ : J ⥤ C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ {
          app := fun j ↦
            uncurry
              ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
          naturality := ⋯ }.app
      j =
    (F₁ ◁ f₂ ≫
          {
            app := fun j ↦
              uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
            naturality := ⋯ }).app
      j
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
⊢ { app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯, naturality := ⋯ } =
    { app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯, naturality := ⋯ } ≫
      (ρ_ (functorEnrichedHom C F₁ F₃)).inv ≫
        functorEnrichedHom C F₁ F₃ ◁ (functorHomEquiv C) f₃ ≫ functorEnrichedComp C F₁ F₃ F₃'

Tactic:
ext j

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
⊢ { app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯, naturality := ⋯ }.app
      j =
    ({ app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯, naturality := ⋯ } ≫
          (ρ_ (functorEnrichedHom C F₁ F₃)).inv ≫
            functorEnrichedHom C F₁ F₃ ◁ (functorHomEquiv C) f₃ ≫ functorEnrichedComp C F₁ F₃ F₃').app
      j
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (LinearMap.id (Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A))))
      (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)

Tactic:
simp only [hom_comp, hom_ofHom, id_coe, id_eq, LinearMap.comp_apply]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (mul' R ↑A)
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A))))
        (((TensorProduct.mk R ↑A ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑A ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: case h₂
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
⊢ coprod.inr ≫ coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂) = coprod.inr ≫ 0

Tactic:
· simp [tensorHom_def', ← whiskerLeft_comp_assoc, coprod.inr_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow.obj j
⊢ ∃ c' t, g₁ ≫ p.toCostructuredArrow.map t = g₂ ≫ p.toCostructuredArrow.map t

Tactic:
· obtain ⟨k, a, h⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ p.isColimit
      g₁.left.hom g₂.left.hom ((CostructuredArrow.w g₁).trans (CostructuredArrow.w g₂).symm)
    exact ⟨k, a, by cat_disch⟩

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} V✝
inst✝⁷ : MonoidalCategory C✝
inst✝⁶ : MonoidalCategory V✝
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
inst✝ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
d d' : D
X✝ Y✝ : C × C
f✝ : X✝ ⟶ Y✝
⊢ ((ι C V D).obj d ⊠ (ι C V D).obj d').map f✝ ≫ convolutionUnitApp V d d' Y✝.1 Y✝.2 =
    convolutionUnitApp V d d' X✝.1 X✝.2 ≫ (tensor C ⋙ (ι C V D).obj (tensorObj C V d d')).map f✝

Tactic:
simp only [convolutionUnitApp_eq, Category.assoc, NatTrans.naturality_assoc]

Goal state after:
C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} V✝
inst✝⁷ : MonoidalCategory C✝
inst✝⁶ : MonoidalCategory V✝
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
inst✝ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
d d' : D
X✝ Y✝ : C × C
f✝ : X✝ ⟶ Y✝
⊢ (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj d')).app X✝ ≫
      (tensor C ⋙ DayConvolution.convolution ((ι C V D).obj d) ((ι C V D).obj d')).map f✝ ≫
        (tensorObjIsoConvolution C V d d').inv.app (Y✝.1 ⊗ Y✝.2) =
    (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj d')).app (X✝.1, X✝.2) ≫
      (tensorObjIsoConvolution C V d d').inv.app (X✝.1 ⊗ X✝.2) ≫ (tensor C ⋙ (ι C V D).obj (tensorObj C V d d')).map f✝
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g f₁ g₁ f₂ g₂ : u ⟶ v
h₁ : LeftHomotopy f₁ g₁
h₂ : LeftHomotopy f₂ g₂
⊢ Hom.left (f₁ + f₂) - Hom.left (g₁ + g₂) = u.hom ≫ (h₁.hom + h₂.hom)

Tactic:
simp [← h₁.comm, ← h₂.comm, add_sub_add_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g f₁ g₁ f₂ g₂ : u ⟶ v
h₁ : RightHomotopy f₁ g₁
h₂ : RightHomotopy f₂ g₂
⊢ Hom.right (f₁ + f₂) - Hom.right (g₁ + g₂) = (h₁.hom + h₂.hom) ≫ v.hom

Tactic:
simp [← h₁.comm, ← h₂.comm, add_sub_add_comm]

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
⊢ (λ_ ((Functor.pi' F).obj X)).inv =
    (Functor.pi' F).map (λ_ X).inv ≫
      (fun i ↦ Functor.OplaxMonoidal.δ (F i) (𝟙_ D) X) ≫ (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' F).obj X

Tactic:
by ext; simp

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
⊢ (ρ_ ((Functor.pi' F).obj X)).inv =
    (Functor.pi' F).map (ρ_ X).inv ≫
      (fun i ↦ Functor.OplaxMonoidal.δ (F i) X (𝟙_ D)) ≫ (Functor.pi' F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i)

Tactic:
by ext; simp

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
⊢ (λ_ ((Functor.pi F).obj X)).inv =
    (Functor.pi F).map (λ_ X).inv ≫
      (fun i ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) i) (X i)) ≫
        (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi F).obj X

Tactic:
by ext; simp

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
⊢ (ρ_ ((Functor.pi F).obj X)).inv =
    (Functor.pi F).map (ρ_ X).inv ≫
      (fun i ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) i)) ≫
        (Functor.pi F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ x✝¹ - x✝ = x✝¹ + -x✝

Tactic:
ext <;> simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
⊢ (M.map f).map g = M.map fun x x_1 x_2 ↦ g (f x_2)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝¹ : HasCoproduct obj₁
inst✝ : HasCoproduct obj₂
d : D₁ W Z
⊢ Sigma.ι obj₁ d ≫ t W Z = (↑d.fst).hom ≫ Sigma.ι obj₂ d

Tactic:
apply ι_colimMap

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝¹ : HasCoproduct obj₁
inst✝ : HasCoproduct obj₂
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ ιLeft f hf g ≫ t W Z = f ≫ ιRight f hf g

Tactic:
apply ι_colimMap

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ ≫ toSucc W Z = g₂ ≫ toSucc W Z

Tactic:
by
  simpa using D₂.condition f hf (g₁ := g₁ ≫ toStep W Z) (g₂ := g₂ ≫ toStep W Z)
    (by simp [reassoc_of% hg])

Goal state after: