awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
⊢ det (n := m × n)
      ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
            Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
          (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
        B) =
    (HMul.hMul (α := Matrix (m × n) (m × n) γ) (β := Matrix (m × n) (m × n) γ)
        ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
                Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            1 :
          Matrix (m × n) (m × n) γ)
        (((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) 1 :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            B :
          Matrix (m × n) (m × n) γ)).det
have rw : Eq.{u_7 + 1} (α := γ)
  (det (n := m × n)
    ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
          Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
        (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
      B))
  (det (n := m × n)
    ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) (A * 1) :
          Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
        (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
      (1 * B)))
Tactic: rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
rw :
  Eq.{u_7 + 1} (α := γ)
    (det (n := m × n)
      ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
            Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
          (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
        B))
    (det (n := m × n)
      ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) (A * 1) :
            Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
          (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
        (1 * B)))
⊢ det (n := m × n)
      ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
            Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
          (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
        B) =
    (HMul.hMul (α := Matrix (m × n) (m × n) γ) (β := Matrix (m × n) (m × n) γ)
        ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
                Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            1 :
          Matrix (m × n) (m × n) γ)
        (((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) 1 :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            B :
          Matrix (m × n) (m × n) γ)).det
have rw₁ : Eq.{u_7 + 1} (α := γ)
  (det (n := m × n)
    ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
          Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
        (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
      B))
  (det (n := m × n)
    ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
          Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
        (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
      (1 * B)))
