mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case mp
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂) → z₁ = z₂

pp: case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ z₁ = z₂ → ∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂

Tactic:
<;>

Goal state after:
case mp
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂) → z₁ = z₂

case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ z₁ = z₂ → ∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
⊢ s.piecewise a v j = v j

Tactic:
s.piecewise_eq_of_notMem _ _ hjs

Goal state after:
case neg
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
⊢ v j = v j
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.map f.1 ≫ T.app Y.1).app X.2

pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.1).map f.2

Tactic:
NatTrans.naturality,

Goal state after:
case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (T.app X.1 ≫ Y✝.map f.1).app X.2

case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.1).map f.2
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j = F.map ((liftLimit t).π.app j)

Tactic:
rw [← liftedLimitMapsToOriginal_inv_map_π (t := t)]
  simp only [← Category.assoc, ← Cone.category_comp_hom,
    Iso.hom_inv_id, Cone.category_id_hom, Category.id_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
⊢ IsLimit c

Tactic:
by
    have : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) := ⟨_, hc⟩
    have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using! this
    have := reflectsLimit_of_reflectsIsomorphisms F (forget₂ (ModuleCat R) AddCommGrpCat)
    exact isLimitOfReflects _ hc

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

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ X ◁ f h✝ = X ◁ f h✝

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ X ◁ f' h✝ = X ◁ f' h✝

Tactic:
<;>

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ X ◁ f h✝ = X ◁ f h✝

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ X ◁ f' h✝ = X ◁ f' h✝
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : P
⊢ f h✝ ▷ Z = f h✝ ▷ Z

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : ¬P
⊢ f' h✝ ▷ Z = f' h✝ ▷ Z

Tactic:
<;>

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : P
⊢ f h✝ ▷ Z = f h✝ ▷ Z

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : ¬P
⊢ f' h✝ ▷ Z = f' h✝ ▷ Z
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ f ⊗ₘ g h✝ = f ⊗ₘ g h✝

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ f ⊗ₘ g' h✝ = f ⊗ₘ g' h✝

Tactic:
<;>

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ f ⊗ₘ g h✝ = f ⊗ₘ g h✝

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ f ⊗ₘ g' h✝ = f ⊗ₘ g' h✝
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ g h✝ ⊗ₘ f = g h✝ ⊗ₘ f

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ g' h✝ ⊗ₘ f = g' h✝ ⊗ₘ f

Tactic:
<;>

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ g h✝ ⊗ₘ f = g h✝ ⊗ₘ f

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ g' h✝ ⊗ₘ f = g' h✝ ⊗ₘ f
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : Linear R F
X : C
r : R
⊢ r • F.map (𝟙 X) = r • 𝟙 (F.obj X)

Tactic:
F.map_id

Goal state after:
case mp
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : Linear R F
X : C
r : R
⊢ r • 𝟙 (F.obj X) = r • 𝟙 (F.obj X)
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 Y : C
f : J → C
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)

Tactic:
cases nonempty_fintype J
  ext
  simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum,
    id_tensor_comp, tensorIso_hom, leftDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
    biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero]
  simp_rw [← id_tensorHom]
  simp only [← id_tensor_comp, biproduct.ι_π]
  simp only [id_tensor_comp, tensor_dite, comp_dite]
  simp

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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ G.map (F.map x✝¹) ▷ G.obj (F.obj x✝) ≫ μ G (F.obj Y✝) (F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ G.map (F.map (x✝¹ ▷ x✝))

Tactic:
μ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ μ G (F.obj X✝) (F.obj x✝) ≫ G.map (F.map x✝¹ ▷ F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ G.map (F.map (x✝¹ ▷ x✝))
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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      G.map (μ F x✝² x✝¹) ▷ G.obj (F.obj x✝) ≫
        μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
μ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F x✝² x✝¹ ▷ F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul

pp: case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul

Tactic:
<;>

Goal state after:
case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul

case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
x✝¹ : ℤ
x✝ : ↑A
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

pp: case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
x✝¹ : ℤ
x✝ : ↑B
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

Tactic:
<;>

Goal state after:
case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
x✝¹ : ℤ
x✝ : ↑A
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
x✝¹ : ℤ
x✝ : ↑B
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod G) ≫ η (F.prod G)).1 = (𝟙 (𝟙_ (D × C'))).1

pp: case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod G) ≫ η (F.prod G)).2 = (𝟙 (𝟙_ (D × C'))).2

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod G) ≫ η (F.prod G)).1 = (𝟙 (𝟙_ (D × C'))).1

case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod G) ≫ η (F.prod G)).2 = (𝟙 (𝟙_ (D × C'))).2
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).1 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).1

pp: case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).2 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).2

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).1 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).1

case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).2 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).2
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝).1 = (𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)).1

pp: case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝).2 = (𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)).2

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝).1 = (𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)).1

case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝).2 = (𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)).2
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝).1 = (𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))).1

pp: case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝).2 = (𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))).2

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝).1 = (𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))).1

case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝).2 = (𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))).2
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeUnop s)).unop

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
    simpa only [Quiver.Hom.op_unop, IsColimit.fac] using! w (unop j)

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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).2 = η G

Tactic:
change G.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).2 = δ G X Y

Tactic:
change G.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

Goal state after: