awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ (((((toLinearMapₛₗ₂ σ₁ b₁ b₂ : (a : Matrix n m N₂) → M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) M : M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂) :
              (a : M₁) → M₂ →ₗ[R] N₂)
            ((b₁ : (a : n) → M₁) i) :
          M₂ →ₗ[R] N₂) :
        (a : M₂) → N₂)
      ((b₂ : (a : m) → M₂) j : M₂) =
    M i j
have simp : ∑ x : n,
    ∑ x_1 : m,
      ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) x : R) : R) •>
        ((Finsupp.single j 1 : (a : m) → R) x_1 : R) •> M x x_1 =
  M i j
Tactic: simp only [toLinearMapₛₗ₂_apply, Basis.repr_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ ∑ x : n,
      ∑ x_1 : m,
        ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) x : R) : R) •>
          ((Finsupp.single j 1 : (a : m) → R) x_1 : R) •> M x x_1 =
    M i j
have rw : ((σ₁ : (a : R) → R) ((Finsupp.single i 1 : (a : n) → R) i : R) : R) •>
    ((Finsupp.single j 1 : (a : m) → R) j : R) •> M i j =
  M i j
Tactic: rw [Finset.sum_eq_single_of_mem i (by simp) fun k _ hk ↦ by simp [hk],
    Finset.sum_eq_single_of_mem j (by simp) fun k _ hk ↦ by simp [hk]]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
⊢ Eq (α := R)
    ((⇑σ₁ : (a : R) → R) ∘ x ⬝ᵥ
        (toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B *ᵥ (⇑σ₂ : (a : R) → R) ∘ y :
      R)
    ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁.equivFun.symm : (a : n → R) → M₁) x) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
        ((b₂.equivFun.symm : (a : m → R) → M₂) y : M₂) :
      R)
have simp : Eq.{u_1 + 1} (α := R)
  (∑ x_1 : n,
    ∑ i : m,
      HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
        (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) i : M₂) :
            R)))
  (∑ x_1 : m,
    ∑ i : n,
      HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
        (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x_1 : M₂) :
            R)))
Tactic: simp only [dotProduct, Function.comp_apply, Function.comp_def, mulVec_eq_sum, op_smul_eq_smul,
    Finset.sum_apply, Pi.smul_apply, transpose_apply, toMatrix₂_apply, smul_eq_mul, mul_sum,
    Basis.equivFun_symm_apply, map_sum, map_smulₛₗ, coe_sum, LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 : n,
      ∑ i : m,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) i : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))
have rw : Eq.{u_1 + 1} (α := R)
  (∑ y_1 : m,
    ∑ x_1 : n,
      HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
        (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y y_1) : R)
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) y_1 : M₂) :
            R)))
  (∑ x_1 : m,
    ∑ i : n,
      HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
        (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x_1 : M₂) :
            R)))
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y_1 : m,
      ∑ x_1 : n,
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y y_1) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_1) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) y_1 : M₂) :
              R)))
    (∑ x_1 : m,
      ∑ i : n,
        HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y x_1) : R)
          (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x i) : R)
            ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x_1 : M₂) :
              R)))
have refine : ∀ (i : m),
  Membership.mem (γ := Finset m) univ i →
    ∀ (j : n),
      Membership.mem (γ := Finset n) univ j →
        HMul.hMul (α := R) ((σ₁ : (a : R) → R) (x j) : R)
            (HMul.hMul (α := R) (β := R) ((σ₂ : (a : R) → R) (y i) : R)
              ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) j) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) i : M₂) :
                R)) =
          HMul.hMul (α := R) ((σ₂ : (a : R) → R) (y i) : R)
            (HMul.hMul (α := R) (β := R) ((σ₁ : (a : R) → R) (x j) : R)
              ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) j) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
                  ((b₂ : (a : m) → M₂) i : M₂) :
                R))
