R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) * f i_1 j_1 *
          ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) =
    f i j
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
⊢ ↑(↑(toLinearMap₂'Aux σ₁ σ₂ f) (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1))
      (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) =
    f i j
rw [Matrix.toLinearMap₂'Aux, mk₂'ₛₗ_apply]
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
this : (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) * f i_1 j_1 *
          ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) =
    f i j
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) * f i_1 j_1 *
          ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) =
    f i j
have : (∑ i', ∑ j', (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j := by
  simp_rw [mul_assoc, ← Finset.mul_sum]
  simp only [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true, mul_comm (f _ _)]
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
this : (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) * f i_1 j_1 *
          ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) =
    ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
this : (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) * f i_1 j_1 *
          ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) =
    f i j
rw [← this]
no goals
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
this : (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) * f i_1 j_1 *
          ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) =
    ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0
exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by simp
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
⊢ (∑ x : n, (if i = x then 1 else 0) * ∑ x_1 : m, f x x_1 * if j = x_1 then 1 else 0) = f i j
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
⊢ (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j
simp_rw [mul_assoc, ← Finset.mul_sum]
no goals
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
⊢ (∑ x : n, (if i = x then 1 else 0) * ∑ x_1 : m, f x x_1 * if j = x_1 then 1 else 0) = f i j
simp only [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true, mul_comm (f _ _)]
no goals
R : Type u_3
R₁ : Type u_5
R₂ : Type u_4
M : Type ?u.83428
M₁ : Type ?u.83431
M₂ : Type ?u.83434
M₁' : Type ?u.83437
M₂' : Type ?u.83440
n : Type u_1
m : Type u_2
n' : Type ?u.83449
m' : Type ?u.83452
ι : Type ?u.83455
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m R
i : n
j : m
this : (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) * f i' j' * if j = j' then 1 else 0) = f i j
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ ↑σ₁ (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1 x✝³) * f x✝³ x✝¹ *
      ↑σ₂ (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1 x✝¹) =
    (if i = x✝³ then 1 else 0) * f x✝³ x✝¹ * if j = x✝¹ then 1 else 0
simp