-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_mul {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
    map f.toLinearMap (M * N) = map f.toLinearMap M * map f.toLinearMap N :=
  calc
    map f.toLinearMap (M * N) = ⨆ i : M, (N.map (LinearMap.mul R A i)).map f.toLinearMap

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ (range fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) =
    range fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Tactic:
ext S

Result:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ↔
    S ∈ range fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Proof state:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ = S

Tactic:
refine Eq.trans ?_ hy

Result:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ =
    (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y

Proof state:
case h.mpr.intro
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
⊢ S ∈ range fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Tactic:
obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2

Result:
case h.mpr.intro.intro.intro
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : f.toLinearMap y' = ↑y
⊢ S ∈ range fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Proof state:
case h.h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : f y' = ↑y
x✝ : A'
⊢ x✝ ∈ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ ↔
    x✝ ∈ (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y

Tactic:
simp [fy_eq]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N) =
    map₂ (LinearMap.mul R A') (map f.toLinearMap M) (map f.toLinearMap N)

Tactic:
apply congr_arg sSup

Result:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ (range fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) =
    range fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N) = map f.toLinearMap M * map f.toLinearMap N

Tactic:
rw [mul_eq_map₂]

Result:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N) =
    map₂ (LinearMap.mul R A') (map f.toLinearMap M) (map f.toLinearMap N)

Proof state:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ =
    (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y

Tactic:
ext

Result:
case h.h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
x✝ : A'
⊢ x✝ ∈ (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ ↔
    x✝ ∈ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y