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

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

Tactic:
simp [shrinkYoneda]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
⊢ LiftsToLimit F (forget₂ CommGrpCat GrpCat) c hc

Tactic:
have : HasLimit _ := ⟨_, hc⟩
    have : Small.{u} (F ⋙ forget CommGrpCat).sections :=
      Concrete.small_sections_of_hasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
    have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙
      forget MonCat).sections := this
    have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections := this
    exact
      { liftedCone :=
          { pt := CommGrpCat.of (Types.Small.limitCone.{v, u} (F ⋙ forget CommGrpCat)).pt
            π :=
              { app j := ofHom <| MonCat.limitπMonoidHom
                  (F ⋙ forget₂ CommGrpCat GrpCat.{u} ⋙ forget₂ GrpCat MonCat.{u}) j
                naturality i j h := hom_ext <| congr_arg MonCat.Hom.hom <|
                  (MonCat.HasLimits.limitCone _).π.naturality h } }
        validLift := by apply IsLimit.uniqueUpToIso (GrpCat.limitConeIsLimit _) hc
        makesLimit :=
          IsLimit.ofFaithful (forget₂ _ GrpCat.{u} ⋙ forget₂ _ MonCat.{u})
            (by apply MonCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }

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

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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ (ε (F.prod' H)).2 ≫ ((prod' α β).app (𝟙_ C)).2 = (ε (G.prod' K)).2

Tactic:
prod'_ε_snd,

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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ ε H ≫ ((prod' α β).app (𝟙_ C)).2 = (ε (G.prod' K)).2
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ ε H ≫ ((prod' α β).app (𝟙_ C)).2 = (ε (G.prod' K)).2

Tactic:
prod'_ε_snd,

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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ ε H ≫ ((prod' α β).app (𝟙_ C)).2 = ε K
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η η' : f ⟶ g
θ θ' : h ⟶ i
ι : f ⊗ h ⟶ g ⊗ i
e_η : η = η'
e_θ : θ = θ'
e_ι : η' ⊗ₘ θ' = ι
⊢ η ⊗ₘ θ = ι

Tactic:
by
  simp [e_η, e_θ, e_ι]

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
h : F.CoreMonoidal
inst✝² : F.OplaxMonoidal
inst✝¹ : IsIso (η F)
inst✝ : ∀ (X Y : C), IsIso (δ F X Y)
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ (asIso (η F)).symm.hom ≫ (asIso (δ F X (𝟙_ C))).symm.hom ≫ F.map (ρ_ X).hom

Tactic:
simp [← cancel_epi (ρ_ (F.obj X)).inv]

Goal state after:
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ᵒᵖ
inst✝ : HasColimit F
j : J
⊢ (limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop

Tactic:
simp [limitUnopIsoUnopColimit]

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

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

Tactic:
refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
  rw [← hasColimitsOfShape_opposite_opposite_iff]
  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
this : F.map (G.map f) ▷ F.obj (G.obj X') ≫ ?m.200 = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.237
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')

Tactic:
by rw [this]

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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
this : F.obj (G.obj X) ◁ F.map (G.map g) ≫ ?m.305 = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.342
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)

Tactic:
by rw [this]

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 ⟶ Z
g : Y ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingSpan} (f_1 : X_1 ⟶ Y_1),
    (span f.op g.op).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((span f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((span f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
        (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map f_1

Tactic:
rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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 ⟶ Z
g : Y ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingSpan} (f_1 : X_1 ⟶ Y_1),
    (span f.unop g.unop).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((span f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((span f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom ≫
        (walkingCospanOpEquiv.inverse ⋙ (cospan f g).leftOp).map f_1

Tactic:
rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ Surjective ⇑(ConcreteCategory.hom (𝟙 X))

Tactic:
convert! surjective_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ ⇑(ConcreteCategory.hom (𝟙 X)) = id
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
⊢ ∀ {X_1 Y_1 : WalkingCospan} (f_1 : X_1 ⟶ Y_1),
    (cospan f.op g.op).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((cospan f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((cospan f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
        (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map f_1

Tactic:
rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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
⊢ ∀ {X_1 Y_1 : WalkingCospan} (f_1 : X_1 ⟶ Y_1),
    (cospan f.unop g.unop).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((cospan f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((cospan f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
        (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map f_1

Tactic:
rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
⊢ μ G X Y ≫ G.map (β_ X Y).hom = (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X

Tactic:
have (X Y : C) : μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by
      simp [NatTrans.IsMonoidal.tensor X Y, tensorHom_comp_tensorHom_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
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ μ G X Y ≫ G.map (β_ X Y).hom = (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X
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₁ X₂ Y₁ Y₂ : C
⊢ tensorδ X₁ X₂ Y₁ Y₂ ≫ tensorμ X₁ X₂ Y₁ Y₂ = 𝟙 ((X₁ ⊗ Y₁) ⊗ X₂ ⊗ Y₂)

Tactic:
simp only [tensorδ, ← whiskerLeft_comp_assoc, tensorμ, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id_assoc, inv_hom_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp,
    Iso.hom_inv_id]

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ ((Quot.ι (F ⋙ uliftFunctor) j').comp AddEquiv.ulift.symm.toAddMonoidHom) ((ConcreteCategory.hom (F.map u)) a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0

Tactic:
change Quot.ι (F ⋙ uliftFunctor) j' ((F ⋙ uliftFunctor).map u (AddEquiv.ulift.symm a)) - _ = _

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ (Quot.ι (F ⋙ uliftFunctor) j') ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) (AddEquiv.ulift.symm a)) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.snd = (inl r⁻¹).snd

Tactic:
snd_inv,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ -((inl r).fst⁻¹ •> (inl r).snd <• (inl r).fst⁻¹) = (inl r⁻¹).snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.snd = snd 0

Tactic:
snd_inv,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -((inr m).fst⁻¹ •> (inr m).snd <• (inr m).fst⁻¹) = snd 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ ↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ
      rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) =
    lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
      (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)

Tactic:
ext x : 2

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : A
⊢ ((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ
          rTensor (A × B)
              ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        inl R A B)
      x =
    ((lTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        inl R A B)
      x

case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ ((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ
          rTensor (A × B)
              ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        inr R A B)
      x =
    ((lTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        inr R A B)
      x
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      (((rTensor (A × B)
              ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
          comul)
        x) =
    ((lTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
        comul)
      x

Tactic:
rTensor_comp_map,

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) ∘ₗ
              inl R A B)
            (inl R A B) ∘ₗ
          comul)
        x) =
    ((lTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
        comul)
      x
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
L₁ L₂ : B ⥤ C
R₁ R₂ : C ⥤ B
L : A ⥤ B
R : B ⥤ A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
⊢ ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ)).app X =
    (whiskerRight ((conjugateEquiv adj₁ adj₂) τ) R).app X

Tactic:
have h₁ := congr_map (R₂ ⋙ R) (τ.naturality (adj.counit.app (R₁.obj X)))

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
L₁ L₂ : B ⥤ C
R₁ R₂ : C ⥤ B
L : A ⥤ B
R : B ⥤ A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  (R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app ((𝟭 B).obj (R₁.obj X))) =
    (R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X)))
⊢ ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ)).app X =
    (whiskerRight ((conjugateEquiv adj₁ adj₂) τ) R).app X
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      (((rTensor (A × B)
              ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
          comul)
        x) =
    ((lTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
        comul)
      x

Tactic:
rTensor_comp_map,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) ∘ₗ
              inr R A B)
            (inr R A B) ∘ₗ
          comul)
        x) =
    ((lTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
        comul)
      x
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] repr.right i) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
map_sum

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ ∑ x ∈ repr.index, (map ↑φ ↑φ) (repr.left x ⊗ₜ[R] repr.right x) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i