mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

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

Tactic:
map_add,

Goal state after:
case refine_3.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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • x✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝
ih2 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • y✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y✝
⊢ (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • x✝) +
      (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • y✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (x✝ + y✝)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

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

Tactic:
map_add,

Goal state after:
case refine_3.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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • x✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝
ih2 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • y✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y✝
⊢ s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝ +
      s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y✝ =
    s •
      ((lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝ +
        (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) 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 : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) (x✝ + y✝) = (Hom.hom 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
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
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ +
      (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ =
    (Hom.hom g) (x✝ + 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 : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ +
      (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ =
    (Hom.hom 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
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
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ +
      (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ =
    (Hom.hom g) x✝ + (Hom.hom 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
Y : ModuleCat S
s : S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih1 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • x✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝
ih2 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        y✝
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • x✝ + s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (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 : ModuleCat S
s : S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih1 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • x✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝
ih2 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        y✝
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s • x✝) +
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (x✝ + 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 : ModuleCat S
s : S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih1 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • x✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝
ih2 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        y✝
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s • x✝) +
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (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 : ModuleCat S
s : S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih1 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • x✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        x✝
ih2 :
  (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • y✝) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        y✝
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s • x✝) +
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s • y✝) =
    (RingHom.id S) s •
      ((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' := ⋯ })
          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:
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✝ + 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✝ + 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✝ + y✝)
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + a * a * b = a
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ ∃! I, I.IsMaximal

Tactic:
by
  simp [isMaximal_iff]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S) ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ((algebraMap R S) ↑(sec M (f i)).2 * f i) =
    ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Tactic:
← mul_assoc,

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S) ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * (algebraMap R S) ↑(sec M (f i)).2 * f i =
    ↑(∏ i ∈ s, (sec M (f i)).2) • f i
Module: Mathlib.CategoryTheory.Monoidal.Mon

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
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
⊢ F.essImage M.X → F.mapMon.essImage M

Tactic:
by
    rintro ⟨N, ⟨e⟩⟩
    let : MonObj (F.obj N) := .ofIso e.symm
    let : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
    refine ⟨.mk N, ⟨Mon.mkIso e ?_ ?_⟩⟩ <;> simp

Goal state after:
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
⊢ t₁.fst ≫ g₁ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃

Tactic:
by rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr

Tactic:
by rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ inr ≫ fst' = inr ≫ snd'

Tactic:
by simp [← cancel_epi g, ← h.w_assoc, heq]

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
s : ↥S
⊢ mk 0 s = 0

Tactic:
by simp [mk]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
s : ↥S
⊢ mk (-m) s = -mk m s

Tactic:
by simp [mk]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁✝ : PushoutCocone g₂ i₃
i₂✝ : Y₂ ⟶ t₁✝.pt
t₂✝ : PushoutCocone g₁ i₂✝
hi₂✝ : i₂✝ = t₁✝.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr

Tactic:
← reassoc_of% t₁.condition,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁✝ : PushoutCocone g₂ i₃
i₂✝ : Y₂ ⟶ t₁✝.pt
t₂✝ : PushoutCocone g₁ i₂✝
hi₂✝ : i₂✝ = t₁✝.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
⊢ (g₂ ≫ g₁) ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) (x + y) = f (x + y)

Tactic:
map_add,

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) x + (lift (⇑f ∘ of)) y = f (x + y)
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
r : R
m : M
s s' : ↥S
⊢ ∃ u,
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m

Tactic:
obtain ⟨c, hc⟩ := IsLocalization.eq.mp <| IsLocalization.mk'_sec T (IsLocalization.mk' T r s)

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
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ ∃ u,
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ (↑c * (↑s * ↑s') * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    (↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * ↑s') * r) • m

Tactic:
← mul_assoc,

Goal state after:
case h
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
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ (↑c * ↑s * ↑s' * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    (↑c * ↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * ↑s' * r) • m