-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@[ext]
lemma hom_ext {M : ModuleCat R} {N : ModuleCat S}
    {α β : (extendScalars f).obj M ⟶ N}
    (h : ∀ (m : M), α ((1 : S) ⊗ₜ m) = β ((1 : S) ⊗ₜ m)) : α = β

Proof state:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)

Tactic:
have : s ⊗ₜ[R] (m : M) = s • (1 : S) ⊗ₜ[R] m := by
  rw [ExtendScalars.smul_tmul, mul_one]

Result:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this✝ : Algebra R S := f.toAlgebra
s : S
m : ↑M
this : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)

Proof state:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
rw [ExtendScalars.smul_tmul, mul_one]

Result:
no goals

Proof state:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (Hom.hom ((restrictScalars f).map α)) (s ⊗ₜ[R] m) = (Hom.hom ((restrictScalars f).map β)) (s ⊗ₜ[R] m)

Tactic:
change α (s ⊗ₜ m) = β (s ⊗ₜ m)

Result:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)

Proof state:
case a
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ (restrictScalars f).map α = (restrictScalars f).map β

Tactic:
letI := f.toAlgebra

Result:
case a
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ (restrictScalars f).map α = (restrictScalars f).map β

Proof state:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ ∀ (x : ↑((restrictScalars f).obj (of S S))) (y : ↑M),
    (Hom.hom ((restrictScalars f).map α)) (x ⊗ₜ[R] y) = (Hom.hom ((restrictScalars f).map β)) (x ⊗ₜ[R] y)

Tactic:
intro (s : S) m

Result:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (Hom.hom ((restrictScalars f).map α)) (s ⊗ₜ[R] m) = (Hom.hom ((restrictScalars f).map β)) (s ⊗ₜ[R] m)

Proof state:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this✝ : Algebra R S := f.toAlgebra
s : S
m : ↑M
this : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)

Tactic:
simp only [this, map_smul, h]

Result:
no goals

Proof state:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ α = β

Tactic:
apply (restrictScalars f).map_injective

Result:
case a
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ (restrictScalars f).map α = (restrictScalars f).map β

Proof state:
case a.hf
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)

Tactic:
apply TensorProduct.ext'

Result:
case a.hf.H
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ ∀ (x : ↑((restrictScalars f).obj (of S S))) (y : ↑M),
    (Hom.hom ((restrictScalars f).map α)) (x ⊗ₜ[R] y) = (Hom.hom ((restrictScalars f).map β)) (x ⊗ₜ[R] y)

Proof state:
case a
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ (restrictScalars f).map α = (restrictScalars f).map β

Tactic:
ext : 1

Result:
case a.hf
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)