-- 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'
⊢ map f.toLinearMap (M * N) = ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) 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'
⊢ map f.toLinearMap (map₂ (LinearMap.mul R A) M N) = ⨆ 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 : ↥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

Tactic:
simp

Result:
no goals

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'
⊢ (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)

Tactic:
constructor <;> rintro ⟨y, hy⟩

Result:
case h.mp.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 : ↥M
hy : (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ S ∈ range fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

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)

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 : ↥(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
⊢ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ =
    (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y

Tactic:
rw [f.toLinearMap_apply] at fy_eq

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 : ↥(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
⊢ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ =
    (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y

Proof state:
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)

Tactic:
use ⟨y', 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 : ↥(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
⊢ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ = S

Proof state:
case h.mp.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 : ↥M
hy : (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ S ∈ range fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Tactic:
use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩

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, ⋯⟩ = S

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'
⊢ map f.toLinearMap (map₂ (LinearMap.mul R A) M N) = ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Tactic:
apply map_iSup

Result:
no goals

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 : ↥(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
⊢ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ =
    (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap 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 : ↥(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

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 : ↥(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
⊢ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ = 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 : ↥(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
⊢ (fun i => map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ =
    (fun s => map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y