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

Tactic:
Iso.inv_hom_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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = F.map (𝟙 (X ⊗ Y ⊗ Z)) ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ PreservesLimit (cospan f g) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (pullbackIsPullback f g)

Goal state after:
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✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) ⋯))
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi f

Tactic:
apply
    PushoutCocone.epi_of_isColimitMkIdId _
      (isColimitOfIsColimitPushoutCoconeMap F _ 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 : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (𝟙_ C) (G.obj X) ≫
      η F ▷ F.obj (G.obj X) ≫ (λ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X ≫ (λ_ X).inv ≫ (λ_ X).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (𝟙_ C) (G.obj X) ≫ η F ▷ F.obj (G.obj X) ≫ (λ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X ≫ 𝟙 X
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : epimorphisms C f
hg : epimorphisms C g
⊢ epimorphisms C (f ≫ g)

Tactic:
by
    rw [epimorphisms.iff] at hf hg ⊢
    apply epi_comp

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 : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ η F ≫ (ρ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X ≫ (ρ_ X).inv ≫ (ρ_ X).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (G.obj X) (𝟙_ C) ≫ F.obj (G.obj X) ◁ η F ≫ (ρ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ 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 X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)

Tactic:
← cancel_epi (δ e.functor _ _),

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 : 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 X Y ≫ μ e.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)
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
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝ ∈
    ↑(DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)).ker

Tactic:
simp only [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (Hom.hom (c.ι.app w✝²)) ((ConcreteCategory.hom (F.map w✝¹)) w✝) - (Hom.hom (c.ι.app w✝³)) w✝ = 0
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
⊢ Quot F →+ ↑c.pt

Tactic:
refine QuotientAddGroup.lift _ (DFinsupp.sumAddHom fun x => (c.ι.app x).hom) ?_
  dsimp
  rw [AddSubgroup.closure_le]
  intro _ ⟨_, _, _, _, eq⟩
  rw [eq]
  simp only [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single]
  change (F.map _ ≫ c.ι.app _) _ - _ = 0
  rw [c.ι.naturality]
  simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id, sub_self]

Goal state after:
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 (𝟙 (R₁.obj X✝)) ≫ β.natTrans.app X✝ = β.natTrans.app X✝

Tactic:
map_id,

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.obj (R₁.obj X✝)) ≫ β.natTrans.app X✝ = β.natTrans.app X✝
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ (tensorAlgebra R).map ({ app := fun M ↦ ModuleCat.ofHom (TensorAlgebra.ι R), naturality := ⋯ }.app x✝) ≫
      { app := fun A ↦ ofHom ((TensorAlgebra.lift R) LinearMap.id), naturality := ⋯ }.app ((tensorAlgebra R).obj x✝) =
    𝟙 ((tensorAlgebra R).obj x✝)

Tactic:
by
    ext : 1
    dsimp
    ext
    simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
x✝¹ x✝ : A
⊢ (((LinearMap.mul R A).compr₂ comul) x✝¹) x✝ = (((LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul) x✝¹) x✝

Tactic:
exact comul_mul

Goal state after:
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
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ map (g ∘ₗ f) = (map g).comp (map f)

Tactic:
by
  apply algHom_ext
  simp only [map_inr, LinearMap.coe_comp, Function.comp_apply, AlgHom.coe_comp, forall_const]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
A : n → Type u_3
inst✝³ : (i : n) → AddCommMonoid (A i)
inst✝² : (i : n) → Module R (A i)
inst✝¹ : (i : n) → Coalgebra R (A i)
inst✝ : ∀ (i : n), IsCocomm R (A i)
⊢ ↑(TensorProduct.comm R ((i : n) → A i) ((i : n) → A i)) ∘ₗ comul = comul

Tactic:
by ext; simp [← map_comm]

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
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x y : S
⊢ g (x * s + y * s) = g (x * s) + g (y * s)

Tactic:
map_add

Goal state after:
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
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x y : S
⊢ g (x * s) + g (y * s) = g (x * s) + g (y * s)
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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹ + 1 ⊗ₜ[R] x✝) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)

Tactic:
map_add

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)
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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
x✝¹ x✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (x✝¹ + x✝) =
    (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹ +
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝

Tactic:
map_add

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
x✝¹ x✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹ +
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝ =
    (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹ +
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih₁ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝
ih₂ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ +
      (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) (x✝ + y✝)

Tactic:
map_add

Goal state after:
case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih₁ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝
ih₂ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ +
      (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝ + (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
a✝¹ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝
a✝ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ +
      (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) (x✝ + y✝)

Tactic:
map_add

Goal state after:
case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
a✝¹ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝
a✝ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ +
      (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝ +
      (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
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
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b

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
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b

Tactic:
· rintro ⟨c, rfl⟩
    rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb
    rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ,
      normalizedFactors_irreducible ha, singleton_add, cons_le_cons_iff, ← ih hb.2]
    apply Dvd.intro _ rfl

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
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hp : Irreducible p
⊢ count p (normalizedFactors x) = n

Tactic:
· exact count_normalizedFactors_eq hp hnorm hle hlt

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y✝ : R
hy✝ : y✝ ∈ closure s
this : (AddMonoidHom.mulLeft x) y✝ ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
y : R
hy : y ∈ s
⊢ (AddMonoidHom.mulLeft x) y ∈ s

Tactic:
exact h_left x y hy

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ limit.π F i ≫
      limit.lift F
          { pt := F.1 i,
            π :=
              { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
                naturality := ⋯ } } ≫
        limit.π F j✝ =
    𝟙 (limit F) ≫ limit.π F j✝

Tactic:
limit.lift_π

Goal state after:
case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ limit.π F i ≫
      { pt := F.1 i,
              π :=
                { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
                  naturality := ⋯ } }.π.app
        j✝ =
    𝟙 (limit F) ≫ limit.π F j✝
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = (algebraMap R B) a₀

Tactic:
hyp2,

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = (algebraMap R B) (x ^ m * a)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
⊢ IsLimit t₁

Tactic:
apply PullbackCone.isLimitAux'
  intro s
  -- Obtain the induced morphism from the universal property of the big square
  obtain ⟨l, hl, hl'⟩ := PullbackCone.IsLimit.lift' H' s.fst (s.snd ≫ f₂)
    (by rw [Category.assoc, ← t₂.condition, reassoc_of% s.condition, ← hi₂])
  refine ⟨l, hl, ?_, ?_⟩
  -- To check that `l` is compatible with the projections, we use the universal property of `t₂`
  · apply PullbackCone.IsLimit.hom_ext H
    · simp [← s.condition, ← hl, ← t₁.condition, ← hi₂]
    · simpa using hl'
  -- Uniqueness of the lift follows from the universal property of the big square
  · intro m hm₁ hm₂
    apply PullbackCone.IsLimit.hom_ext H'
    · simpa [hm₁] using hl.symm
    · simpa [← hm₂] using hl'.symm

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

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x✝ : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x✝ y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x✝ y)
x : R
⊢ (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Goal state after:
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
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
⊢ PreservesColimit (span f g) F

Tactic:
apply preservesColimit_of_preserves_colimit_cocone h.isColimit

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
⊢ IsColimit (F.mapCocone h.cocone)