awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ Eq.{u_16 + 1} (α := T) (∑ i : n, ∑ j : m, v i •> w j •> M i j) (∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1)
have refine : ∀ (x : n), Membership.mem (γ := Finset n) univ x → ∑ j : m, v x •> w j •> M x j = v x * ∑ x_2 : m, M x x_2 * w x_2
Tactic: refine Finset.sum_congr rfl fun _ _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
⊢ ∑ j : m, v x •> w j •> M x j = v x * ∑ x_1 : m, M x x_1 * w x_1
have rw : Eq.{u_16 + 1} (α := T) (∑ j : m, v x •> w j •> M x j) (∑ i : m, v x * (M x i * w i))
Tactic: rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
⊢ Eq.{u_16 + 1} (α := T) (∑ j : m, v x •> w j •> M x j) (∑ i : m, v x * (M x i * w i))
have refine : ∀ (x_1 : m), Membership.mem (γ := Finset m) univ x_1 → v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
Tactic: refine Finset.sum_congr rfl fun _ _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
x_1 : m
h_1 : Membership.mem (γ := Finset m) univ x_1
⊢ v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
have rw : v x * w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
x_1 : m
h_1 : Membership.mem (γ := Finset m) univ x_1
rw : v x * w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
⊢ v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
have rw₁ : v x * (w x_1 * M x x_1) = v x * (M x x_1 * w x_1)
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
x_1 : m
h_1 : Membership.mem (γ := Finset m) univ x_1
rw : v x * w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
rw₁ : v x * (w x_1 * M x x_1) = v x * (M x x_1 * w x_1)
⊢ v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
have rw₂ : v x * (M x x_1 * w x_1) = v x * (M x x_1 * w x_1)
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq n
inst_3 : DecidableEq m
T : Type u_16
inst_4 : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x : n
h : Membership.mem (γ := Finset n) univ x
x_1 : m
h_1 : Membership.mem (γ := Finset m) univ x_1
rw : v x * w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
rw₁ : v x * (w x_1 * M x x_1) = v x * (M x x_1 * w x_1)
rw₂ : v x * (M x x_1 * w x_1) = v x * (M x x_1 * w x_1)
⊢ v x •> w x_1 •> M x x_1 = v x * (M x x_1 * w x_1)
have rw₃ : v x * M x x_1 * w x_1 = v x * M x x_1 * w x_1
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
⊢ ((toMatrix₂' R : ((n' → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m' R) :
        (a : (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ l r) =
    HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) l)ᵀ
        (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
              (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
            B :
          Matrix n m R))
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) r : Matrix m m' R)
have a : ∀ (i : n') (j : m'),
  ((toMatrix₂' R : ((n' → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m' R) :
        (a : (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ l r) i j =
    HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) l)ᵀ
        (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
              (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
            B :
          Matrix n m R))
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) r : Matrix m m' R) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : 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₂' R : ((n' → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m' R) :
        (a : (n' → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ l r) i j =
    HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) l)ᵀ
        (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
              (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
            B :
          Matrix n m R))
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) r : Matrix m m' R) i j
have a : Eq.{u_16 + 1} (α := R)
  ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
          (m → R) →ₗ[R] R) :
        (a : m → R) → R)
      ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
    R)
  (∑ x : m,
      ∑ i_1 : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((of : (a : n → n' → R) → Matrix n n' R)
                (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i_1 i :
              R)
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i_1 1) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                (Pi.single (M := fun (a : m) ↦ R) x 1) :
              R))
          ((of : (a : m → m' → R) → Matrix m m' R)
              (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
            R) :
    R)
Tactic: simp only [LinearMap.toMatrix₂'_apply, LinearMap.compl₁₂_apply, transpose_apply, Matrix.mul_apply,
    LinearMap.toMatrix', LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, sum_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : 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'
⊢ Eq.{u_16 + 1} (α := R)
    ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
            (m → R) →ₗ[R] R) :
          (a : m → R) → R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
      R)
    (∑ x : m,
        ∑ i_1 : n,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i_1 i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i_1 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
              R) :
      R)
have a : Eq.{u_16 + 1} (α := R)
  ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
          (m → R) →ₗ[R] R) :
        (a : m → R) → R)
      ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
    R)
  (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((of : (a : n → n' → R) → Matrix n n' R)
                (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
              R)
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                (Pi.single (M := fun (a : m) ↦ R) x 1) :
              R))
          ((of : (a : m → m' → R) → Matrix m m' R)
              (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
            R) :
    R)
Tactic: rw [sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : 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 : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
          (m → R) →ₗ[R] R) :
        (a : m → R) → R)
      ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
    R)
have rw : Finsupp.sum
  ((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
    ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)))
  fun (i : n) (xi : R) ↦
  Finsupp.sum
    ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
      ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
    fun (j : m) (yj : R) ↦
    xi •>
      yj •>
        ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] R) :
              (a : m → R) → R)
            ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
          R)
