mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
⊢ Nonempty (Cone F)

Tactic:
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), ((Functor.const J).obj Z).map f_1 ≫ f ⋯ = f ⋯ ≫ F.map f_1
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
⊢ PreservesColimitsOfShape J F

Tactic:
by
    let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm
    have := IsFiltered.of_equivalence e.symm
    exact preservesColimitsOfShape_of_equiv e F

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
⊢ M.det = N.det

Tactic:
have k_ne_succ : (Fin.castSucc k) ≠ k.succ := Fin.castSucc_lt_succ.ne

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
⊢ M.det = N.det
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
j : J
⊢ (Equiv.ulift.invFun ∘ f) ∘ c.ι j = (Equiv.ulift.invFun ∘ g) ∘ c.ι j

Tactic:
simp [Function.comp_assoc, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ (f fun j ↦ if h : P j then update x i (a + b) ⟨j, h⟩ else z ⟨j, h⟩) =
    (f fun j ↦ if h : P j then update x i a ⟨j, h⟩ else z ⟨j, h⟩) +
      f fun j ↦ if h : P j then update x i b ⟨j, h⟩ else z ⟨j, h⟩

Tactic:
by
    classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ A.det = B.det

Tactic:
by
  rw [← det_transpose A, ← det_transpose B]
  exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2

Tactic:
rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]

Goal state after:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∑ x ∈ preserving_snd, ↑↑(sign x) * ∏ i, blockDiagonal M (x i) i =
    ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2

n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ x ∈ univ, x ∉ preserving_snd → ↑↑(sign x) * ∏ i, blockDiagonal M (x i) i = 0
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
⊢ (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj ↔ ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj

Tactic:
by
  have : HasColimit F := ⟨_, ht⟩
  refine Iff.trans ?_ (colimit_eq_iff_aux F)
  rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]
  convert! Iff.rfl
  · exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm
  · exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z : M₂
⊢ MultilinearMap.mkPiRing R ι z = MultilinearMap.mkPiRing R ι 0 ↔ z = 0

Tactic:
mkPiRing_eq_iff

Goal state after:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z : M₂
⊢ z = 0 ↔ z = 0
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case empty
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
⊢ f a - f a = ∑ i ∈ ∅, f fun j ↦ if j ∈ ∅ → j < i then a j else if i = j then a j - b j else b j

Tactic:
sum_empty,

Goal state after:
case empty
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
⊢ f a - f a = 0
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
X : C
a : limit (F ⋙ coyoneda.obj (op X))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ ((const J).obj X).map x✝ ≫ (ConcreteCategory.hom (limit.π (F ⋙ coyoneda.obj (op X)) x✝¹)) a =
    (ConcreteCategory.hom (limit.π (F ⋙ coyoneda.obj (op X)) x✝²)) a ≫ F.map x✝

Tactic:
by simpa using! (limit.w_apply _ _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
x : P.obj (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ ((shrinkYoneda.{w, v, u}.obj X).map g ≫
      ↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Z)).symm f)))) x) =
    (↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x) ≫ P.map g

Tactic:
ext; simp [shrinkYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: 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✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limitObjIsoLimitCompEvaluation F i).inv ≫ (limit F).map f =
    limMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (limitObjIsoLimitCompEvaluation F j).inv

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv,
    limit_map_limitObjIsoLimitCompEvaluation_hom]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : LocallySmall.{max w w', v, u} C
X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ (shrinkYoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).map x✝ ≫
      (FunctorToTypes.shrinkCompUliftFunctorIso (yoneda.obj Y✝)).hom =
    (FunctorToTypes.shrinkCompUliftFunctorIso (yoneda.obj X✝)).hom ≫ shrinkYoneda.{max w w', v, u}.map x✝

Tactic:
ext; simp [shrinkYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
x : P.obj (unop X)
Y Z : C
g : Y ⟶ Z
⊢ ((shrinkCoyoneda.{w, v, u}.obj X).map g ≫
      ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Z)).symm f))) x) =
    (↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x) ≫ P.map g

Tactic:
ext; simp [shrinkYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : LocallySmall.{max w w', v, u} C
X✝ Y✝ : Cᵒᵖᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (shrinkCoyoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).map
        x✝ ≫
      (FunctorToTypes.shrinkCompUliftFunctorIso (coyoneda.obj Y✝)).hom =
    (FunctorToTypes.shrinkCompUliftFunctorIso (coyoneda.obj X✝)).hom ≫ shrinkCoyoneda.{max w w', v, u}.map x✝

Tactic:
ext; simp [shrinkYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ C₃ ⥤ C₄
f : G ⟶ G'
⊢ (bifunctorComp₁₂FunctorObj F₁₂).map f ≫
      {
        app := fun X₁ ↦
          { app := fun X₂ ↦ { app := fun X₃ ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun X₁ ↦
          { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ },
        naturality := ⋯ } ≫
      (bifunctorComp₁₂FunctorObj F₁₂').map f

Tactic:
by
    ext X₁ X₂ X₃
    dsimp
    simp only [← NatTrans.comp_app, NatTrans.naturality]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) → R.essImage Y

pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ R.essImage Y → IsIso (h.unit.app Y)

Tactic:
· intro
    exact ⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ R.essImage Y → IsIso (h.unit.app Y)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
⊢ 𝟙 X ⊗ₘ f = X ◁ f

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ f ⊗ₘ 𝟙 Y = f ▷ Y

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : V ⟶ W
⊢ f ▷ V ≫ (g ⊗ₘ h) = f ≫ g ⊗ₘ h

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ⊗ₘ g) ≫ W ◁ h = f ⊗ₘ g ≫ h

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' Y' Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h)

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (g ⊗ₘ 𝟙 W) ≫ (𝟙 Z ⊗ₘ f) = g ⊗ₘ f

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : W ⟶ X
⊢ f ⊗ₘ 0 = 0

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : Y ⟶ Z
⊢ 0 ⊗ₘ f = 0

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : W ⟶ X
g h : Y ⟶ Z
⊢ f ⊗ₘ (g + h) = f ⊗ₘ g + f ⊗ₘ h

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f g : W ⟶ X
h : Y ⟶ Z
⊢ (f + g) ⊗ₘ h = f ⊗ₘ h + g ⊗ₘ h

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j ↦ X ⊗ f j) j = X ◁ biproduct.π f j

Tactic:
by
  classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (F.map f ⊗ₘ F.map g) ≫ μ F Y Y' = μ F X X' ≫ F.map (f ⊗ₘ g)

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ (f ⊗ₘ ε F) ≫ μ F X (𝟙_ C) = f ▷ 𝟙_ D ≫ (ρ_ (F.obj X)).hom ≫ F.map (ρ_ X).inv

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ f ▷ 𝟙_ D ≫ (ρ_ (F.obj X)).hom = (f ⊗ₘ ε F) ≫ μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ δ F X X' ≫ (F.map f ⊗ₘ F.map g) = F.map (f ⊗ₘ g) ≫ δ F Y Y'

Tactic:
by
  simp [tensorHom_def]

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

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

Tactic:
by
  rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ δ F (𝟙_ C) X ≫ (η F ⊗ₘ f) = F.map (λ_ X).hom ≫ (λ_ (F.obj X)).inv ≫ 𝟙_ D ◁ f

Tactic:
by
  simp [tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasWidePushouts Cᵒᵖ
ι : Type w
⊢ HasLimitsOfShape (WidePullbackShape ι) C

Tactic:
← hasColimitsOfShape_opposite_opposite_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasWidePushouts Cᵒᵖ
ι : Type w
⊢ HasColimitsOfShape (WidePullbackShape ι)ᵒᵖ Cᵒᵖ
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasFiniteWidePullbacks Cᵒᵖ ↔ HasFiniteWidePushouts C

Tactic:
refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
  rw [← hasLimitsOfShape_opposite_opposite_iff]
  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasFiniteWidePushouts Cᵒᵖ
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
← hasColimitsOfShape_opposite_opposite_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasFiniteWidePushouts Cᵒᵖ
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePullbackShape J)ᵒᵖ Cᵒᵖ
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ?m.108)

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G

Tactic:
· apply PullbackCone.isLimitOfFlip
        apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
        exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom = (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv

Tactic:
apply (cancel_epi (α_ X Y Z).hom).1
  apply (cancel_mono (α_ Y Z X).hom).1
  simp [hexagon_forward]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : monomorphisms C f
hg : monomorphisms C g
⊢ monomorphisms C (f ≫ g)

Tactic:
rw [monomorphisms.iff] at hf hg ⊢
    apply mono_comp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.op g.op ↔ HasPullback f g

Tactic:
rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
hx : a✝ ∈ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a}
⊢ a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker

Tactic:
obtain ⟨j, j', u, a, rfl⟩ := hx

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a ∈
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker