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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ f ≫ X ◁ inv f = 𝟙 (X ⊗ Y)

Tactic:
← whiskerLeft_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ (f ≫ inv f) = 𝟙 (X ⊗ Y)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z)

Tactic:
← whiskerLeft_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ (inv f ≫ f) = 𝟙 (X ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ X (𝟙_ C) Y).inv ≫ (ρ_ X).hom ▷ Y = X ◁ (λ_ Y).hom

Tactic:
by
  rw [← triangle, Iso.inv_hom_id_assoc]

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

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
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
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (Functor.whiskerRight τ G₁)

Tactic:
rw [← Functor.hcomp_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
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
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (τ ◫ 𝟙 G₁)
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

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

Tactic:
F.map_comp,

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
this : r • f = (r • 𝟙 X) ≫ f
⊢ F.map (r • 𝟙 X) ≫ F.map f = r • F.map f
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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 G : LaxMonoidalFunctor C D
α β : F ⟶ G
h : α.hom = β.hom
⊢ α = β

Tactic:
cases α; cases β; subst h; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ ∃ X' Y' eX eY f', f = eX.inv ≫ F.map f' ≫ eY.hom

Tactic:
obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)

Goal state after:
R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
⊢ ∃ X' Y' eX eY f', f = eX.inv ≫ F.map f' ≫ eY.hom
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
rw [← ih_η]
  apply Iso.ext
  simp [← whisker_exchange_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod' G)).2 = ε G

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

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod' G) X Y).2 = μ G X Y

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

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✝ Y✝ : Arrow (Type u)
φ : X✝ ⟶ Y✝
x : X✝.left
⊢ (hom (Arrow.Hom.right φ)) ↑⟨(TypeCat.Hom.hom X✝.hom) x, ⋯⟩ ∈ Set.range ⇑(TypeCat.Hom.hom Y✝.hom)

Tactic:
exact ⟨φ.left x, congr_hom φ.w x⟩

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

Goal state before:
pp: case mpr
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
⊢ (forget C).PreservesEpimorphisms → MorphismProperty.surjective C = epimorphisms C

Tactic:
· intro
    apply le_antisymm (surjective_le_epimorphisms C)
    intro _ _ f hf
    have : Epi f := hf
    change Function.Surjective ((forget C).map f)
    rw [← epi_iff_surjective]
    infer_instance

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)).hom ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)

Tactic:
braiding_tensorUnit_right

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).hom ≫ (λ_ X).inv) ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)
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✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ G.map x✝¹ ▷ G.obj x✝ ≫ ((i.symm.app Y✝ ⊗ᵢ i.symm.app x✝) ≪≫ μIso F Y✝ x✝ ≪≫ i.app (Y✝ ⊗ x✝)).hom =
    ((i.symm.app X✝ ⊗ᵢ i.symm.app x✝) ≪≫ μIso F X✝ x✝ ≪≫ i.app (X✝ ⊗ x✝)).hom ≫ G.map (x✝¹ ▷ x✝)

Tactic:
by simp [NatTrans.whiskerRight_app_tensor_app_assoc]

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

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

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

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

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

Tactic:
← whiskerLeft_comp,

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

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

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

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom
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:
← whiskerLeft_comp,

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 ≫ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ 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.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
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
⊢ ∀ (X Y : C), μ (𝟭 C) X Y ≫ (𝟭 C).map (β_ X Y).hom = (β_ ((𝟭 C).obj X) ((𝟭 C).obj Y)).hom ≫ μ (𝟭 C) Y X

Tactic:
by
    simp +instances [reverseBraiding, braiding_swap_eq_inv_braiding]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ (inl r * x).snd = (r •> x).snd

Tactic:
by dsimp; rw [smul_zero, add_zero]

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

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.fst •> x.snd

Tactic:
← h,

Goal state after:
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> (x.snd <• x.fst)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ (lift (Algebra.ofId R' (tsze R' N)) ↑⟨inrHom R' N ∘ₗ f, ⋯⟩ ⋯ ⋯ ⋯) (inl r) = inl r