Tactic: refine Finset.sum_congr rfl (fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ Eq (α := R) ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) x : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R) y : R)
    (dotProduct.{u_1, u_11} (m := n)
        (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
          (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
      R)
have nth_rw : Eq (α := R)
  (((B : (a : M₁) → M₂ →ₛₗ[σ₂] R)
          (∑ i : n,
            ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) •> ((b₁ : (a : n) → M₁) i : M₁)) :
        (a : M₂) → R)
      (∑ i : m, ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) i : R) •> ((b₂ : (a : m) → M₂) i : M₂)) :
    R)
  (dotProduct.{u_1, u_11} (m := n)
      (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
      (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
        (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
    R)
Tactic: nth_rw 1 [← b₁.sum_repr x, ← b₂.sum_repr y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ Eq (α := R)
    (((B : (a : M₁) → M₂ →ₛₗ[σ₂] R)
            (∑ i : n,
              ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) •> ((b₁ : (a : n) → M₁) i : M₁)) :
          (a : M₂) → R)
        (∑ i : m, ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) i : R) •> ((b₂ : (a : m) → M₂) i : M₂)) :
      R)
    (dotProduct.{u_1, u_11} (m := n)
        (Function.comp (β := R) (⇑σ₁ : (a : R) → R) (⇑((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (mulVec.{u_1, u_11, u_12} (n := m) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) → Matrix n m R) B)
          (Function.comp (β := R) (⇑σ₂ : (a : R) → R) (⇑((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R))) :
      R)
have suffices : Eq.{u_1 + 1} (α := R)
  (∑ j : m,
    ∑ i : n,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R)
          ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R))
        ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) j : M₂) :
          R))
  (∑ i : n,
    ∑ j : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
          ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
        ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) j : M₂) :
          R))
Tactic: suffices ∑ j, ∑ i, σ₂ (b₂.repr y j) * σ₁ (b₁.repr x i) * B (b₁ i) (b₂ j) =
           ∑ i, ∑ j, σ₁ (b₁.repr x i) * σ₂ (b₂.repr y j) * B (b₁ i) (b₂ j) by
    simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
σ₁ σ₂ : R →+* R
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ Eq.{u_1 + 1} (α := R)
    (∑ j : m,
      ∑ i : n,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
    (∑ i : n,
      ∑ j : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
            ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
          ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
have simp_rw : Eq.{u_1 + 1} (α := R)
  (∑ x_1 : m,
    ∑ x_2 : n,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) x_2 : R) : R)
          ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) x_1 : R) : R))
        ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) x_2) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) x_1 : M₂) :
          R))
  (∑ i : n,
    ∑ j : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((σ₁ : (a : R) → R) ((((b₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i : R) : R)
          ((σ₂ : (a : R) → R) ((((b₂.repr : (a : M₂) → m →₀ R) y : m →₀ R) : (a : m) → R) j : R) : R))
        ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] R) : (a : M₂) → R)
            ((b₂ : (a : m) → M₂) j : M₂) :
          R))
Tactic: simp_rw [mul_comm (σ₂ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ σ₂ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R (⇑b₁ : (a : n) → M₁) (⇑b₂ : (a : m) → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        B i j :
      N₂)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂) B i j : N₂)
have rw : Eq.{u_10 + 1} (α := N₂)
  (((toMatrix₂Aux R (⇑b₁ : (a : n) → M₁) (⇑b₂ : (a : m) → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      B i j :
    N₂)
  ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
      ((b₂ : (a : m) → M₂) j : M₂) :
    N₂)
Tactic: rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
σ₁ σ₂ : R →+* R
inst_7 : Fintype n
inst_8 : Fintype m
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
i : n
j : m
rw :
  Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R (⇑b₁ : (a : n) → M₁) (⇑b₂ : (a : m) → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        B i j :
      N₂)
    ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
        ((b₂ : (a : m) → M₂) j : M₂) :
      N₂)
⊢ Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R (⇑b₁ : (a : n) → M₁) (⇑b₂ : (a : m) → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        B i j :
      N₂)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) → Matrix n m N₂) B i j : N₂)
have rw₁ : Eq.{u_10 + 1} (α := N₂)
  ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
      ((b₂ : (a : m) → M₂) j : M₂) :
    N₂)
  ((((B : (a : M₁) → M₂ →ₛₗ[σ₂] N₂) ((b₁ : (a : n) → M₁) i) : M₂ →ₛₗ[σ₂] N₂) : (a : M₂) → N₂)
      ((b₂ : (a : m) → M₂) j : M₂) :
    N₂)
Tactic: rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : DecidableEq m
inst_6 : DecidableEq n
⊢ Eq (α := Matrix n m N₂ ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) (toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m))
    (toLinearMap₂' R)
have h : ∀ (M : Matrix n m N₂) (i : n) (i_1 : m),
  Eq.{u_10 + 1} (α := N₂)
    ((((((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix n m N₂) → (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) M ∘ₗ
                      LinearMap.single R (fun (i : n) ↦ R) i :
                    R →ₗ[R] (m → R) →ₗ[R] N₂) :
                  (a : R) → (m → R) →ₗ[R] N₂)
                1 ∘ₗ
              LinearMap.single R (fun (i : m) ↦ R) i_1 :
            R →ₗ[R] N₂) :
          (a : R) → N₂)
        1 :
      N₂)
    (((((((toLinearMap₂' R : Matrix n m N₂ ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) :
                          (a : Matrix n m N₂) → (n → R) →ₗ[R] (m → R) →ₗ[R] N₂)
                        M ∘ₗ
                      LinearMap.single R (fun (i : n) ↦ R) i :
                    R →ₗ[R] (m → R) →ₗ[R] N₂) :
                  (a : R) → (m → R) →ₗ[R] N₂)
                1 ∘ₗ
              LinearMap.single R (fun (i : m) ↦ R) i_1 :
            R →ₗ[R] N₂) :
          (a : R) → N₂)
        1 :
      N₂)
Tactic: ext M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : DecidableEq m
inst_6 : DecidableEq n
⊢ Eq (α := ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) (toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m))
    (toMatrix₂' R)
have h : ∀ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) (i : n) (j : m),
  Eq.{u_10 + 1} (α := N₂)
    ((toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂) B i j : N₂)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
        B i j :
      N₂)
Tactic: ext B
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : DecidableEq m
inst_6 : DecidableEq n
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂)
    ((toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂) B i j : N₂)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
        B i j :
      N₂)
have h : Eq.{u_10 + 1} (α := N₂)
  ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] N₂) :
        (a : m → R) → N₂)
      ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
    N₂)
  (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
        (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
      B i j :
    N₂)
Tactic: rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : DecidableEq m
inst_6 : DecidableEq n
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i : n
j : m
h :
  Eq.{u_10 + 1} (α := N₂)
    ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] N₂) :
          (a : m → R) → N₂)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
      N₂)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
        B i j :
      N₂)
⊢ Eq.{u_10 + 1} (α := N₂)
    ((toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂) B i j : N₂)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
        B i j :
      N₂)
have h₁ : Eq.{u_10 + 1} (α := N₂)
  ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] N₂) :
        (a : m → R) → N₂)
      ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
    N₂)
  ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) (Pi.single (M := fun (a : n) ↦ R) i 1) : (m → R) →ₗ[R] N₂) : (a : m → R) → N₂)
      (Pi.single (M := fun (a : m) ↦ R) j 1) :
    N₂)
Tactic: rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid N₂
inst_2 : Module R N₂
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : DecidableEq m
inst_6 : DecidableEq n
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i : n
j : m
h :
  Eq.{u_10 + 1} (α := N₂)
    ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] N₂) :
          (a : m → R) → N₂)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
      N₂)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
        B i j :
      N₂)
h₁ :
  Eq.{u_10 + 1} (α := N₂)
    ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) ((Pi.basisFun R n : (a : n) → n → R) i) : (m → R) →ₗ[R] N₂) :
          (a : m → R) → N₂)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
      N₂)
    ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) (Pi.single (M := fun (a : n) ↦ R) i 1) : (m → R) →ₗ[R] N₂) :
          (a : m → R) → N₂)
        (Pi.single (M := fun (a : m) ↦ R) j 1) :
      N₂)
⊢ Eq.{u_10 + 1} (α := N₂)
    ((toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) : (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂) B i j : N₂)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (m → R) →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂) :
          (a : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂) → Matrix n m N₂)
        B i j :
      N₂)
have h₂ : Eq.{u_10 + 1} (α := N₂)
  ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) (Pi.single (M := fun (j : n) ↦ R) i 1) : (m → R) →ₗ[R] N₂) : (a : m → R) → N₂)
      ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
    N₂)
  ((((B : (a : n → R) → (m → R) →ₗ[R] N₂) (Pi.single (M := fun (a : n) ↦ R) i 1) : (m → R) →ₗ[R] N₂) : (a : m → R) → N₂)
      (Pi.single (M := fun (a : m) ↦ R) j 1) :
    N₂)
Tactic: rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]