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

Goal state before:
pp: case e'_2
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
a : R
f₀ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
j : ι
⊢ (update f i (a • f₀) j) (x j) = update (fun j ↦ (f j) (x j)) i (a • f₀ (x i)) j

Tactic:
exact Function.apply_update c f i (a • f₀) j

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: 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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ ∑ s with 2 ≤ #s, f (s.piecewise h x) - ∑ s with 2 ≤ #s, f (s.piecewise h' x) =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
sum_sub_distrib

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: 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
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))

Tactic:
simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp]

Goal state after:
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 G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ G.mapCone (liftLimit ((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm t)) ≅ c

Tactic:
by
        refine (IsLimit.mapConeEquiv h ?_).uniqueUpToIso t
        apply IsLimit.ofIsoLimit _ (liftedLimitMapsToOriginal _).symm
        apply (IsLimit.postcomposeInvEquiv _ _).symm t

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type u_1
inst✝ : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)} (F ⋙ uliftFunctor.{v, u_1})

Tactic:
rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftCoyonedaCoreprXIso.symm]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type u_1
inst✝ : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
    (uliftCoyoneda.{u_1, v, u}.obj (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesColimit G (F ⋙ (evaluation K C).obj k)
c : Cocone G
hc : IsColimit c
X : K
this : PreservesColimit G (F ⋙ (evaluation K C).obj X)
⊢ IsColimit (((evaluation K C).obj X).mapCocone (F.mapCocone c))

Tactic:
change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesColimit G (F ⋙ (evaluation K C).obj k)
c : Cocone G
hc : IsColimit c
X : K
this : PreservesColimit G (F ⋙ (evaluation K C).obj X)
⊢ IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommMonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommMonCat).sections
⊢ CreatesLimit F (forget CommMonCat)

Tactic:
by
  set e : forget CommMonCat.{u} ≅ forget₂ CommMonCat.{u} MonCat.{u} ⋙ forget MonCat.{u} :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _) (fun _ ↦ rfl)
  exact createsLimitOfNatIso e.symm

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 ≫ α.app (𝟙_ C) = ε G

Tactic:
IsMonoidal.unit

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 β
⊢ ε G = ε G
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 ≫ β.app (𝟙_ C) = ε K

Tactic:
IsMonoidal.unit

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 β
⊢ ε K = ε K
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
⊢ F.CoreMonoidal

Tactic:
by
  letI := induced F fData
  exact
    { εIso := fData.εIso
      μIso := fData.μIso
      μIso_hom_natural_left := fun _ ↦ by simp [fData.whiskerRight_eq]
      μIso_hom_natural_right := fun _ ↦ by simp [fData.whiskerLeft_eq]
      associativity := fun _ _ _ ↦ by simp [fData.associator_eq]
      left_unitality := fun _ ↦ by simp [fData.leftUnitor_eq]
      right_unitality := fun _ ↦ by simp [fData.rightUnitor_eq] }

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
by
  rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, id_comp]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ?m.108)

Tactic:
apply PullbackCone.isLimitOfFlip
        apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
        exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)

Tactic:
by
  simp [IsMonoidal.leftAdjoint_μ (adj := adj), ← adj.unit_naturality_assoc,
    ← Functor.map_comp, ← δ_natural_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget₂ C D ⋙ forget D).PreservesMonomorphisms

Tactic:
simp only [HasForget₂.forget_comp]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget₂ C D ⋙ forget D).PreservesEpimorphisms

Tactic:
simp only [HasForget₂.forget_comp]
    infer_instance

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✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj (X ⊗ Y) ⊗ F.obj Z)).symm
          ((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
        (adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj (Y ⊗ Z))).symm
            ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
          F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
by
    rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm,
      Equiv.apply_symm_apply, Equiv.apply_symm_apply, assoc, assoc]
    conv_lhs =>
      rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_assoc]
      dsimp
      rw [← comp_whiskerRight_assoc]
    conv_rhs =>
      rw [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_assoc]
      dsimp
      rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_assoc]
    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 (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:
associator_inv_naturality_middle_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.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom) ▷ F.obj Z ≫
            (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.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: 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
⊢ Subalgebra.map ((lift R) f) ⊤ = Algebra.adjoin R (Set.range ⇑f)

Tactic:
← adjoin_range_ι,

Goal state after:
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
⊢ Subalgebra.map ((lift R) f) (Algebra.adjoin R (Set.range ⇑(ι R))) = Algebra.adjoin R (Set.range ⇑f)
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (α.natTrans.app (R₁.obj (R₃.obj c))) ≫
        R₂.map (H.map (adj₁.counit.app (R₃.obj c))) ≫
          R₂.map (adj₄.unit.app (H.obj (R₃.obj c))) ≫
            R₂.map (R₄.map (β.natTrans.app (R₃.obj c))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Tactic:
slice_rhs 2 4 =>
    rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      (R₂.map
            (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
              R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
by
  suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa using this
  infer_instance

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2.inr.inl
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb0 : b.fst = 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

pp: case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
· simp [hb0]

Goal state after:
case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
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✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ TensorProduct.map ↑e.toLinearEquiv.symm ↑e.toLinearEquiv.symm ∘ₗ comul = comul ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
change (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
        = comul ∘ₗ (e : A ≃ₗ[R] B).symm

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ ↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv).symm ∘ₗ comul = comul ∘ₗ ↑e.toLinearEquiv.symm
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
⊢ lTensor R (inl R A B) ∘ₗ rTensor A counit ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B

Tactic:
rTensor_counit_comp_comul,

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
⊢ lTensor R (inl R A B) ∘ₗ (TensorProduct.mk R R A) 1 = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B
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
⊢ lTensor R (inr R A B) ∘ₗ rTensor B counit ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
rTensor_counit_comp_comul,

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
⊢ lTensor R (inr R A B) ∘ₗ (TensorProduct.mk R R B) 1 = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ lTensor R (lsingle i✝) ∘ₗ rTensor (A i✝) counit ∘ₗ comul = (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1 ∘ₗ lsingle i✝

Tactic:
rTensor_counit_comp_comul,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ lTensor R (lsingle i✝) ∘ₗ (TensorProduct.mk R R (A i✝)) 1 = (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1 ∘ₗ lsingle i✝