awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h : B * (A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B)) = B * (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)
⊢ B * A = 1
have h₁ : B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) =
  detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B)
Tactic: simp only [mul_add, Matrix.mul_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B)
⊢ B * A = 1
have h₁ : B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
    HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1 =
  detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
    HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1
Tactic: replace h := congr($h + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
      HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1 =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
      HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1
⊢ B * A = 1
have h₁ : B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
    (detp 1 A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp (-1) B) 1 +
      detp (-1) A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 B) 1) =
  detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
    (detp 1 A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp (-1) B) 1 +
      detp (-1) A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 B) 1)
Tactic: simp_rw [add_smul, ← smul_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ (((toLinearMap₂'Aux σ₁ σ₂ f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (a : n) ↦ R₁) i 1) :
          (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : m → R₂) → N₂)
      (Pi.single (M := fun (a : m) ↦ R₂) j 1) =
    f i j
have rw : ∑ i_1 : n,
    ∑ j_1 : m,
      ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
        ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1 =
  f i j
Tactic: rw [Matrix.toLinearMap₂'Aux, mk₂'ₛₗ_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
have simp_rw : ∑ x : n, (if i = x then 1 else 0) •> ∑ x_1 : m, (if j = x_1 then 1 else 0) •> f x x_1 = f i j
Tactic: simp_rw [← Finset.smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (hypothesis)
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
          ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1 =
    f i j
have this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
Tactic: have : (∑ i', ∑ j', (if i = i' then (1 : S₁) else (0 : S₁)) •
        (if j = j' then (1 : S₂) else (0 : S₂)) • f i' j') =
      f i j := by
    simp_rw [← Finset.smul_sum]
    simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
⊢ ∑ i_1 : n,
      ∑ j_1 : m,
        ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
          ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1 =
    f i j
have rw : Eq.{u_10 + 1} (α := N₂)
  (∑ i_1 : n,
    ∑ j_1 : m,
      ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
        ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1)
  (∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j')
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
⊢ toLinearMap₂'Aux σ₁ σ₂
      (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
              Pi.single (M := fun (j : m) ↦ R₂) j 1 :
            (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        f) =
    f
have refine : ∀ (i : n) (j : m),
  Eq.{u_10 + 1} (α := N₂)
    ((((toLinearMap₂'Aux σ₁ σ₂
                  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                          Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                        (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                      (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                    f) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
Tactic: refine ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
i : n
j : m
⊢ Eq.{u_10 + 1} (α := N₂)
    ((((toLinearMap₂'Aux σ₁ σ₂
                  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                          Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                        (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                      (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                    f) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
have simp_rw : Eq.{u_10 + 1} (α := N₂)
  ((((toLinearMap₂'Aux σ₁ σ₂
                (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                        Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                      (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                    (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                  f) :
              (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
            (Pi.single (M := fun (j : n) ↦ R₁) i 1) :
          (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : m → R₂) → N₂)
      (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
    N₂)
  ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (j : n) ↦ R₁) i 1) : (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : m → R₂) → N₂)
      (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
    N₂)
Tactic: simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
i : n
j : m
simp_rw :
  Eq.{u_10 + 1} (α := N₂)
    ((((toLinearMap₂'Aux σ₁ σ₂
                  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                          Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                        (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                      (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                    f) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              (Pi.single (M := fun (j : n) ↦ R₁) i 1) :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (j : n) ↦ R₁) i 1) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
      N₂)
⊢ Eq.{u_10 + 1} (α := N₂)
    ((((toLinearMap₂'Aux σ₁ σ₂
                  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                          Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                        (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                      (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                    f) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
have simp_rw₁ : Eq.{u_10 + 1} (α := N₂)
  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      f i j :
    N₂)
  ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (j : n) ↦ R₁) i 1) : (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : m → R₂) → N₂)
      (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
    N₂)
Tactic: simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : Matrix n m N₂
⊢ ((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      (toLinearMap₂'Aux σ₁ σ₂ f) =
    f
have a : ∀ (i : n) (j : m),
  ((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      (toLinearMap₂'Aux σ₁ σ₂ f) i j =
    f i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
            Pi.single (M := fun (j : m) ↦ R₂) j 1 :
          (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
        (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
      (toLinearMap₂'Aux σ₁ σ₂ f) i j =
    f i j
have a : (((toLinearMap₂'Aux σ₁ σ₂ f : (a : (j : n) → R₁) → ((j : m) → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (j : n) ↦ R₁) i 1) :
        ((j : m) → R₂) →ₛₗ[σ₂] N₂) :
      (a : (j : m) → R₂) → N₂)
    (Pi.single (M := fun (j : m) ↦ R₂) j 1) =
  f i j
Tactic: simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
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 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
⊢ Eq.{u_10 + 1} (α := N₂)
    (((((((toLinearMapₛₗ₂' R σ₁ σ₂ : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
                      (a : Matrix n m N₂) → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
                    M :
                  (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              x :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        y :
      N₂)
    (∑ i : n, ∑ j : m, ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> M i j : N₂)
have rw : Eq.{u_10 + 1} (α := N₂)
  (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> M i j)
  (∑ i : n, ∑ j : m, ((σ₁ : (a : R₁) → S₁) (x i) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y j) : S₂) •> M i j)
Tactic: rw [toLinearMapₛₗ₂', toMatrixₛₗ₂', LinearEquiv.coe_symm_mk, toLinearMap₂'Aux, mk₂'ₛₗ_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
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 : Semiring R₁
inst_4 : Semiring R₂
inst_5 : Semiring S₁
inst_6 : Semiring S₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
x_1 : n
h : Membership.mem (γ := Finset n) univ x_1
x_2 : m
h_1 : Membership.mem (γ := Finset m) univ x_2
⊢ ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 =
    ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> M x_1 x_2
have rw : ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> M x_1 x_2 =
  ((σ₁ : (a : R₁) → S₁) (x x_1) : S₁) •> ((σ₂ : (a : R₂) → S₂) (y x_2) : S₂) •> M x_1 x_2
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
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 : Semiring S₁
inst_4 : Semiring S₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₁ R N₂
inst_8 : SMulCommClass S₂ R N₂
inst_9 : SMulCommClass S₂ S₁ N₂
inst_10 : Fintype n
inst_11 : Fintype m
inst_12 : DecidableEq n
inst_13 : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x_1 : n
h : Membership.mem (γ := Finset n) univ x_1
x_2 : m
h_1 : Membership.mem (γ := Finset m) univ x_2
⊢ ((RingHom.id S₂ : (a : S₂) → S₂) (y x_2) : S₂) •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 =
    x x_1 •> y x_2 •> M x_1 x_2
have rw : y x_2 •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
Tactic: rw [RingHom.id_apply, RingHom.id_apply, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
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 : Semiring S₁
inst_4 : Semiring S₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₁ R N₂
inst_8 : SMulCommClass S₂ R N₂
inst_9 : SMulCommClass S₂ S₁ N₂
inst_10 : Fintype n
inst_11 : Fintype m
inst_12 : DecidableEq n
inst_13 : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x_1 : n
h : Membership.mem (γ := Finset n) univ x_1
x_2 : m
h_1 : Membership.mem (γ := Finset m) univ x_2
rw : y x_2 •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
⊢ ((RingHom.id S₂ : (a : S₂) → S₂) (y x_2) : S₂) •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 =
    x x_1 •> y x_2 •> M x_1 x_2
have rw₁ : y x_2 •> x x_1 •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
Tactic: rw [RingHom.id_apply, RingHom.id_apply, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
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 : Semiring S₁
inst_4 : Semiring S₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₁ R N₂
inst_8 : SMulCommClass S₂ R N₂
inst_9 : SMulCommClass S₂ S₁ N₂
inst_10 : Fintype n
inst_11 : Fintype m
inst_12 : DecidableEq n
inst_13 : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x_1 : n
h : Membership.mem (γ := Finset n) univ x_1
x_2 : m
h_1 : Membership.mem (γ := Finset m) univ x_2
rw : y x_2 •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
rw₁ : y x_2 •> x x_1 •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
⊢ ((RingHom.id S₂ : (a : S₂) → S₂) (y x_2) : S₂) •> ((RingHom.id S₁ : (a : S₁) → S₁) (x x_1) : S₁) •> M x_1 x_2 =
    x x_1 •> y x_2 •> M x_1 x_2
have rw₂ : x x_1 •> y x_2 •> M x_1 x_2 = x x_1 •> y x_2 •> M x_1 x_2
Tactic: rw [RingHom.id_apply, RingHom.id_apply, smul_comm]
-- 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
⊢ ((((((toLinearMap₂' T : Matrix n m T ≃ₗ[T] (n → T) →ₗ[T] (m → T) →ₗ[T] T) :
                    (a : Matrix n m T) → (n → T) →ₗ[T] (m → T) →ₗ[T] T)
                  M :
                (n → T) →ₗ[T] (m → T) →ₗ[T] T) :
              (a : n → T) → (m → T) →ₗ[T] T)
            v :
          (m → T) →ₗ[T] T) :
        (a : m → T) → T)
      w =
    v ⬝ᵥ M *ᵥ w
have simp_rw : 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)
Tactic: simp_rw [Matrix.toLinearMap₂'_apply, dotProduct, Matrix.mulVec, dotProduct]