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.Monoidal
T : D
⊢ T ◁ η F ≫ T ◁ ε F = 𝟙 (T ⊗ F.obj (𝟙_ C))

Tactic:
by
  rw [← MonoidalCategory.whiskerLeft_comp, η_ε, MonoidalCategory.whiskerLeft_id]

Goal state after:
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 ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (pushoutComparison G f g)

Tactic:
rw [← PreservesPushout.iso_hom]

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 ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (PreservesPushout.iso G f g).hom
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) ⊗ₘ adj.unit.app Z) ≫
    (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
          G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
tensorHom_def'_assoc

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
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    adj.unit.app (X ⊗ Y) ▷ (F ⋙ G).obj Z ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
          G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case refine_1
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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
⊢ ε G = adj.unit.app (𝟙_ C) ≫ G.map (η F)

pp: case refine_2
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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
X Y : D
⊢ μ G X Y = adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))

Tactic:
· simp [homEquiv_counit, leftAdjointOplaxMonoidal_η]

Goal state after:
case refine_2
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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
X Y : D
⊢ μ G X Y = adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.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 : C
⊢ (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv

Tactic:
by
  apply (cancel_mono (λ_ X).hom).1
  simp only [assoc, braiding_leftUnitor, Iso.inv_hom_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
⊢ μ (F ⋙ G) X Y ≫ (F ⋙ G).map (β_ X Y).hom = (β_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y)).hom ≫ μ (F ⋙ G) Y X

Tactic:
dsimp
    slice_lhs 2 3 =>
      rw [← CategoryTheory.Functor.map_comp, braided, CategoryTheory.Functor.map_comp]
    slice_lhs 1 2 => rw [braided]
    simp only [Category.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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    (εIso F ≪≫ i.app (𝟙_ C)).hom ▷ G.obj X ≫
      ((i.symm.app (𝟙_ C) ⊗ᵢ i.symm.app X) ≪≫ μIso F (𝟙_ C) X ≪≫ i.app (𝟙_ C ⊗ X)).hom ≫ G.map (λ_ X).hom

Tactic:
by
    simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Iso.hom_inv_id_app,
      Category.comp_id, Category.id_comp]
    rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]
    simp

Goal state after:
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)
i j : J
f : i ⟶ j
⊢ AddCommGrpCat.ofHom ↑(Hom.hom (F.map f)) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i ≫ AddCommGrpCat.ofHom ↑LinearMap.id

Tactic:
colimit.w (F ⋙ forget₂ _ AddCommGrpCat),

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)
i j : J
f : i ⟶ j
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i ≫ AddCommGrpCat.ofHom ↑LinearMap.id
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
⊢ (∃ a b, c a b ∧ f a = f x ∧ f b = f y) ↔ c x y

Tactic:
refine ⟨fun ⟨a, b, h₁, h₂, h₃⟩ ↦ ?_, by grind⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
x✝ : ∃ a b, c a b ∧ f a = f x ∧ f b = f y
a b : M
h₁ : c a b
h₂ : f a = f x
h₃ : f b = f y
⊢ c x y
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a + ↑↑b) = d.mk' a + d.mk' b

Tactic:
rw [← d.mk'.map_add]; 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
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ (List.map (fun i ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)).length •> x.fst ^ n •> x.snd =
    n.succ •> x.fst ^ n •> x.snd

Tactic:
rw [List.length_map, List.length_range]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ (fun x ↦ ↑x) f = (fun x ↦ ↑x) g

Tactic:
ext; assumption

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
⊢ counit ∘ₗ (↑f).copy f' h = counit

Tactic:
by ext; simp_all

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : CoalgebraStruct R A
f g : R →ₐc[R] A
h : f 1 = g 1
⊢ (fun x ↦ ↑x) f = (fun x ↦ ↑x) g

Tactic:
ext; assumption

Goal state after:
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
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) (x✝ + y✝) = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) (x✝ + y✝)

Tactic:
LinearMap.map_add,

Goal state after:
case add
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ + (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) (x✝ + y✝)
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
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : ↑Y
r : R
s : S
⊢ (ConcreteCategory.hom g) ((r • s) • y) = (RingHom.id R) r • (ConcreteCategory.hom g) (s • y)

Tactic:
rw [← g.hom.map_smul]

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
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : ↑Y
r : R
s : S
⊢ (ConcreteCategory.hom g) ((r • s) • y) = (Hom.hom g) ((RingHom.id R) r • s • y)
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
s : S
g : X ⟶ (restrictScalars f).obj Y
⊢ ∀ (m : R) (x : ↑X),
    { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun x

Tactic:
intro r x

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
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
x : ↑X
⊢ { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun (r • x) =
    (RingHom.id R) r • { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_3
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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
⊢ (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • z) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) z

Tactic:
induction z using TensorProduct.induction_on with

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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((extendScalars f).obj X)
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) z = (Hom.hom g) z

Tactic:
induction z using TensorProduct.induction_on with

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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
⊢ 1 ⊗ₜ[R] (r • x) = (RingHom.id R) r • 1 ⊗ₜ[R] x

Tactic:
by
      let m1 : Module R S := Module.compHom S f
      dsimp; rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul']

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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
r : R
s : S
y : ↑Y
⊢ { toFun := fun y ↦ (r • s) • y, map_add' := ⋯, map_smul' := ⋯ } y =
    ((RingHom.id R) r • { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }) y

Tactic:
change (f r • s) • y = (f r) • s • y

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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
r : R
s : S
y : ↑Y
⊢ (f r • s) • y = f r • s • y
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
s : S
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • z) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        z

Tactic:
induction z using TensorProduct.induction_on with

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
Y : ModuleCat S
y : ↑Y
⊢ (ConcreteCategory.hom (map f)) (1 ⊗ₜ[R] y) = y

Tactic:
change (1 : S) • y = y

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
y : ↑Y
⊢ 1 • y = 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
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✝ + y✝) =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) (x✝ + y✝)

Tactic:
| add _ _ ih₁ ih₂ =>

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✝¹ : 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
z : ↑((restrictScalars f ⋙ extendScalars f).obj Y)
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) z =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) z

Tactic:
induction z using TensorProduct.induction_on with

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

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
      Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄) ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
          (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).inv ≫ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
extendScalars_assoc_assoc

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
      (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv ≫
          ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
            (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).inv ≫
              (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
rw [add_mul, mul_add]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.rightAdjointUniq adj1).hom = 𝟙 G

Tactic:
delta rightAdjointUniq

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ ((conjugateIsoEquiv adj1 adj1) (Iso.refl F)).hom = 𝟙 G
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (x - y) • e = 0 ↔ e * x = e * y

Tactic:
sub_smul,

Goal state after:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ x • e - y • e = 0 ↔ e * x = e * y
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ (α_ M N P).hom = η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 1 3 => rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ (((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫ (α_ M N P).hom = η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
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
⊢ span R (⇑f '' Set.range ⇑b) = map f (span R (Set.range ⇑b))

Tactic:
by rw [Submodule.map_span]

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ mk ((a₁, s₁).1 * (a₂, s₂).1) ((a₂, s₂).2 * (a₁, s₁).2) = mk ((b₁, t₁).1 * (b₂, t₂).1) ((b₂, t₂).2 * (b₁, t₁).2)

Tactic:
simp only [mul_comm s₂ s₁, mul_comm t₂ t₁]

Goal state after:
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ mk (a₁ * a₂) (s₁ * s₂) = mk (b₁ * b₂) (t₁ * t₂)