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

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

Tactic:
rfl

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

Goal state before:
pp: case id_tensorHom_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 𝟙 (projectObj f✝ X✝ ⊗ projectObj f✝ Y✝) = 𝟙 (projectObj f✝ (X✝.tensor Y✝))

Tactic:
rfl

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

Goal state before:
pp: case mk.mk
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : X✝ ⟶ Y✝
a✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ : Y✝ ⟶ Z✝
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMap f X✝ Z✝ (Quot.mk (⇑(X✝.setoidHom Y✝)) a✝¹ ≫ Quot.mk (⇑(Y✝.setoidHom Z✝)) a✝) =
    projectMap f X✝ Y✝ (Quot.mk (⇑(X✝.setoidHom Y✝)) a✝¹) ≫ projectMap f Y✝ Z✝ (Quot.mk (⇑(Y✝.setoidHom Z✝)) a✝)

Tactic:
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✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : { of := X✝ }.of
⊢ (f ≫ g) x✝ = do
    let a ← f x✝
    g a

Tactic:
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✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : X✝.of
⊢ (do
      let a ← (ConcreteCategory.hom f.of) t
      (TypeCat.Hom.hom g.of) a) =
    ((fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x) t

Tactic:
rfl

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

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.OplaxLeftLinear C
c c' : C
d : D
⊢ δₗ F c (c' ⊙ₗ d) ≫ c ⊴ₗ δₗ F c' d ≫ (αₗ c c' (F.obj d)).inv = F.map (αₗ c c' d).inv ≫ δₗ F (c ⊗ c') d

Tactic:
simpa [-δₗ_associativity, -δₗ_associativity_assoc] using
    F.map (αₗ _ _ _).inv ≫=
      (δₗ_associativity F c c' d).symm =≫
      (αₗ _ _ _).inv

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✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ HasColimit (parallelPair f g ⋙ G)

Tactic:
hasColimit_iff_of_iso (diagramIsoParallelPair.{v₁} _)

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✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Mon C
X : Cᵒᵖ
⊢ Small.{w, v} ↑((yonedaMon.obj M).obj X)

Tactic:
by
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
X : Cᵒᵖ
⊢ Small.{w, v} ↑((yonedaGrp.obj M).obj X)

Tactic:
by
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
Z : C
f g : Z ⟶ X
m : Z ⟶ M
x : Z ⟶ X
⊢ lift m x ≫ γ = f ∧ x = g ↔ x = g ∧ lift m x ≫ γ = f

Tactic:
grind

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

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
X : C
smul✝ : M ⊙ₗ X ⟶ X
one_smul✝¹ : η ⊵ₗ X ≫ smul✝ = (λₗ X).hom
mul_smul✝¹ : μ ⊵ₗ X ≫ smul✝ = (αₗ M M X).hom ≫ M ⊴ₗ smul✝ ≫ smul✝
one_smul✝ : η ⊵ₗ X ≫ γ = (λₗ X).hom
mul_smul✝ : μ ⊵ₗ X ≫ γ = (αₗ M M X).hom ≫ M ⊴ₗ γ ≫ γ
⊢ { smul := smul✝, one_smul := one_smul✝¹, mul_smul := mul_smul✝¹ } =
    { smul := γ, one_smul := one_smul✝, mul_smul := mul_smul✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
f g : Z ⟶ X
a : { a // a.2 = f ∧ a.1 • a.2 = g }
⊢ (↑a).1 • f = g

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
f g : Z ⟶ X
a : { b // b • f = g }
⊢ (↑a, f).2 = f ∧ (↑a, f).1 • (↑a, f).2 = g

Tactic:
grind

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalLeftAction C D
A : C
inst✝ : MonObj A
M : Mod D A
⊢ (𝟙 M).hom = 𝟙 M.X

Tactic:
rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
⊢ (a + b) * c = a * c + b * c

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ

Tactic:
· have := lift (lift a b) c ≫= h
    simp only [lift_whiskerRight_assoc] at this
    simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]
    cat_disch

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ x ◁ (ihom.ev y).app ((ihom x).obj z) ≫ (ihom.ev x).app z = uncurry ((ihom.ev y).app ((ihom x).obj z))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
⊢ IsIso ((reflectorAdjunction i).unit.app (𝟙_ C))

Tactic:
have := reflective_products i
           refine Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩
           exact IsLimit.conePointUniqueUpToIso (limit.isLimit _) isTerminalTensorUnit

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

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
V : Type u₂
inst✝² : Category.{v₂, u₂} V
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalCategory V
F G : C ⊛⥤ V
natTrans✝¹ natTrans✝ : F.functor ⟶ G.functor
h : { natTrans := natTrans✝¹ }.natTrans = { natTrans := natTrans✝ }.natTrans
⊢ { natTrans := natTrans✝¹ } = { natTrans := natTrans✝ }

Tactic:
grind

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

Goal state before:
pp: case mk.id
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = X✝.normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: case mk.α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
x✝ : NormalMonoidalObject C
⊢ ((X✝.tensor Y✝).tensor Z✝).normalizeObj x✝ = (X✝.tensor (Y✝.tensor Z✝)).normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: case mk.α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor (Y✝.tensor Z✝)).normalizeObj x✝ = ((X✝.tensor Y✝).tensor Z✝).normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: case mk.l_hom
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ (unit.tensor X✝).normalizeObj x✝ = X✝.normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: case mk.l_inv
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (unit.tensor X✝).normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: case mk.ρ_hom
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor unit).normalizeObj x✝ = X✝.normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: case mk.ρ_inv
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (X✝.tensor unit).normalizeObj x✝

Tactic:
rfl

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

Goal state before:
pp: C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
revert n
  induction f using Hom.inductionOn
  case comp f g ihf ihg => simp [ihg, reassoc_of% (ihf _)]
  case whiskerLeft X' X Y f ih =>
    intro n
    dsimp only [normalizeObj_tensor, normalizeIsoApp'_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
    simp
  case whiskerRight X Y h η' ih =>
    intro n
    dsimp only [normalizeObj_tensor, normalizeIsoApp'_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
    rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]
    have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)
    simp [this]
  all_goals simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ x * y * z = x * (y * z)

Tactic:
convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_assoc A)) (x ⊗ₜ y ⊗ₜ z)

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

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ x * (y + z) = (Hom.hom μ) (x ⊗ₜ[R] (y + z))

Tactic:
rfl

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

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) ((x + y) ⊗ₜ[R] z)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : Mon (ModuleCat R)
⊢ (TensorProduct.mk R ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
          ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X).compr₂ₛₗ
      (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })) =
    (TensorProduct.mk R ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
          ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X).compr₂ₛₗ
      (Hom.hom
        (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
            (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
          μ))

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
          coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
        ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
        ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
          P.X ◁ TensorBimod.actLeft Q L) =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
        ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f✝ : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow C
