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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (ρ_ (F.obj X)).hom ≫ (ρ_ (F.obj X)).inv =
    (F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom) ≫ (ρ_ (F.obj X)).inv

Tactic:
Iso.hom_inv_id,

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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (F.obj X ⊗ 𝟙_ D) = (F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom) ≫ (ρ_ (F.obj X)).inv
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
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ F.map x✝¹ ▷ F.obj x✝ = F.map x✝¹ ▷ F.obj x✝ ≫ (h.μIso Y✝ x✝).hom ≫ (h.μIso Y✝ x✝).inv

Tactic:
Iso.hom_inv_id,

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
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ F.map x✝¹ ▷ F.obj x✝ = F.map x✝¹ ▷ F.obj x✝ ≫ 𝟙 (F.obj Y✝ ⊗ F.obj 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
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ F.obj x✝¹ ◁ F.map x✝ = F.obj x✝¹ ◁ F.map x✝ ≫ (h.μIso x✝¹ Y✝).hom ≫ (h.μIso x✝¹ Y✝).inv

Tactic:
Iso.hom_inv_id,

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
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ F.obj x✝¹ ◁ F.map x✝ = F.obj x✝¹ ◁ F.map x✝ ≫ 𝟙 (F.obj x✝¹ ⊗ F.obj Y✝)
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
h : F.CoreMonoidal
x✝ : C
⊢ (λ_ (F.obj x✝)).hom ≫ (λ_ (F.obj x✝)).inv =
    (λ_ (F.obj x✝)).hom ≫ F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj x✝

Tactic:
Iso.hom_inv_id,

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
h : F.CoreMonoidal
x✝ : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj x✝) = (λ_ (F.obj x✝)).hom ≫ F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj 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
h : F.CoreMonoidal
x✝ : C
⊢ (ρ_ (F.obj x✝)).hom ≫ (ρ_ (F.obj x✝)).inv =
    (ρ_ (F.obj x✝)).hom ≫ F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv

Tactic:
Iso.hom_inv_id,

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
h : F.CoreMonoidal
x✝ : C
⊢ 𝟙 (F.obj x✝ ⊗ 𝟙_ D) = (ρ_ (F.obj x✝)).hom ≫ F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv
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 : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)

Tactic:
by
    apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun
    apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm
    apply PushoutCocone.isColimitOfFlip
    apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
    · -- Need to unfold these to allow the `PreservesColimit` instance to be found.
      dsimp only [span_map_fst, span_map_snd]
      exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)

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
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ 𝟙 ((Z ⊗ Y) ⊗ X) =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv
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
inst✝ : HasPullback f g
⊢ (pushout.inr f.unop g.unop ≫ (pullbackIsoOpPushout f g).hom.unop).op = (pullback.snd f g).unop.op

Tactic:
by simp [← pullbackIsoOpPushout_inv_snd]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ HasPullback f.unop g.unop

Tactic:
rwa [hasPullback_unop_iff_hasPushout]

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
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ 𝟙 (X ⊗ 𝟙_ C) = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom
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 : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ 𝟙 (𝟙_ C ⊗ X) = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ≫ f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ≫ (β_ Y₂ V₁).hom ⊗ₘ g₂ ≫ 𝟙 V₂

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

Tactic:
comp_id g₂,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ≫ f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ≫ (β_ Y₂ V₁).hom ⊗ₘ g₂

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C ≫ X₁ ◁ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ C

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (α_ X₁ X₂ (𝟙_ C)).hom

Tactic:
rw [← whiskerLeft_comp, ← comp_whiskerRight,
    rightUnitor_inv_braiding]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| X₁ ◁ (λ_ X₂).inv ▷ 𝟙_ C

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (α_ X₁ X₂ (𝟙_ C)).hom
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x

Tactic:
rcases x with ⟨⟩

Goal state after:
case mk
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.rTensor B counit ∘ₗ comul = (TensorProduct.mk R R B) 1

Tactic:
simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]
    ext x
    simp [← (ℛ R _).eq]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.lTensor B counit ∘ₗ comul = (TensorProduct.mk R B R).flip 1

Tactic:
simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]
    ext x
    simp [← (ℛ R _).eq]

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : CoalgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CoalgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (CoalgCat.{v} R)).map f)

Goal state after:
R : Type u
inst✝ : CommRing R
X Y : CoalgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CoalgCat R)).map f)
i : (forget (CoalgCat R)).obj X ≅ (forget (CoalgCat R)).obj Y := asIso ((forget (CoalgCat R)).map f)
⊢ IsIso f
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
      Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄) ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
          (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).inv ≫ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
rw [extendScalars_assoc_assoc]
  simp only [Iso.inv_hom_id_assoc, ← Functor.whiskerLeft_comp_assoc, Iso.hom_inv_id,
    Functor.whiskerLeft_id', Category.id_comp]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⇨ b) = f' a ⇨ f' b

Tactic:
simpa only [h] using map_himp f

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⇨ b) = f' a ⇨ f' b

Tactic:
simpa only [h] using map_himp f

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ ε ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
← LinearMap.lTensor_comp_rTensor,

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ (LinearMap.lTensor R f ∘ₗ LinearMap.rTensor M ε) ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S : Under R
x✝ : ↑R
⊢ (Hom.hom
        ((((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).obj S).hom ≫
          ofHom
            (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
              (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯)))
      x✝ =
    (Hom.hom ((𝟭 (Under R)).obj S).hom) x✝

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ Hom.hom
      (Under.Hom.right
        (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
          Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
            ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
            ⋯ ≫
          (𝟭 (Under R)).map f))

Tactic:
apply MonoidAlgebra.ringHom_ext <;>
        intro

Goal state after:
case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single 1 r✝)

case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
m✝ : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single m✝ 1)
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
K L : CoalgCat R
⊢ CoalgebraStruct.comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
ofComonObjCoalgebraStruct_comul

Goal state after:
R : Type u
inst✝ : CommRing R
K L : CoalgCat R
⊢ ModuleCat.Hom.hom Δ =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
G : CommMonCat
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r✝)

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h_of
R : CommRingCat
G : CommMonCat
m✝ : ↑G
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m✝ 1)

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S : Under R
x✝ : ↑((forget₂ CommRingCat CommMonCat).obj S.right)
⊢ (CommMonCat.Hom.hom
        (CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑S.right) ≫
          CommMonCat.ofHom ↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id ↑S.right) ⋯)))
      x✝ =
    (CommMonCat.Hom.hom (𝟙 ((forget₂ CommRingCat CommMonCat).obj S.right))) x✝

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
ofComonObjCoalgebraStruct_comul

Goal state after:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom Δ = CoalgebraStruct.comul