case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ↑toMatrix₂' (compl₁₂ B l r) i j = ((↑toMatrix' l)ᵀ ⬝ ↑toMatrix₂' B ⬝ ↑toMatrix' r) i j
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
⊢ ↑toMatrix₂' (compl₁₂ B l r) = (↑toMatrix' l)ᵀ ⬝ ↑toMatrix₂' B ⬝ ↑toMatrix' r
ext (i j)
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ↑(↑B (↑l (↑(stdBasis R (fun x => R) i) 1))) (↑r (↑(stdBasis R (fun x => R) j) 1)) =
    ∑ x : m,
      ∑ x_1 : n,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) x_1 i *
            ↑(↑B (↑(stdBasis R (fun x => R) x_1) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ↑toMatrix₂' (compl₁₂ B l r) i j = ((↑toMatrix' l)ᵀ ⬝ ↑toMatrix₂' B ⬝ ↑toMatrix' r) i j
simp only [LinearMap.toMatrix₂'_apply, LinearMap.compl₁₂_apply, transpose_apply, Matrix.mul_apply,
  LinearMap.toMatrix', LinearEquiv.coe_mk, sum_mul]
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ↑(↑B (↑l (↑(stdBasis R (fun x => R) i) 1))) (↑r (↑(stdBasis R (fun x => R) j) 1)) =
    ∑ y : n,
      ∑ x : m,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) y i *
            ↑(↑B (↑(stdBasis R (fun x => R) y) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ↑(↑B (↑l (↑(stdBasis R (fun x => R) i) 1))) (↑r (↑(stdBasis R (fun x => R) j) 1)) =
    ∑ x : m,
      ∑ x_1 : n,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) x_1 i *
            ↑(↑B (↑(stdBasis R (fun x => R) x_1) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
rw [sum_comm]
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (Finsupp.sum (↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) fun i xi =>
      Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
        xi • yj • ↑(↑B (↑(Pi.basisFun R n) i)) (↑(Pi.basisFun R m) j)) =
    ∑ y : n,
      ∑ x : m,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) y i *
            ↑(↑B (↑(stdBasis R (fun x => R) y) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ↑(↑B (↑l (↑(stdBasis R (fun x => R) i) 1))) (↑r (↑(stdBasis R (fun x => R) j) 1)) =
    ∑ y : n,
      ∑ x : m,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) y i *
            ↑(↑B (↑(stdBasis R (fun x => R) y) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (∑ i_1 : n,
      Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
        ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i_1 •
          yj • ↑(↑B (↑(Pi.basisFun R n) i_1)) (↑(Pi.basisFun R m) j)) =
    ∑ y : n,
      ∑ x : m,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) y i *
            ↑(↑B (↑(stdBasis R (fun x => R) y) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j

case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (i : n),
    (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
        0 • yj • ↑(↑B (↑(Pi.basisFun R n) i)) (↑(Pi.basisFun R m) j)) =
      0
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (Finsupp.sum (↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) fun i xi =>
      Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
        xi • yj • ↑(↑B (↑(Pi.basisFun R n) i)) (↑(Pi.basisFun R m) j)) =
    ∑ y : n,
      ∑ x : m,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) y i *
            ↑(↑B (↑(stdBasis R (fun x => R) y) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
rw [Finsupp.sum_fintype]
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (x : n),
    x ∈ univ →
      (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
          ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) x •
            yj • ↑(↑B (↑(Pi.basisFun R n) x)) (↑(Pi.basisFun R m) j)) =
        ∑ x_1 : m,
          ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) x i *
              ↑(↑B (↑(stdBasis R (fun x => R) x) 1)) (↑(stdBasis R (fun x => R) x_1) 1) *
            ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x_1 j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (∑ i_1 : n,
      Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
        ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i_1 •
          yj • ↑(↑B (↑(Pi.basisFun R n) i_1)) (↑(Pi.basisFun R m) j)) =
    ∑ y : n,
      ∑ x : m,
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) y i *
            ↑(↑B (↑(stdBasis R (fun x => R) y) 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
apply sum_congr rfl
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
      ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
        yj • ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) j)) =
    ∑ x : m,
      ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
          ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) x) 1) *
        ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (x : n),
    x ∈ univ →
      (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
          ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) x •
            yj • ↑(↑B (↑(Pi.basisFun R n) x)) (↑(Pi.basisFun R m) j)) =
        ∑ x_1 : m,
          ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) x i *
              ↑(↑B (↑(stdBasis R (fun x => R) x) 1)) (↑(stdBasis R (fun x => R) x_1) 1) *
            ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x_1 j
rintro i' -
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∑ i_1 : m,
      ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
        ↑(↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) i_1 •
          ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) i_1) =
    ∑ x : m,
      ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
          ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) x) 1) *
        ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j

case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m),
    ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
        0 • ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) i_1) =
      0
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
      ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
        yj • ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) j)) =
    ∑ x : m,
      ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
          ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) x) 1) *
        ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
rw [Finsupp.sum_fintype]
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (x : m),
    x ∈ univ →
      ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
          ↑(↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) x •
            ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) x) =
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
            ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∑ i_1 : m,
      ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
        ↑(↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) i_1 •
          ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) i_1) =
    ∑ x : m,
      ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
          ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) x) 1) *
        ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
apply sum_congr rfl
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
j' : m
⊢ ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
      ↑(↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) j' •
        ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) j') =
    ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
        ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) j') 1) *
      ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) j' j
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (x : m),
    x ∈ univ →
      ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
          ↑(↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) x •
            ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) x) =
        ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
            ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) x) 1) *
          ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) x j
rintro j' -
no goals
case a.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
j' : m
⊢ ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
      ↑(↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) j' •
        ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) j') =
    ↑of (fun i j => ↑l (↑(stdBasis R (fun x => R) j) 1) i) i' i *
        ↑(↑B (↑(stdBasis R (fun x => R) i') 1)) (↑(stdBasis R (fun x => R) j') 1) *
      ↑of (fun i j => ↑r (↑(stdBasis R (fun x => R) j) 1) i) j' j
simp only [smul_eq_mul, Pi.basisFun_repr, mul_assoc, mul_comm, mul_left_comm,
  Pi.basisFun_apply, of_apply]
case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
i✝ : m
⊢ ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
      0 • ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) i✝) =
    0
case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m),
    ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
        0 • ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) i_1) =
      0
intros
no goals
case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
i✝ : m
⊢ ↑(↑(Pi.basisFun R n).repr (↑l (↑(stdBasis R (fun x => R) i) 1))) i' •
      0 • ↑(↑B (↑(Pi.basisFun R n) i')) (↑(Pi.basisFun R m) i✝) =
    0
simp only [zero_smul, smul_zero]
case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i✝ : n
⊢ (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
      0 • yj • ↑(↑B (↑(Pi.basisFun R n) i✝)) (↑(Pi.basisFun R m) j)) =
    0
case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (i : n),
    (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
        0 • yj • ↑(↑B (↑(Pi.basisFun R n) i)) (↑(Pi.basisFun R m) j)) =
      0
intros
no goals
case a.h.h
R : Type u_1
R₁ : Type ?u.654456
R₂ : Type ?u.654459
M : Type ?u.654462
M₁ : Type ?u.654465
M₂ : Type ?u.654468
M₁' : Type ?u.654471
M₂' : Type ?u.654474
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.654489
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i✝ : n
⊢ (Finsupp.sum (↑(Pi.basisFun R m).repr (↑r (↑(stdBasis R (fun x => R) j) 1))) fun j yj =>
      0 • yj • ↑(↑B (↑(Pi.basisFun R n) i✝)) (↑(Pi.basisFun R m) j)) =
    0
simp only [zero_smul, Finsupp.sum_zero]