hf : f ∈ (ofHoms f✝).toSet
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f✝ i), ⋯⟩) a = ⟨f, hf⟩

Tactic:
MorphismProperty.mem_toSet_iff,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f✝ : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow C
hf✝ : f ∈ (ofHoms f✝).toSet
hf : ofHoms f✝ f.hom
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f✝ i), ⋯⟩) a = ⟨f, hf✝⟩
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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
y : C
this :
  can ▷ F.obj y ≫
      (DayConvolution.unit U F).app (𝟙_ C, y) ≫
        ((U ⊛ F).descOfIsLeftKanExtension (DayConvolution.unit U F) F
              ((U ⊠ F).descOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ F)
                ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                          prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ F)))
                    ((NatIso.ofComponents (fun x ↦ (λ_ (F.obj x)).symm) ⋯).inv ≫
                      ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ λ_ x) ⋯).inv).app F))))).app
          (𝟙_ C ⊗ y) =
    ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                  prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ F)))
            ((NatIso.ofComponents (fun x ↦ (λ_ (F.obj x)).symm) ⋯).inv ≫
              ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ λ_ x) ⋯).inv).app F))).app
      ({ as := PUnit.unit }, y)
⊢ ((ConcreteCategory.hom
            (𝟙
              (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ F)))
          ((NatIso.ofComponents (fun x ↦ (λ_ (F.obj x)).symm) ⋯).inv ≫
            ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ λ_ x) ⋯).inv).app F)).app
      y =
    (λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv

Tactic:
rfl

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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝ : DayConvolution F U
x : C
this :
  F.obj x ◁ can ≫
      (DayConvolution.unit F U).app (x, 𝟙_ C) ≫
        ((F ⊛ U).descOfIsLeftKanExtension (DayConvolution.unit F U) F
              ((F ⊠ U).descOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ F)
                ((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                          prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F)))
                    ((NatIso.ofComponents (fun x ↦ (ρ_ (F.obj x)).symm) ⋯).inv ≫
                      ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))))).app
          (x ⊗ 𝟙_ C) =
    ((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                  prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F)))
            ((NatIso.ofComponents (fun x ↦ (ρ_ (F.obj x)).symm) ⋯).inv ≫
              ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))).app
      (x, { as := PUnit.unit })
⊢ ((ConcreteCategory.hom
            (𝟙
              (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F)))
          ((NatIso.ofComponents (fun x ↦ (ρ_ (F.obj x)).symm) ⋯).inv ≫
            ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F)).app
      x =
    (ρ_ (F.obj x)).hom ≫ F.map (ρ_ x).inv

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q : MorphismProperty C
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : HasPushouts C
A B A' : C
f : A ⟶ A'
g : A ⟶ B
x✝ : HasPushout f g
hf : P.underObj.ind (CategoryTheory.Under.mk f)
⊢ P.underObj.ind (CategoryTheory.Under.mk (pushout.inr f g))

Tactic:
exact ind_underObj_pushout g hf

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁
          (N.X ◁ f.hom ≫
            colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))
              WalkingParallelPair.one) ≫
        AssociatorBimod.invAux M N P'

Tactic:
dsimp [AssociatorBimod.invAux]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁
          (N.X ◁ f.hom ≫
            colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))
              WalkingParallelPair.one) ≫
        (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)).inv ≫
          coequalizer.desc
            ((α_ M.X N.X P'.X).inv ≫
              coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
                coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
                  ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft))
            ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
R : Presieve X
hR : R ∈ K.coverings X
h : ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)
⊢ ∀ (U : C) (g : U ⟶ X), R g → sourceLocalClosure K P (g ≫ f)

Tactic:
grind

Goal state after: