mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ G.obj X ◁ G.map g ≫
      (adj.homEquiv (G.obj X ⊗ G.obj Y') (X ⊗ Y'))
        (δ F (G.obj X) (G.obj Y') ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')) =
    (adj.homEquiv (G.obj X ⊗ G.obj X') (X ⊗ X')) (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (X ◁ g)

Tactic:
by
    simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp,
      assoc, ← δ_natural_right_assoc F]
    suffices F.obj (G.obj X) ◁ F.map (G.map g) ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
    simpa using NatTrans.whiskerLeft_app_tensor_app adj.counit adj.counit (f := g) _

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

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h

pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k

Tactic:
<;>

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
i : HasPushout f g
⊢ G.map f ≫ G.map (pushout.inl f g) = G.map g ≫ G.map (pushout.inr f g)

Tactic:
simp only [← G.map_comp, pushout.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono (F.map f)

Tactic:
F.map_id

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono (F.map f)
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)

Tactic:
F.map_id

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi (F.map f)
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
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).ContainsIdentities
⊢ (⨅ i, W i).ContainsIdentities

Tactic:
by
  rw [← sInf_range]
  exact sInf (by simpa)

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
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsStableUnderComposition
⊢ (⨅ i, W i).IsStableUnderComposition

Tactic:
by
  rw [← sInf_range]
  exact sInf (by simpa)

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
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsMultiplicative
⊢ (⨅ i, W i).IsMultiplicative

Tactic:
by
  rw [← sInf_range]
  exact sInf (by simpa)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map ((α_ X✝ Y✝ Z✝).hom ≫ (β X✝ (Y✝ ⊗ Z✝)).hom ≫ (α_ Y✝ Z✝ X✝).hom) =
    μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map ((β X✝ Y✝).hom ▷ Z✝ ≫ (α_ Y✝ X✝ Z✝).hom ≫ Y✝ ◁ (β X✝ Z✝).hom)

Tactic:
refine (cancel_epi (μ F _ _ ▷ _)).1 ?_

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ μ F X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map ((α_ X✝ Y✝ Z✝).hom ≫ (β X✝ (Y✝ ⊗ Z✝)).hom ≫ (α_ Y✝ Z✝ X✝).hom) =
    μ F X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map ((β X✝ Y✝).hom ▷ Z✝ ≫ (α_ Y✝ X✝ Z✝).hom ≫ Y✝ ◁ (β X✝ Z✝).hom)
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    adj.unit.app (X ⊗ Y) ▷ G.obj (F.obj Z) ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
          G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
rw [← comp_whiskerRight_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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    (adj.unit.app (X ⊗ Y) ≫
          G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case h₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ pushout.inl g₁.op g₂.op ≫ (pushoutIsoOpPullback g₁.op g₂.op).hom ≫ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    pushout.inl g₁.op g₂.op ≫
      pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom

pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ pushout.inr g₁.op g₂.op ≫ (pushoutIsoOpPullback g₁.op g₂.op).hom ≫ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    pushout.inr g₁.op g₂.op ≫
      pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom

Tactic:
<;>

Goal state after:
case h₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ pushout.inl g₁.op g₂.op ≫ (pushoutIsoOpPullback g₁.op g₂.op).hom ≫ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    pushout.inl g₁.op g₂.op ≫
      pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom

case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ pushout.inr g₁.op g₂.op ≫ (pushoutIsoOpPullback g₁.op g₂.op).hom ≫ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    pushout.inr g₁.op g₂.op ≫
      pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case h₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ ((pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op ≫ (pullbackIsoOpPushout f₁.op f₂.op).inv) ≫ pullback.fst f₁.op f₂.op =
    ((pullbackIsoOpPushout g₁.op g₂.op).inv ≫ pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) ≫
      pullback.fst f₁.op f₂.op

pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ ((pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op ≫ (pullbackIsoOpPushout f₁.op f₂.op).inv) ≫ pullback.snd f₁.op f₂.op =
    ((pullbackIsoOpPushout g₁.op g₂.op).inv ≫ pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) ≫
      pullback.snd f₁.op f₂.op

Tactic:
<;>

Goal state after:
case h₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ ((pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op ≫ (pullbackIsoOpPushout f₁.op f₂.op).inv) ≫ pullback.fst f₁.op f₂.op =
    ((pullbackIsoOpPushout g₁.op g₂.op).inv ≫ pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) ≫
      pullback.fst f₁.op f₂.op

case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ ((pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op ≫ (pullbackIsoOpPushout f₁.op f₂.op).inv) ≫ pullback.snd f₁.op f₂.op =
    ((pullbackIsoOpPushout g₁.op g₂.op).inv ≫ pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) ≫
      pullback.snd f₁.op f₂.op
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ (f₁ ⊗ₘ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ = ((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂

pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂) = tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂)

Tactic:
<;>

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ (f₁ ⊗ₘ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ = ((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂

case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂) = tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = ((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂

pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂) = tensorμ Z₁ Z₂ X₁ X₂ ≫ ((𝟙 Z₁ ⊗ₘ f₁) ⊗ₘ 𝟙 Z₂ ⊗ₘ f₂)

Tactic:
<;>

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = ((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂

case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂) = tensorμ Z₁ Z₂ X₁ X₂ ≫ ((𝟙 Z₁ ⊗ₘ f₁) ⊗ₘ 𝟙 Z₂ ⊗ₘ f₂)
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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    G.obj X ◁ (εIso F ≪≫ i.app (𝟙_ C)).hom ≫
      ((i.symm.app X ⊗ᵢ i.symm.app (𝟙_ C)) ≪≫ μIso F X (𝟙_ C) ≪≫ i.app (X ⊗ 𝟙_ C)).hom ≫ G.map (ρ_ X).hom

Tactic:
by
    simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Category.id_comp,
      Iso.hom_inv_id_app, Category.comp_id]
    rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]
    simp

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        F.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj Y ⊗ F.obj X) (F.obj Z)).inv ≫
            (F.obj W ◁ μ F Y X) ▷ F.obj Z ≫
              μ F W (Y ⊗ X) ▷ F.obj Z ≫
                F.map (α_ W Y X).inv ▷ F.obj Z ≫ μ F ((W ⊗ Y) ⊗ X) Z ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)

Tactic:
μ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        F.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj Y ⊗ F.obj X) (F.obj Z)).inv ≫
            (F.obj W ◁ μ F Y X) ▷ F.obj Z ≫
              μ F W (Y ⊗ X) ▷ F.obj Z ≫ μ F (W ⊗ Y ⊗ X) Z ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).inv ≫
        (α_ (F.obj W ⊗ F.obj X) (F.obj Y) (F.obj Z)).inv ≫
          μ F W X ▷ F.obj Y ▷ F.obj Z ≫
            μ F (W ⊗ X) Y ▷ F.obj Z ≫
              F.map (α_ W X Y).hom ▷ F.obj Z ≫
                F.map (W ◁ (β_ X Y).hom) ▷ F.obj Z ≫
                  μ F (W ⊗ Y ⊗ X) Z ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)

Tactic:
μ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).inv ≫
        (α_ (F.obj W ⊗ F.obj X) (F.obj Y) (F.obj Z)).inv ≫
          μ F W X ▷ F.obj Y ▷ F.obj Z ≫
            μ F (W ⊗ X) Y ▷ F.obj Z ≫
              F.map (α_ W X Y).hom ▷ F.obj Z ≫
                μ F (W ⊗ X ⊗ Y) Z ≫
                  F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).inv ≫
        (α_ (F.obj W ⊗ F.obj X) (F.obj Y) (F.obj Z)).inv ≫
          μ F W X ▷ F.obj Y ▷ F.obj Z ≫
            μ F (W ⊗ X) Y ▷ F.obj Z ≫
              F.map (α_ W X Y).hom ▷ F.obj Z ≫
                μ F (W ⊗ X ⊗ Y) Z ≫
                  F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)

Tactic:
μ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).inv ≫
        (α_ (F.obj W ⊗ F.obj X) (F.obj Y) (F.obj Z)).inv ≫
          μ F W X ▷ F.obj Y ▷ F.obj Z ≫
            μ F (W ⊗ X) Y ▷ F.obj Z ≫
              μ F ((W ⊗ X) ⊗ Y) Z ≫
                F.map ((α_ W X Y).hom ▷ Z) ≫
                  F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
a✝ b✝ : M
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) (FreeAlgebra.ι R (a✝ + b✝))
    (FreeAlgebra.ι R a✝ + FreeAlgebra.ι R b✝)

pp: case smul
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
r✝ : R
a✝ : M
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) (FreeAlgebra.ι R (r✝ • a✝))
    ((algebraMap R (FreeAlgebra R M)) r✝ * FreeAlgebra.ι R a✝)

Tactic:
<;>

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
a✝ b✝ : M
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) (FreeAlgebra.ι R (a✝ + b✝))
    (FreeAlgebra.ι R a✝ + FreeAlgebra.ι R b✝)

case smul
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
r✝ : R
a✝ : M
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) (FreeAlgebra.ι R (r✝ • a✝))
    ((algebraMap R (FreeAlgebra R M)) r✝ * FreeAlgebra.ι R a✝)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).fst = (inl ↑x✝ + 1).fst

pp: case h2
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).snd = (inl ↑x✝ + 1).snd

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).fst = (inl ↑x✝ + 1).fst

case h2
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).snd = (inl ↑x✝ + 1).snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst 1

pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd 1

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst 1

case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd 1