Tactic: rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : 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'
⊢ Eq.{u_16 + 1} (α := R)
    ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
            (m → R) →ₗ[R] R) :
          (a : m → R) → R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) : m → R) :
      R)
    (∑ y : n,
        ∑ x : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
              R) :
      R)
have a : Eq.{u_16 + 1} (α := R)
  (Finsupp.sum
    ((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
      ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)))
    fun (i : n) (xi : R) ↦
    Finsupp.sum
      ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
      fun (j : m) (yj : R) ↦
      xi •>
        yj •>
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
            R))
  (∑ y : n,
    ∑ x : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((of : (a : n → n' → R) → Matrix n n' R)
              (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
            R)
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              (Pi.single (M := fun (a : m) ↦ R) x 1) :
            R))
        ((of : (a : m → m' → R) → Matrix m m' R)
            (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
          R))
Tactic: conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : 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'
⊢ Eq.{u_16 + 1} (α := R)
    (Finsupp.sum
      ((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
        ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)))
      fun (i : n) (xi : R) ↦
      Finsupp.sum
        ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
          ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
        fun (j : m) (yj : R) ↦
        xi •>
          yj •>
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((of : (a : n → n' → R) → Matrix n n' R)
                (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
              R)
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                (Pi.single (M := fun (a : m) ↦ R) x 1) :
              R))
          ((of : (a : m → m' → R) → Matrix m m' R)
              (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
            R))
have a : Eq.{u_16 + 1} (α := R)
  (∑ i_1 : n,
    Finsupp.sum
      ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
      fun (j : m) (yj : R) ↦
      ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                  ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
                n →₀ R) :
              (a : n) → R)
            i_1 :
          R) •>
        yj •>
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i_1) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
            R))
  (∑ y : n,
    ∑ x : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((of : (a : n → n' → R) → Matrix n n' R)
              (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
            R)
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              (Pi.single (M := fun (a : m) ↦ R) x 1) :
            R))
        ((of : (a : m → m' → R) → Matrix m m' R)
            (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
          R))
Tactic: rw [Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : 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
⊢ Eq.{u_16 + 1} (α := R)
    (Finsupp.sum
      ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
        ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
      fun (j : m) (yj : R) ↦
      ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                  ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
                n →₀ R) :
              (a : n) → R)
            i' :
          R) •>
        yj •>
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i') : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
            R))
    (∑ x : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((of : (a : n → n' → R) → Matrix n n' R)
              (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i' i :
            R)
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i' 1) : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              (Pi.single (M := fun (a : m) ↦ R) x 1) :
            R))
        ((of : (a : m → m' → R) → Matrix m m' R)
            (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
          R))
have a : Eq.{u_16 + 1} (α := R)
  (∑ i_1 : m,
    ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
              n →₀ R) :
            (a : n) → R)
          i' :
        R) •>
      ((((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
                  ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)) :
                m →₀ R) :
              (a : m) → R)
            i_1 :
          R) •>
        ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i') : (m → R) →ₗ[R] R) :
              (a : m → R) → R)
            ((Pi.basisFun R m : (a : m) → m → R) i_1 : m → R) :
          R))
  (∑ x : m,
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R)
        ((of : (a : n → n' → R) → Matrix n n' R)
            (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) i' i :
          R)
        ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i' 1) : (m → R) →ₗ[R] R) :
              (a : m → R) → R)
            (Pi.single (M := fun (a : m) ↦ R) x 1) :
          R))
      ((of : (a : m → m' → R) → Matrix m m' R)
          (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
        R))
Tactic: rw [Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ ((toMatrix₂' R : ((n' → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m R) :
        (a : (n' → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n' m R)
      (B ∘ₗ f) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) f)ᵀ
      (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
            (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
          B :
        Matrix n m R)
have rw : ((toMatrix₂' R : ((n' → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n' m R) :
      (a : (n' → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n' m R)
    (B.compl₁₂ f id) =
  HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix' : (a : (n' → R) →ₗ[R] n → R) → Matrix n n' R) f)ᵀ
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
        B :
      Matrix n m R)
Tactic: rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
n : Type u_11
m : Type u_12
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype m'
inst_6 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ ((toMatrix₂' R : ((n → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n m' R) :
        (a : (n → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n m' R)
      (B.compl₂ f) =
    HMul.hMul (α := Matrix n m R) (β := Matrix m m' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
            (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
          B :
        Matrix n m R)
      ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) f : Matrix m m' R)
have rw : ((toMatrix₂' R : ((n → R) →ₗ[R] (m' → R) →ₗ[R] R) ≃ₗ[R] Matrix n m' R) :
      (a : (n → R) →ₗ[R] (m' → R) →ₗ[R] R) → Matrix n m' R)
    (B.compl₁₂ id f) =
  HMul.hMul (α := Matrix n m R) (β := Matrix m m' R)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] R) → Matrix n m R)
        (B ∘ₗ id) :
      Matrix n m R)
    ((toMatrix' : (a : (m' → R) →ₗ[R] m → R) → Matrix m m' R) f : Matrix m m' R)
Tactic: rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂]