-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
theorem map'_comp {M₁ M₂ M₃ : ModuleCat.{v} R} (l₁₂ : M₁ ⟶ M₂) (l₂₃ : M₂ ⟶ M₃) :
    map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃

Proof state:
case hf.h.zero
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₃
⊢ (Hom.hom (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) 0 =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) 0

Tactic:
rfl

Result:
no goals

Proof state:
case hf.h
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 : ↑(obj' f M₁)
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x

Tactic:
dsimp only [map']

Result:
case hf.h
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 : ↑(obj' f M₁)
⊢ (Hom.hom (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) x =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) x

Proof state:
case hf.h
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 : ↑(obj' f M₁)
⊢ (Hom.hom (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) x =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) x

Tactic:
induction x using TensorProduct.induction_on with
| zero => rfl
| tmul => rfl
| add _ _ ihx ihy => rw [map_add, map_add, ihx, ihy]

Result:
no goals

Proof state:
case hf.h.tmul
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✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑M₁
⊢ (Hom.hom (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) (x✝ ⊗ₜ[R] y✝) =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) (x✝ ⊗ₜ[R] y✝)

Tactic:
rfl

Result:
no goals

Proof state:
case hf.h.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 (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) x✝ =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) x✝
ihy :
  (Hom.hom (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) y✝ =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) y✝
⊢ (Hom.hom (↟(LinearMap.baseChange S (Hom.hom (l₁₂ ≫ l₂₃))))) (x✝ + y✝) =
    (Hom.hom (↟(LinearMap.baseChange S (Hom.hom l₁₂)) ≫ ↟(LinearMap.baseChange S (Hom.hom l₂₃)))) (x✝ + y✝)

Tactic:
rw [map_add, map_add, ihx, ihy]

Result:
no goals

Proof state:
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₃
⊢ map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃

Tactic:
ext x

Result:
case hf.h
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 : ↑(obj' f M₁)
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x