Tactic:
lift_apply_inl,

Goal state after:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ (Algebra.ofId R' (tsze R' N)) r = inl r
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (Hom.hom
        (((extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((𝟭 (ModuleCat R)).obj M))
          ((extendScalarsId R).hom.app M)))
      m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m

Tactic:
extendRestrictScalarsAdj_homEquiv_apply,

Goal state after:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).hom.app M)) (1 ⊗ₜ[R] m) = (Hom.hom ((restrictScalarsId R).inv.app M)) m
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0

Tactic:
rwa [left_eq_add] at this

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 ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ ∘ₗ δ

Tactic:
simp_rw [← LinearMap.lTensor_def, ← coassoc, ← LinearMap.comp_assoc, LinearMap.lTensor_def,
    map_map_comp_assoc_eq]

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'
⊢ (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = ((α ∘ₗ (LinearMap.id ⊗ₘ LinearMap.id) ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ

Tactic:
← symm_comp_map_assoc,

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ LinearMap.id ⊗ₘ δ ∘ₗ δ
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map (Δ ≫ Δ ▷ A ≫ (α_ A A A).hom) ≫ δ F A (A ⊗ A) ≫ F.obj A ◁ δ F A A =
    F.map (Δ ≫ Δ ▷ A) ≫ δ F (A ⊗ A) A ≫ δ F A A ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom

Tactic:
F.map_comp,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ F.map (Δ ▷ A) ≫ F.map (α_ A A A).hom) ≫ δ F A (A ⊗ A) ≫ F.obj A ◁ δ F A A =
    (F.map Δ ≫ F.map (Δ ▷ A)) ≫ δ F (A ⊗ A) A ≫ δ F A A ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ (∃ u, normalizedFactors b = replicate (n + 1) (normalize a) + u) → a ^ (n + 1) ∣ b

Tactic:
rintro ⟨u, hu⟩

Goal state after:
case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
⊢ y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Tactic:
rw [hm]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
inj : Function.Injective ⇑f
h : jacobson R₂ M₂ = ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥

Tactic:
simp_rw [h, comap_bot, (LinearMap.ker_eq_bot.mpr inj).le]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ comap f (jacobson R₂ M₂) = jacobson R M

Tactic:
by
  rw [← map_jacobson_of_ker_le surj le, comap_map_eq_self le]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : jacobson R (M ⧸ N) = ⊥
⊢ jacobson R M ≤ comap N.mkQ ⊥

Tactic:
← h,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : jacobson R (M ⧸ N) = ⊥
⊢ jacobson R M ≤ comap N.mkQ (jacobson R (M ⧸ N))
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), jacobson R (M i) = ⊥
⊢ (pi Set.univ fun x ↦ jacobson R (M x)) ≤ ⊥

Tactic:
by simp_rw [h, pi_univ_bot, le_rfl]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : ↑(jacobson (R ⧸ I)) ⊆ ↑⊥
⊢ ↑(Module.jacobson R (R ⧸ I)) ⊆ ↑⊥

Tactic:
← coe_jacobson_quotient

Goal state after:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : ↑(jacobson (R ⧸ I)) ⊆ ↑⊥
⊢ ↑(jacobson (R ⧸ I)) ⊆ ↑⊥
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : x ∉ I
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
← h,

Goal state after:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : x ∉ I.jacobson
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
this : IsIso prod.fst
⊢ I ⨯ X ≅ I

Tactic:
exact asIso prod.fst

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ (↑R ↑(ofIsLocalizedModule Rₛ S f b).repr) (f (b i)) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr) (b i)

Tactic:
LinearMap.coe_restrictScalars,

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ ↑(ofIsLocalizedModule Rₛ S f b).repr (f (b i)) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr) (b i)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ (tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g) = (tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ)

Tactic:
slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ) = (tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.hom ≫ pullback.fst f g = fst

Tactic:
by
  dsimp [isoPullback, cone, CommSq.cone]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.hom ≫ pullback.snd f g = snd

Tactic:
by
  dsimp [isoPullback, cone, CommSq.cone]
  simp

Goal state after: