-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂'_compl₁₂ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (l : (n' → R) →ₗ[R] n → R)
    (r : (m' → R) →ₗ[R] m → R) :
    toMatrix₂' R (B.compl₁₂ l r) = (toMatrix' l)ᵀ * toMatrix₂' R B * toMatrix' r

Proof state:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 (Pi.single i 1))) (r (Pi.single j 1)) =
    ∑ y : n,
      ∑ x : m,
        of (fun i j => l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j => r (Pi.single j 1) i) x j

Tactic:
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]

Result:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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'
⊢ (((Pi.basisFun R n).repr (l (Pi.single i 1))).sum fun i xi =>
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum 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 (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j => r (Pi.single j 1) i) x j

Proof state:
case a.h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 (Pi.single i 1))) i' •> 0 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) = 0

Tactic:
intros

Result:
case a.h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 (Pi.single i 1))) i' •> 0 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i✝) = 0

Proof state:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 (Pi.single i 1))) (r (Pi.single j 1)) =
    ∑ x : m,
      ∑ i_1 : n,
        of (fun i j => l (Pi.single j 1) i) i_1 i * (B (Pi.single i_1 1)) (Pi.single x 1) *
          of (fun i j => r (Pi.single j 1) i) x j

Tactic:
rw [sum_comm]

Result:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 (Pi.single i 1))) (r (Pi.single j 1)) =
    ∑ y : n,
      ∑ x : m,
        of (fun i j => l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j => r (Pi.single j 1) i) x j

Proof state:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 (Pi.single i 1))) i' •>
      ((Pi.basisFun R m).repr (r (Pi.single j 1))) j' •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) j') =
    of (fun i j => l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single j' 1) *
      of (fun i j => r (Pi.single j 1) i) j' j

Tactic:
simp only [smul_eq_mul, Pi.basisFun_repr, mul_assoc, mul_comm, mul_left_comm,
  Pi.basisFun_apply, of_apply]

Result:
no goals

Proof state:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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 ∈ univ,
    (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj =>
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) x •> yj •> (B ((Pi.basisFun R n) x)) ((Pi.basisFun R m) j)) =
      ∑ x_1 : m,
        of (fun i j => l (Pi.single j 1) i) x i * (B (Pi.single x 1)) (Pi.single x_1 1) *
          of (fun i j => r (Pi.single j 1) i) x_1 j

Tactic:
rintro i' -

Result:
case a
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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
⊢ (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj =>
      ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •> yj •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) j)) =
    ∑ x : m,
      of (fun i j => l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j => r (Pi.single j 1) i) x j

Proof state:
case a.h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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
⊢ (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj =>
      0 •> yj •> (B ((Pi.basisFun R n) i✝)) ((Pi.basisFun R m) j)) =
    0

Tactic:
simp only [zero_smul, Finsupp.sum_zero]

Result:
no goals

Proof state:
case a.h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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),
    (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj =>
        0 •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) =
      0

Tactic:
intros

Result:
case a.h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
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
⊢ (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj =>
      0 •> yj •> (B ((Pi.basisFun R n) i✝)) ((Pi.basisFun R m) j)) =
    0