Tactic: rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
⊢ (HMul.hMul (α := Matrix (m × n) (m × n) γ) (β := Matrix (m × n) (m × n) γ)
        ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
                Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            1 :
          Matrix (m × n) (m × n) γ)
        (((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) 1 :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            B :
          Matrix (m × n) (m × n) γ)).det =
    HMul.hMul (α := γ)
      (det (n := m × n)
        (blockDiagonal fun (x : n) ↦ A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (det (n := n × m) (blockDiagonal fun (x : m) ↦ B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b))
have rw : ∀ (x : β), Eq.{u_7 + 1} (α := γ) (((f : (a : α) → β →ₗ[S] γ) 0 : (a : β) → γ) x : γ) (0 : γ)
Tactic: rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
rw : ∀ (x : β), Eq.{u_7 + 1} (α := γ) (((f : (a : α) → β →ₗ[S] γ) 0 : (a : β) → γ) x : γ) (0 : γ)
⊢ (HMul.hMul (α := Matrix (m × n) (m × n) γ) (β := Matrix (m × n) (m × n) γ)
        ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
                Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            1 :
          Matrix (m × n) (m × n) γ)
        (((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) 1 :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            B :
          Matrix (m × n) (m × n) γ)).det =
    HMul.hMul (α := γ)
      (det (n := m × n)
        (blockDiagonal fun (x : n) ↦ A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (det (n := n × m) (blockDiagonal fun (x : m) ↦ B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b))
have rw₁ : ∀ (x : α), Eq.{u_7 + 1} (α := γ) ((((f : (a : α) → β →ₗ[S] γ) x : β →ₗ[S] γ) : (a : β) → γ) 0 : γ) (0 : γ)
Tactic: rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
⊢ HMul.hMul (α := γ)
      (det (n := m × n)
        (blockDiagonal fun (x : n) ↦ A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (det (n := n × m)
        (blockDiagonal fun (x : m) ↦ B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) =
    HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Fintype.card n) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
have simp_rw : HMul.hMul (α := γ) (∏ k : n, det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
    (∏ k : m, det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) =
  HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (Fintype.card n) *
    HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
Tactic: simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
simp_rw :
  HMul.hMul (α := γ) (∏ k : n, det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (∏ k : m, det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) =
    HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Fintype.card n) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
⊢ HMul.hMul (α := γ)
      (det (n := m × n)
        (blockDiagonal fun (x : n) ↦ A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (det (n := n × m)
        (blockDiagonal fun (x : m) ↦ B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) =
    HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Fintype.card n) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
have simp_rw₁ : HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (Finset.card.{u_11} (α := n) Finset.univ) *
    HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b))
      (Finset.card.{u_10} (α := m) Finset.univ) =
  HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (Fintype.card n) *
    HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
Tactic: simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq m
inst_2 : DecidableEq n
a b : ℕ
⊢ Eq (α := Matrix (m × n) (m × n) α) (diagonal fun (mn : m × n) ↦ HMul.hMul (α := α) (↑a : α) (↑b : α))
    (↑(a * b) : Matrix (m × n) (m × n) α)
have simp_rw : Eq (α := Matrix (m × n) (m × n) α) (diagonal fun (mn : m × n) ↦ (↑(a * b) : α)) (↑(a * b) : Matrix (m × n) (m × n) α)
Tactic: simp_rw [← Nat.cast_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq n
A : Matrix l m α
b : ℕ
⊢ Eq (α := Matrix (l × n) (m × n) α) (blockDiagonal fun (i : n) ↦ A <• (↑b : α)) (blockDiagonal fun (x : n) ↦ b •> A)
have h : ∀ (x : n), A <• (↑b : α) = b •> A
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq n
A : Matrix l m α
b : ℕ
x : n
⊢ A <• (↑b : α) = b •> A
have h : ∀ (i : l) (j : m), (A <• (↑b : α)) i j = (b •> A) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ Eq (α := Matrix (l × m) (l × n) α)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
        (blockDiagonal fun (i : l) ↦ (↑a : α) •> B) :
      Matrix (l × m) (l × n) α)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
        (blockDiagonal fun (x : l) ↦ a •> B) :
      Matrix (l × m) (l × n) α)
have h : Eq (α := l → Matrix m n α) (fun (i : l) ↦ (↑a : α) •> B) fun (x : l) ↦ a •> B
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ Eq (α := l → Matrix m n α) (fun (i : l) ↦ (↑a : α) •> B) fun (x : l) ↦ a •> B
have h : ∀ (x : l) (i : m) (j : n), ((↑a : α) •> B) i j = (a •> B) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
m : Type u_10
n : Type u_11
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ det (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) = A.det ^ Fintype.card n * B.det ^ Fintype.card m
have refine : HPow.hPow (α := R)
      (det
        (A.map fun (a : R) ↦
          (((AlgHom.toLinearMap (Algebra.lmul ℕ R) : (a : R) → R →ₗ[ℕ] R) a : R →ₗ[ℕ] R) : (a : R) → R) 1))
      (Fintype.card n) *
    HPow.hPow (α := R)
      (det (B.map fun (b : R) ↦ ((AlgHom.toLinearMap (Algebra.lmul ℕ R) : (a : R) → R →ₗ[ℕ] R) 1 : (a : R) → R) b))
      (Fintype.card m) =
  A.det ^ Fintype.card n * B.det ^ Fintype.card m
Tactic: refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommMagma R
inst_1 : StarMul R
x : Matrix l m R
y : Matrix n p R
⊢ Eq (α := Matrix (m × p) (l × n) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) xᴴ yᴴ)
have a : ∀ (i : m × p) (j : l × n),
  Eq (α := R) ((kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ i j) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) xᴴ yᴴ i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Mul R
inst_1 : StarMul R
x : Matrix l m R
y : Matrix n p R
⊢ Eq (α := Matrix (m × p) (l × n) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ
    (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) yᴴ xᴴ) Prod.swap Prod.swap)
have a : ∀ (i : m × p) (j : l × n),
  Eq (α := R) ((kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ i j)
    (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) yᴴ xᴴ) Prod.swap Prod.swap i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : StarRing R
inst_6 : StarAddMonoid α
inst_7 : StarAddMonoid β
inst_8 : StarModule R α
inst_9 : StarModule R β
x : Matrix l m α
y : Matrix n p β
⊢ Eq (α := Matrix (m × p) (l × n) (α ⊗[R] β)) (kroneckerMap (tmul R) x y)ᴴ (kroneckerMap (tmul R) xᴴ yᴴ)
have a : ∀ (i : m × p) (j : l × n), Eq (α := α ⊗[R] β) ((kroneckerMap (tmul R) x y)ᴴ i j) (kroneckerMap (tmul R) xᴴ yᴴ i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ Eq (α := α ⊗[R] β) (det (kroneckerMap (tmul R) A B)) ((A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m))
have refine : HPow.hPow (α := α ⊗[R] β)
      (det
        (A.map fun (a : α) ↦ (((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) a : β →ₗ[R] α ⊗[R] β) : (a : β) → α ⊗[R] β) 1))
      (Fintype.card n) *
    HPow.hPow (α := α ⊗[R] β)
      (det (B.map fun (b : β) ↦ ((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) 1 : (a : β) → α ⊗[R] β) b)) (Fintype.card m) =
  (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
Tactic: refine (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ HPow.hPow (α := α ⊗[R] β)
        (det
          (A.map fun (a : α) ↦ (((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) a : β →ₗ[R] α ⊗[R] β) : (a : β) → α ⊗[R] β) 1))
        (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β)
        (det (B.map fun (b : β) ↦ ((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) 1 : (a : β) → α ⊗[R] β) b))
        (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
have simp : HPow.hPow (α := α ⊗[R] β) (det (A.map fun (a : α) ↦ (includeLeft : (a : α) → α ⊗[R] β) a)) (Fintype.card n) *
    HPow.hPow (α := α ⊗[R] β) (det (B.map fun (b : β) ↦ (includeRight : (a : β) → α ⊗[R] β) b)) (Fintype.card m) =
  (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
Tactic: simp -eta only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ HPow.hPow (α := α ⊗[R] β) (det (A.map fun (a : α) ↦ (includeLeft : (a : α) → α ⊗[R] β) a)) (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β) (det (B.map fun (b : β) ↦ (includeRight : (a : β) → α ⊗[R] β) b)) (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
have simp : HPow.hPow (α := α ⊗[R] β) ((includeLeft : (a : α) → α ⊗[R] β) A.det : α ⊗[R] β) (Fintype.card n) *
    HPow.hPow (α := α ⊗[R] β) ((includeRight : (a : β) → α ⊗[R] β) B.det : α ⊗[R] β) (Fintype.card m) =
  (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
Tactic: simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
⊢ Eq.{u_3 + 1} (α := M) (∑ x : ι, (N₁ * N₂) i x • v x)
    (∑ x : ι, HSMul.hSMul (β := M) (N₁ i x) (∑ x_1 : ι, N₂ x x_1 • v x_1))
have simp_rw : Eq.{u_3 + 1} (α := M) (∑ x : ι, ∑ x_1 : ι, N₁ i x_1 • N₂ x_1 x • v x) (∑ x : ι, ∑ x_1 : ι, N₁ i x • N₂ x x_1 • v x_1)
Tactic: simp_rw [mul_apply, Finset.smul_sum, Finset.sum_smul, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
⊢ Eq.{u_3 + 1} (α := M) (∑ x : ι, ∑ x_1 : ι, N₁ i x_1 • N₂ x_1 x • v x) (∑ x : ι, ∑ x_1 : ι, N₁ i x • N₂ x x_1 • v x_1)
have rw : Eq.{u_3 + 1} (α := M) (∑ y : ι, ∑ x : ι, N₁ i y • N₂ y x • v x) (∑ x : ι, ∑ x_1 : ι, N₁ i x • N₂ x x_1 • v x_1)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Matrix ι ι R
v : ι → M
⊢ N • v = ∑ j : ι, fun (i : ι) ↦ N i j • v j
have h : ∀ (x : ι), (N • v) x = (∑ j : ι, fun (i : ι) ↦ N i j • v j) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
⊢ single i j r • v = Pi.single (M := fun (j : ι) ↦ M) i (r • v j)
have h : ∀ (i' : ι), (single i j r • v) i' = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
Tactic: ext i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
⊢ Eq.{u_3 + 1} (α := M) (∑ j_1 : ι, single i j r i' j_1 • v j_1 : M)
    (Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i' : M)
have h : single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
Tactic: rw [Fintype.sum_eq_single j fun j' hj => ?_]