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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁
          (adj.unit.app (Y ⊗ Z) ≫
            G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z)) ≫ adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁
          (adj.unit.app (Y ⊗ Z) ≫
            G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z))) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
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'
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ μ e.functor X Y =
    e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y) ≫ (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y))

Tactic:
map_comp,

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'
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ μ e.functor X Y =
    e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) ≫
        e.functor.map (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y)
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
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ (f₁ ⊗ₘ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ = tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂)

Tactic:
convert! tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1

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

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom (s.ι.app j))

Tactic:
rw [← hm]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom ((colimitCocone F).ι.app j ≫ m))
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') ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) (AddEquiv.ulift.symm a)) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0

Tactic:
Quot.map_ι

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) (AddEquiv.ulift.symm a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0
Module: Mathlib.CategoryTheory.Adjunction.Mates

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

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X✝ : D
⊢ G.map (adj₁.unit.app (R₁.obj X✝) ≫ R₁.map (adj₁.counit.app X✝)) ≫ β.natTrans.app X✝ = β.natTrans.app X✝
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
inst✝ : Small.{w, max w u} (Quot F)
x✝³ x✝² : J
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑(F.obj x✝³)
⊢ Shrink.addEquiv.symm ((Quot.ι F x✝²) ((Hom.hom (F.map x✝¹)) x✝)) = Shrink.addEquiv.symm ((Quot.ι F x✝³) x✝)

Tactic:
Quot.map_ι

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max w u} (Quot F)
x✝³ x✝² : J
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑(F.obj x✝³)
⊢ Shrink.addEquiv.symm ((Quot.ι F x✝³) x✝) = Shrink.addEquiv.symm ((Quot.ι F x✝³) x✝)
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 ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫
      G₂.map (R₂.map (α.natTrans.app (R₁.obj b))) ≫
        G₂.map (R₂.map (H₁.map (adj₁.counit.app b))) ≫
          adj₃.unit.app (G₂.obj (R₂.obj (H₁.obj b))) ≫
            R₃.map (β.natTrans.app (R₂.obj (H₁.obj b))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
slice_rhs 1 4 => rw [← assoc, ← 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 ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map
            (L₃.map
              ((G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b)))) ≫
                G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
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 : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (⇑(((fun f ↦ (ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯) ((fun F ↦ F.toLinearMap ∘ₗ ι R) F)).comp
            (RingCon.mkₐ R (ringCon R M))) ∘
        FreeAlgebra.ι R)
      x =
    (⇑(F.comp (RingCon.mkₐ R (ringCon R M))) ∘ FreeAlgebra.ι R) x

Tactic:
rw [ι]
            simp
            rfl

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:
dsimp; rw [smul_zero, add_zero]

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
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)

Tactic:
rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]

Goal state after:
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₂
α : L₂ ⟶ L₁
β : L₁ ⟶ L₂
βα : β ≫ α = 𝟙 L₁
⊢ (conjugateEquiv adj₁ adj₁) (𝟙 L₁) = 𝟙 R₁

Tactic:
conjugateEquiv_id

Goal state after:
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₂
α : L₂ ⟶ L₁
β : L₁ ⟶ L₂
βα : β ≫ α = 𝟙 L₁
⊢ 𝟙 R₁ = 𝟙 R₁
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⁻¹))

Tactic:
simp [hb0]

Goal state after:
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))
      ((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) =
    (TensorProduct.map (inl R 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) ∘ₗ
            inl R A B) ∘ₗ
        comul)
      x

Tactic:
coprod_inl,

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) (inl R A B) ∘ₗ comul) x) =
    (TensorProduct.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) ∘ₗ comul) x
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := ⋯
this : Module R A := ⋯
x✝ : A
⊢ (TensorProduct.map (↑(linearEquiv R e)) LinearMap.id) ((LinearMap.lTensor A counit ∘ₗ comul) x✝) =
    (TensorProduct.map (↑(linearEquiv R e)) LinearMap.id) (((TensorProduct.mk R A R).flip 1) x✝)

Tactic:
simpa +instances [coalgebraStruct, LinearMap.comp_assoc, TensorProduct.map_map,
        LinearMap.lTensor] using! Coalgebra.lTensor_counit_comul _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat R
r : R
x : ↑((restrictScalars f).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj M)) (r • x) = r • (AddEquiv.refl ↑((restrictScalars f).obj M)) x

Tactic:
subst hf; rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y : ModuleCat S
s : S
y : ↑Y
t : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
          { toFun := fun s_1 ↦ s_1 • s • y, map_add' := ⋯, map_smul' := ⋯ }))
      t =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((RingHom.id S) s •
          (CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }))
      t

Tactic:
by
        simp [mul_smul]

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✝² : EquivLike F α β
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ f a) ≤ b

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (EquivLike.inv f c ⊓ a) ≤ f b ↔ EquivLike.inv f (c ⊓ f a) ≤ b
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✝² : EquivLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (f b ⊔ c)

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f a ≤ f (b ⊔ EquivLike.inv f c) ↔ a ≤ EquivLike.inv f (f b ⊔ c)
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✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ f a) ≤ b

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (EquivLike.inv f c ⊓ a) ≤ f b ↔ EquivLike.inv f (c ⊓ f a) ≤ b
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✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (f b ⊔ c)

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f a ≤ f (b ⊔ EquivLike.inv f c) ↔ a ≤ EquivLike.inv f (f b ⊔ c)
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
A : Comon C
f : A ⟶ trivial C
⊢ f.hom ≫ 𝟙 (𝟙_ C) = ε

Tactic:
← trivial_comon_counit,

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
A : Comon C
f : A ⟶ trivial C
⊢ f.hom ≫ ε = ε
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
H : ∀ (p : R), Prime p → emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
p : R
hp : Prime p
this : emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
⊢ emultiplicity p a ≤ emultiplicity p b

Tactic:
rwa [emultiplicity_pow hp, emultiplicity_pow hp,
    ENat.mul_le_mul_left_iff (by exact_mod_cast hn) (ENat.natCast_ne_top _)] at this

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = n - ↑m.natAbs

Tactic:
Int.ofNat_natAbs_of_nonpos hm.le,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = n - -m
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ ↑s • mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x

Tactic:
← algebraMap_smul A

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ (algebraMap R A) ↑s • mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x
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 : Y ⟶ Z
inst✝ : IsMonHom f
⊢ μ ≫ X ◁ f = (X ◁ f ⊗ₘ X ◁ f) ≫ μ

Tactic:
by simpa using ((inferInstance : IsMonHom (𝟙 X ⊗ₘ f))).mul_hom

Goal state after:
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
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ («μ» F X X ≫ F.map μ) ▷ F.obj X ≫ «μ» F X X ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ («μ» F X X ≫ F.map μ) ≫ «μ» F X X ≫ F.map μ

Tactic:
simp_rw [comp_whiskerRight, Category.assoc, μ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, Category.assoc, μ_natural_right_assoc]

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
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ «μ» F X X ▷ F.obj X ≫ «μ» F (X ⊗ X) X ≫ F.map (μ ▷ X) ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ «μ» F X X ≫ «μ» F X (X ⊗ X) ≫ F.map (X ◁ μ) ≫ F.map μ
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • v • a.1 = (↑u * ↑a.2) • b.1

Tactic:
← h₁,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • u • b.1 = (↑u * ↑a.2) • b.1
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • u • b.1 = ↑a.2 • ↑u • b.1

Tactic:
Submonoid.smul_def

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • ↑u • b.1 = ↑a.2 • ↑u • b.1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h✝ : HasLimit (cospan f g)
P : C
fst : P ⟶ X
snd : P ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimit (cospan f g) F

Tactic:
rwa [h.preservesLimit_cospan_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X ≫ retraction (T.η.app X))

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X) ≫ T.map (retraction (T.η.app X))
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X) ≫ T.ε.app X)

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.map (T.ε.app X)