-- Mathlib/RingTheory/IsTensorProduct.lean
theorem TensorProduct.isBaseChange : IsBaseChange S (TensorProduct.mk R S M 1)

Proof state:
case h.e'_12.h.h
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ (s • 1) ⊗ₜ[R] x = s ⊗ₜ[R] x

Tactic:
congr 1

Result:
case h.e'_12.h.h.e_m
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 = s

Proof state:
case h.e'_12
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)) = mk R S M

Tactic:
ext s x

Result:
case h.e'_12.h.h
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1))) s) x = ((mk R S M) s) x

Proof state:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)))

Tactic:
convert TensorProduct.isTensorProduct R S M using 1

Result:
case h.e'_12
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)) = mk R S M

Proof state:
case h.e'_12.h.h
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 ⊗ₜ[R] x = s ⊗ₜ[R] x

Tactic:
rw [TensorProduct.smul_tmul']

Result:
case h.e'_12.h.h
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ (s • 1) ⊗ₜ[R] x = s ⊗ₜ[R] x

Proof state:
case h.e'_12.h.h
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1))) s) x = ((mk R S M) s) x

Tactic:
change s • (1 : S) ⊗ₜ[R] x = s ⊗ₜ[R] x

Result:
case h.e'_12.h.h
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 ⊗ₜ[R] x = s ⊗ₜ[R] x

Proof state:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ IsBaseChange S ((mk R S M) 1)

Tactic:
delta IsBaseChange

Result:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)))

Proof state:
case h.e'_12.h.h.e_m
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 = s

Tactic:
exact mul_one _

Result:
no goals