[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M N : Matrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M N : Matrix m n α
h : ∀ (i : m), M i = N i
i : m
⊢ ∀ (j : n), M i j = N i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
⊢ map M id = M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
x✝ : n
⊢ map M id i✝ x✝ = M i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β✝ : Type w
γ✝ : Type u_9
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
⊢ map (map M f) g = map M (g ∘ f)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β✝ : Type w
γ✝ : Type u_9
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
i✝ : m
x✝ : n
⊢ map (map M f) g i✝ x✝ = map M (g ∘ f) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
⊢ map 0 f = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
i✝ : m
x✝ : n
⊢ map 0 f i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty m
M N : Matrix m n α
⊢ M = N
[PROOFSTEP]
ext i
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty m
M N : Matrix m n α
i : m
x✝ : n
⊢ M i x✝ = N i x✝
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty n
M N : Matrix m n α
⊢ M = N
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty n
M N : Matrix m n α
i : m
j : n
⊢ M i j = N i j
[PROOFSTEP]
exact isEmptyElim j
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i : n
⊢ diagonal d i i = d i
[PROOFSTEP]
simp [diagonal]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i j : n
h : i ≠ j
⊢ diagonal d i j = 0
[PROOFSTEP]
simp [diagonal, h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i
[PROOFSTEP]
simpa using congr_arg (fun m : Matrix n n α => m i i) h
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : ∀ (i : n), d₁ i = d₂ i
⊢ diagonal d₁ = diagonal d₂
[PROOFSTEP]
rw [show d₁ = d₂ from funext h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i
[PROOFSTEP]
simpa using Matrix.ext_iff.mpr h i i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
⊢ (diagonal fun x => 0) = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
i✝ x✝ : n
⊢ diagonal (fun x => 0) i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp [diagonal]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
⊢ (diagonal v)ᵀ = diagonal v
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
[PROOFSTEP]
simp [h, transpose]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
[PROOFSTEP]
simp [h, transpose, diagonal_apply_ne' _ h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
⊢ diagonal d₁ + diagonal d₂ = diagonal fun i => d₁ i + d₂ i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
⊢ diagonal (r • d) = r • diagonal d
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
i j : n
h : i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
i j : n
h : ¬i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
⊢ map (diagonal d) f = diagonal fun m => f (d m)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ x✝ : n
⊢ map (diagonal d) f i✝ x✝ = diagonal (fun m => f (d m)) i✝ x✝
[PROOFSTEP]
simp only [diagonal_apply, map_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ x✝ : n
⊢ f (if i✝ = x✝ then d i✝ else 0) = if i✝ = x✝ then f (d i✝) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ x✝ : n
h✝ : i✝ = x✝
⊢ f (d i✝) = f (d i✝)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ x✝ : n
h✝ : ¬i✝ = x✝
⊢ f 0 = 0
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᴴ = diagonal (star v)
[PROOFSTEP]
rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal fun m => star (v m)) = diagonal (star v)
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
⊢ map 1 f = 1
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
⊢ map 1 f i✝ x✝ = OfNat.ofNat 1 i✝ x✝
[PROOFSTEP]
simp only [one_apply, map_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
⊢ f (if i✝ = x✝ then 1 else 0) = if i✝ = x✝ then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
h✝ : i✝ = x✝
⊢ f 1 = 1
[PROOFSTEP]
simp [h₀, h₁]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
h✝ : ¬i✝ = x✝
⊢ f 0 = 0
[PROOFSTEP]
simp [h₀, h₁]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ OfNat.ofNat 1 i j = Pi.single i 1 j
[PROOFSTEP]
simp only [one_apply, Pi.single_apply, eq_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i j : n
⊢ bit1 M i j = if i = j then bit1 (M i j) else bit0 (M i j)
[PROOFSTEP]
dsimp [bit1]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i j : n
⊢ bit0 (M i j) + OfNat.ofNat 1 i j = if i = j then bit0 (M i j) + 1 else bit0 (M i j)
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i j : n
h : i = j
⊢ bit0 (M i j) + OfNat.ofNat 1 i j = if i = j then bit0 (M i j) + 1 else bit0 (M i j)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i j : n
h : ¬i = j
⊢ bit0 (M i j) + OfNat.ofNat 1 i j = if i = j then bit0 (M i j) + 1 else bit0 (M i j)
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i : n
⊢ bit1 M i i = bit1 (M i i)
[PROOFSTEP]
simp [bit1_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i j : n
h : i ≠ j
⊢ bit1 M i j = bit0 (M i j)
[PROOFSTEP]
simp [bit1_apply, h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSemiring α
u : m → α
w : n → α
v : Matrix m n α
⊢ (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w
[PROOFSTEP]
simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : CommSemigroup α
v w : m → α
⊢ v ⬝ᵥ w = w ⬝ᵥ v
[PROOFSTEP]
simp_rw [dotProduct, mul_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
v w : PUnit → α
⊢ v ⬝ᵥ w = v PUnit.unit * w PUnit.unit
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : MulOneClass α
inst✝ : AddCommMonoid α
v : n → α
⊢ v ⬝ᵥ 1 = ∑ i : n, v i
[PROOFSTEP]
simp [(· ⬝ᵥ ·)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : MulOneClass α
inst✝ : AddCommMonoid α
v : n → α
⊢ 1 ⬝ᵥ v = ∑ i : n, v i
[PROOFSTEP]
simp [(· ⬝ᵥ ·)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ v ⬝ᵥ 0 = 0
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ 0 ⬝ᵥ v = 0
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
[PROOFSTEP]
simp [dotProduct, add_mul, Finset.sum_add_distrib]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w
[PROOFSTEP]
simp [dotProduct, mul_add, Finset.sum_add_distrib]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
e : m ≃ n
x✝¹ : m
x✝ : x✝¹ ∈ Finset.univ
⊢ (u ∘ ↑e.symm) (↑e x✝¹) * x (↑e x✝¹) = u x✝¹ * (x ∘ ↑e) x✝¹
[PROOFSTEP]
simp only [Function.comp, Equiv.symm_apply_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
e : n ≃ m
⊢ u ⬝ᵥ x ∘ ↑e.symm = u ∘ ↑e ⬝ᵥ x
[PROOFSTEP]
simpa only [Equiv.symm_symm] using (comp_equiv_symm_dotProduct u x e.symm).symm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
e : m ≃ n
⊢ x ∘ ↑e ⬝ᵥ y ∘ ↑e = x ⬝ᵥ y
[PROOFSTEP]
rw [← dotProduct_comp_equiv_symm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
e : m ≃ n
⊢ x ⬝ᵥ (y ∘ ↑e) ∘ ↑e.symm = x ⬝ᵥ y
[PROOFSTEP]
simp only [Function.comp, Equiv.apply_symm_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
⊢ diagonal v i ⬝ᵥ w = v i * w i
[PROOFSTEP]
have : ∀ (j) (_ : j ≠ i), diagonal v i j * w j = 0 := fun j hij => by simp [diagonal_apply_ne' _ hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i j : m
hij : j ≠ i
⊢ diagonal v i j * w j = 0
[PROOFSTEP]
simp [diagonal_apply_ne' _ hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ diagonal v i ⬝ᵥ w = v i * w i
[PROOFSTEP]
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1
[GOAL]
case h.e'_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ v i * w i = diagonal v i i * w i
[PROOFSTEP]
simp
[GOAL]
case convert_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ ¬i ∈ Finset.univ → diagonal v i i * w i = 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
⊢ v ⬝ᵥ diagonal w i = v i * w i
[PROOFSTEP]
have : ∀ (j) (_ : j ≠ i), v j * diagonal w i j = 0 := fun j hij => by simp [diagonal_apply_ne' _ hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i j : m
hij : j ≠ i
⊢ v j * diagonal w i j = 0
[PROOFSTEP]
simp [diagonal_apply_ne' _ hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i
[PROOFSTEP]
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1
[GOAL]
case h.e'_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v i * w i = v i * diagonal w i i
[PROOFSTEP]
simp
[GOAL]
case convert_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ ¬i ∈ Finset.univ → v i * diagonal w i i = 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
⊢ (v ⬝ᵥ fun j => diagonal w j i) = v i * w i
[PROOFSTEP]
have : ∀ (j) (_ : j ≠ i), v j * diagonal w j i = 0 := fun j hij => by simp [diagonal_apply_ne _ hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i j : m
hij : j ≠ i
⊢ v j * diagonal w j i = 0
[PROOFSTEP]
simp [diagonal_apply_ne _ hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ (v ⬝ᵥ fun j => diagonal w j i) = v i * w i
[PROOFSTEP]
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1
[GOAL]
case h.e'_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ v i * w i = v i * diagonal w i i
[PROOFSTEP]
simp
[GOAL]
case convert_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ ¬i ∈ Finset.univ → v i * diagonal w i i = 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
⊢ Pi.single i x ⬝ᵥ v = x * v i
[PROOFSTEP]
have : ∀ (j) (_ : j ≠ i), Pi.single (f := fun _ => α) i x j * v j = 0 := fun j hij => by simp [Pi.single_eq_of_ne hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i j : m
hij : j ≠ i
⊢ Pi.single i x j * v j = 0
[PROOFSTEP]
simp [Pi.single_eq_of_ne hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ Pi.single i x ⬝ᵥ v = x * v i
[PROOFSTEP]
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1
[GOAL]
case h.e'_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ x * v i = Pi.single i x i * v i
[PROOFSTEP]
simp
[GOAL]
case convert_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ ¬i ∈ Finset.univ → Pi.single i x i * v i = 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
⊢ v ⬝ᵥ Pi.single i x = v i * x
[PROOFSTEP]
have : ∀ (j) (_ : j ≠ i), v j * Pi.single (f := fun _ => α) i x j = 0 := fun j hij => by simp [Pi.single_eq_of_ne hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i j : m
hij : j ≠ i
⊢ v j * Pi.single i x j = 0
[PROOFSTEP]
simp [Pi.single_eq_of_ne hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ v ⬝ᵥ Pi.single i x = v i * x
[PROOFSTEP]
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1
[GOAL]
case h.e'_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ v i * x = v i * Pi.single i x i
[PROOFSTEP]
simp
[GOAL]
case convert_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ ¬i ∈ Finset.univ → v i * Pi.single i x i = 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
⊢ 1 ⬝ᵥ 1 = ↑(Fintype.card n)
[PROOFSTEP]
simp [dotProduct, Fintype.card]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocRing α
u v w : m → α
⊢ -v ⬝ᵥ w = -(v ⬝ᵥ w)
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocRing α
u v w : m → α
⊢ v ⬝ᵥ -w = -(v ⬝ᵥ w)
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocRing α
u v w : m → α
⊢ (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocRing α
u v w : m → α
⊢ u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Monoid R
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
x : R
v w : m → α
⊢ x • v ⬝ᵥ w = x • (v ⬝ᵥ w)
[PROOFSTEP]
simp [dotProduct, Finset.smul_sum, smul_mul_assoc]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Monoid R
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
x : R
v w : m → α
⊢ v ⬝ᵥ x • w = x • (v ⬝ᵥ w)
[PROOFSTEP]
simp [dotProduct, Finset.smul_sum, mul_smul_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ star w = star (w ⬝ᵥ v)
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ w = star (star w ⬝ᵥ v)
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ v ⬝ᵥ star w = star (w ⬝ᵥ star v)
[PROOFSTEP]
simp [dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
[PROOFSTEP]
refine ⟨?_, ?_, ?_, ?_⟩
[GOAL]
case refine_1
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0
[PROOFSTEP]
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
[GOAL]
case refine_1
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x in Finset.range 0, if h : x < 2 then A 0 { val := x, isLt := h } * B { val := x, isLt := h } 0 else 0) +
        if h : 0 < 2 then A 0 { val := 0, isLt := h } * B { val := 0, isLt := h } 0 else 0) +
      if h : 1 < 2 then A 0 { val := 1, isLt := h } * B { val := 1, isLt := h } 0 else 0) =
    A 0 0 * B 0 0 + A 0 1 * B 1 0
[PROOFSTEP]
simp
[GOAL]
case refine_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1
[PROOFSTEP]
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
[GOAL]
case refine_2
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x in Finset.range 0, if h : x < 2 then A 0 { val := x, isLt := h } * B { val := x, isLt := h } 1 else 0) +
        if h : 0 < 2 then A 0 { val := 0, isLt := h } * B { val := 0, isLt := h } 1 else 0) +
      if h : 1 < 2 then A 0 { val := 1, isLt := h } * B { val := 1, isLt := h } 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1
[PROOFSTEP]
simp
[GOAL]
case refine_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0
[PROOFSTEP]
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
[GOAL]
case refine_3
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x in Finset.range 0, if h : x < 2 then A 1 { val := x, isLt := h } * B { val := x, isLt := h } 0 else 0) +
        if h : 0 < 2 then A 1 { val := 0, isLt := h } * B { val := 0, isLt := h } 0 else 0) +
      if h : 1 < 2 then A 1 { val := 1, isLt := h } * B { val := 1, isLt := h } 0 else 0) =
    A 1 0 * B 0 0 + A 1 1 * B 1 0
[PROOFSTEP]
simp
[GOAL]
case refine_4
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
[PROOFSTEP]
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
[GOAL]
case refine_4
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x in Finset.range 0, if h : x < 2 then A 1 { val := x, isLt := h } * B { val := x, isLt := h } 1 else 0) +
        if h : 0 < 2 then A 1 { val := 0, isLt := h } * B { val := 0, isLt := h } 1 else 0) +
      if h : 1 < 2 then A 1 { val := 1, isLt := h } * B { val := 1, isLt := h } 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
⊢ a • M * N = a • (M * N)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i✝ : m
x✝ : l
⊢ (a • M * N) i✝ x✝ = (a • (M * N)) i✝ x✝
[PROOFSTEP]
apply smul_dotProduct a
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
⊢ M * a • N = a • (M * N)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
i✝ : m
x✝ : l
⊢ (M * a • N) i✝ x✝ = (a • (M * N)) i✝ x✝
[PROOFSTEP]
apply dotProduct_smul
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
⊢ M * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
i✝ : m
x✝ : o
⊢ (M * 0) i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
apply dotProduct_zero
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
⊢ 0 * M = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
i✝ : l
x✝ : n
⊢ (0 * M) i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
apply zero_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L * (M + N) = L * M + L * N
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
x✝ : o
⊢ (L * (M + N)) i✝ x✝ = (L * M + L * N) i✝ x✝
[PROOFSTEP]
apply dotProduct_add
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
⊢ (L + M) * N = L * N + M * N
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
i✝ : l
x✝ : n
⊢ ((L + M) * N) i✝ x✝ = (L * N + M * N) i✝ x✝
[PROOFSTEP]
apply add_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * diagonal d) i j = M i j * d j
[PROOFSTEP]
rw [← diagonal_transpose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * (diagonal d)ᵀ) i j = M i j * d j
[PROOFSTEP]
apply dotProduct_diagonal
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
⊢ a • M = (diagonal fun x => a) * M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
i✝ : m
x✝ : n
⊢ (a • M) i✝ x✝ = ((diagonal fun x => a) * M) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : NonUnitalNonAssocSemiring α
a b : n → α
⊢ diag (col a * row b) = a * b
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : NonUnitalNonAssocSemiring α
a b : n → α
x✝ : n
⊢ diag (col a * row b) x✝ = (a * b) x✝
[PROOFSTEP]
simp [Matrix.mul_apply, col, row]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
⊢ 1 * M = M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
x✝ : n
⊢ (1 * M) i✝ x✝ = M i✝ x✝
[PROOFSTEP]
rw [← diagonal_one, diagonal_mul, one_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
⊢ M * 1 = M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
x✝ : n
⊢ (M * 1) i✝ x✝ = M i✝ x✝
[PROOFSTEP]
rw [← diagonal_one, mul_diagonal, mul_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
src✝ : NonUnitalNonAssocSemiring (Matrix n n α) := nonUnitalNonAssocSemiring
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
src✝ : NonUnitalNonAssocSemiring (Matrix n n α) := nonUnitalNonAssocSemiring
i✝ x✝ : n
⊢ NatCast.natCast 0 i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
src✝ : NonUnitalNonAssocSemiring (Matrix n✝ n✝ α) := nonUnitalNonAssocSemiring
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
src✝ : NonUnitalNonAssocSemiring (Matrix n✝ n✝ α) := nonUnitalNonAssocSemiring
n : ℕ
i j : n✝
⊢ NatCast.natCast (n + 1) i j = (NatCast.natCast n + 1) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
src✝ : NonUnitalNonAssocSemiring (Matrix n✝ n✝ α) := nonUnitalNonAssocSemiring
n : ℕ
i j : n✝
⊢ NatCast.natCast (n + 1) i j = (NatCast.natCast n + 1) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
src✝ : NonUnitalNonAssocSemiring (Matrix n✝ n✝ α) := nonUnitalNonAssocSemiring
n : ℕ
i j : n✝
h : i = j
⊢ NatCast.natCast (n + 1) i j = (NatCast.natCast n + 1) i j
[PROOFSTEP]
simp [Nat.cast, *]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
src✝ : NonUnitalNonAssocSemiring (Matrix n✝ n✝ α) := nonUnitalNonAssocSemiring
n : ℕ
i j : n✝
h : ¬i = j
⊢ NatCast.natCast (n + 1) i j = (NatCast.natCast n + 1) i j
[PROOFSTEP]
simp [Nat.cast, *]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
⊢ map (L * M) ↑f = map L ↑f * map M ↑f
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
i✝ : m
x✝ : o
⊢ map (L * M) (↑f) i✝ x✝ = (map L ↑f * map M ↑f) i✝ x✝
[PROOFSTEP]
simp [mul_apply, map_sum]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
⊢ L * M * N = L * (M * N)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
i✝ : l
x✝ : o
⊢ (L * M * N) i✝ x✝ = (L * (M * N)) i✝ x✝
[PROOFSTEP]
apply dotProduct_assoc
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ -M * N = -(M * N)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
x✝ : o
⊢ (-M * N) i✝ x✝ = (-(M * N)) i✝ x✝
[PROOFSTEP]
apply neg_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ M * -N = -(M * N)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
x✝ : o
⊢ (M * -N) i✝ x✝ = (-(M * N)) i✝ x✝
[PROOFSTEP]
apply dotProduct_neg
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') * N = M * N - M' * N
[PROOFSTEP]
rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N - N') = M * N - M * N'
[PROOFSTEP]
rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]
[GOAL]
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Semiring α
n : Type u
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : (fun x => α →+ Matrix n n α) 1 := ↑(AddMonoidHom.flip (smulAddHom α (Matrix n n α))) 1
⊢ (fun a => a • 1) 1 = 1
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Semiring α
n : Type u
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : (fun x => α →+ Matrix n n α) 1 := ↑(AddMonoidHom.flip (smulAddHom α (Matrix n n α))) 1
⊢ ∀ (x y : α),
    OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } x *
        OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } y
[PROOFSTEP]
intros
[GOAL]
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Semiring α
n : Type u
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : (fun x => α →+ Matrix n n α) 1 := ↑(AddMonoidHom.flip (smulAddHom α (Matrix n n α))) 1
x✝ y✝ : α
⊢ OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } x✝ *
      OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } y✝
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Semiring α
n : Type u
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : (fun x => α →+ Matrix n n α) 1 := ↑(AddMonoidHom.flip (smulAddHom α (Matrix n n α))) 1
x✝¹ y✝ : α
i✝ x✝ : n
⊢ OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } (x✝¹ * y✝) i✝ x✝ =
    (OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } x✝¹ *
        OneHom.toFun { toFun := fun a => a • 1, map_one' := (_ : 1 • 1 = 1) } y✝)
      i✝ x✝
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Semiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : α
i : n
⊢ ↑(scalar n) a i i = a
[PROOFSTEP]
simp only [coe_scalar, Matrix.smul_apply, one_apply_eq, smul_eq_mul, mul_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Semiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : α
i j : n
h : i ≠ j
⊢ ↑(scalar n) a i j = 0
[PROOFSTEP]
simp only [h, coe_scalar, one_apply_ne, Ne.def, not_false_iff, Matrix.smul_apply, smul_zero]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ ↑(scalar n) r = ↑(scalar n) s ↔ r = s
[PROOFSTEP]
constructor
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ ↑(scalar n) r = ↑(scalar n) s → r = s
[PROOFSTEP]
intro h
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
h : ↑(scalar n) r = ↑(scalar n) s
⊢ r = s
[PROOFSTEP]
inhabit n
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
h : ↑(scalar n) r = ↑(scalar n) s
inhabited_h : Inhabited n
⊢ r = s
[PROOFSTEP]
rw [← scalar_apply_eq r (Inhabited.default (α := n)), ← scalar_apply_eq s (Inhabited.default (α := n)), h]
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ r = s → ↑(scalar n) r = ↑(scalar n) s
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r : α
⊢ ↑(scalar n) r = ↑(scalar n) r
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ a • M = M * diagonal fun x => a
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
x✝ : n
⊢ (a • M) i✝ x✝ = (M * diagonal fun x => a) i✝ x✝
[PROOFSTEP]
simp [mul_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : α
M : Matrix n n α
⊢ Commute (↑(scalar n) r) M
[PROOFSTEP]
simp [Commute, SemiconjBy]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
src✝ : R →+* Matrix n n α := RingHom.comp (scalar n) (algebraMap R α)
r : R
x : (fun x => Matrix n n α) r
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      x =
    x *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
src✝ : R →+* Matrix n n α := RingHom.comp (scalar n) (algebraMap R α)
r : R
x : (fun x => Matrix n n α) r
i✝ x✝ : n
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x)
      i✝ x✝ =
    (x *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r)
      i✝ x✝
[PROOFSTEP]
simp [Matrix.scalar, Matrix.mul_apply, Matrix.one_apply, Algebra.commutes, smul_ite]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
src✝ : R →+* Matrix n n α := RingHom.comp (scalar n) (algebraMap R α)
r : R
x : (fun x => Matrix n n α) r
⊢ r • x =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      x
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
src✝ : R →+* Matrix n n α := RingHom.comp (scalar n) (algebraMap R α)
r : R
x : (fun x => Matrix n n α) r
i✝ x✝ : n
⊢ (r • x) i✝ x✝ =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x)
      i✝ x✝
[PROOFSTEP]
simp [Matrix.scalar, Algebra.smul_def r]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
⊢ ↑(algebraMap R (Matrix n n α)) r i j = if i = j then ↑(algebraMap R α) r else 0
[PROOFSTEP]
dsimp [algebraMap, Algebra.toRingHom, Matrix.scalar]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
⊢ ↑Algebra.toRingHom r * OfNat.ofNat 1 i j = if i = j then ↑Algebra.toRingHom r else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
h : i = j
⊢ ↑Algebra.toRingHom r * OfNat.ofNat 1 i j = ↑Algebra.toRingHom r
[PROOFSTEP]
simp [h, Matrix.one_apply_ne]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
h : ¬i = j
⊢ ↑Algebra.toRingHom r * OfNat.ofNat 1 i j = 0
[PROOFSTEP]
simp [h, Matrix.one_apply_ne]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ map (↑(algebraMap R (Matrix n n α)) r) f = ↑(algebraMap R (Matrix n n β)) r
[PROOFSTEP]
rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]
  -- Porting note: (congr) the remaining proof was
    -- ```
    -- congr 1
    -- simp only [hf₂, Pi.algebraMap_apply]
    -- ```
    -- But some `congr 1` doesn't quite work.
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ (diagonal fun m => f (↑(algebraMap R (n → α)) r m)) = diagonal (↑(algebraMap R (n → β)) r)
[PROOFSTEP]
simp only [Pi.algebraMap_apply, diagonal_eq_diagonal_iff]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ n → f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
[PROOFSTEP]
intro
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
i✝ : n
⊢ f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
[PROOFSTEP]
rw [hf₂]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NonAssocSemiring α
inst✝¹ : NonAssocSemiring β
inst✝ : NonAssocSemiring γ
f : α →+* β
src✝ : Matrix m m α →+ Matrix m m β := AddMonoidHom.mapMatrix (toAddMonoidHom f)
⊢ (fun M => map M ↑f) 1 = 1
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
⊢ vecMulVec w v = col w * row v
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
i✝ : m
x✝ : n
⊢ vecMulVec w v i✝ x✝ = (col w * row v) i✝ x✝
[PROOFSTEP]
simp only [vecMulVec, mul_apply, Fintype.univ_punit, Finset.sum_singleton]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
i✝ : m
x✝ : n
⊢ ↑of (fun x y => w x * v y) i✝ x✝ = col w i✝ PUnit.unit * row v PUnit.unit x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
⊢ (fun M => mulVec M v) 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x✝ : m
⊢ (fun M => mulVec M v) 0 x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
simp [mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x y : Matrix m n α
⊢ ZeroHom.toFun { toFun := fun M => mulVec M v, map_zero' := (_ : (fun M => mulVec M v) 0 = 0) } (x + y) =
    ZeroHom.toFun { toFun := fun M => mulVec M v, map_zero' := (_ : (fun M => mulVec M v) 0 = 0) } x +
      ZeroHom.toFun { toFun := fun M => mulVec M v, map_zero' := (_ : (fun M => mulVec M v) 0 = 0) } y
[PROOFSTEP]
ext m
[GOAL]
case h
l : Type u_1
m✝ : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x y : Matrix m✝ n α
m : m✝
⊢ ZeroHom.toFun { toFun := fun M => mulVec M v, map_zero' := (_ : (fun M => mulVec M v) 0 = 0) } (x + y) m =
    (ZeroHom.toFun { toFun := fun M => mulVec M v, map_zero' := (_ : (fun M => mulVec M v) 0 = 0) } x +
        ZeroHom.toFun { toFun := fun M => mulVec M v, map_zero' := (_ : (fun M => mulVec M v) 0 = 0) } y)
      m
[PROOFSTEP]
apply add_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ mulVec A w = vecMul v A ⬝ᵥ w
[PROOFSTEP]
simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x : m, ∑ x_1 : n, v x * (A x x_1 * w x_1) = ∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x)
[PROOFSTEP]
exact Finset.sum_comm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ mulVec A 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ mulVec A 0 x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
simp [mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ vecMul 0 A = 0
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ vecMul 0 A x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
simp [vecMul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
⊢ mulVec 0 v = 0
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x✝ : m
⊢ mulVec 0 v x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
simp [mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
⊢ vecMul v 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
x✝ : n
⊢ vecMul v 0 x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
simp [vecMul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
A : Matrix m n α
b : n → α
⊢ mulVec (a • A) b = a • mulVec A b
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
A : Matrix m n α
b : n → α
x✝ : m
⊢ mulVec (a • A) b x✝ = (a • mulVec A b) x✝
[PROOFSTEP]
apply smul_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
⊢ mulVec A (x + y) = mulVec A x + mulVec A y
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ mulVec A (x + y) x✝ = (mulVec A x + mulVec A y) x✝
[PROOFSTEP]
apply dotProduct_add
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ mulVec (A + B) x = mulVec A x + mulVec B x
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
x✝ : m
⊢ mulVec (A + B) x x✝ = (mulVec A x + mulVec B x) x✝
[PROOFSTEP]
apply add_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ vecMul x (A + B) = vecMul x A + vecMul x B
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
x✝ : n
⊢ vecMul x (A + B) x✝ = (vecMul x A + vecMul x B) x✝
[PROOFSTEP]
apply dotProduct_add
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
⊢ vecMul (x + y) A = vecMul x A + vecMul y A
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ vecMul (x + y) A x✝ = (vecMul x A + vecMul y A) x✝
[PROOFSTEP]
apply add_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : IsScalarTower R S S
M : Matrix n m S
b : R
v : n → S
⊢ vecMul (b • v) M = b • vecMul v M
[PROOFSTEP]
ext i
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : IsScalarTower R S S
M : Matrix n m S
b : R
v : n → S
i : m
⊢ vecMul (b • v) M i = (b • vecMul v M) i
[PROOFSTEP]
simp only [vecMul, dotProduct, Finset.smul_sum, Pi.smul_apply, smul_mul_assoc]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
⊢ mulVec M (b • v) = b • mulVec M v
[PROOFSTEP]
ext i
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
i : m
⊢ mulVec M (b • v) i = (b • mulVec M v) i
[PROOFSTEP]
simp only [mulVec, dotProduct, Finset.smul_sum, Pi.smul_apply, mul_smul_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ mulVec (diagonal v) (Pi.single j x) = Pi.single j (v j * x)
[PROOFSTEP]
ext i
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ mulVec (diagonal v) (Pi.single j x) i = Pi.single j (v j * x) i
[PROOFSTEP]
rw [mulVec_diagonal]
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i
[PROOFSTEP]
exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ vecMul (Pi.single j x) (diagonal v) = Pi.single j (x * v j)
[PROOFSTEP]
ext i
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ vecMul (Pi.single j x) (diagonal v) i = Pi.single j (x * v j) i
[PROOFSTEP]
rw [vecMul_diagonal]
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i
[PROOFSTEP]
exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
⊢ vecMul (vecMul v M) N = vecMul v (M * N)
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x✝ : o
⊢ vecMul (vecMul v M) N x✝ = vecMul v (M * N) x✝
[PROOFSTEP]
apply dotProduct_assoc
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
⊢ mulVec M (mulVec N v) = mulVec (M * N) v
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ mulVec M (mulVec N v) x✝ = mulVec (M * N) v x✝
[PROOFSTEP]
symm
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ mulVec (M * N) v x✝ = mulVec M (mulVec N v) x✝
[PROOFSTEP]
apply dotProduct_assoc
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * B * C) i j = A i ⬝ᵥ mulVec B (Cᵀ j)
[PROOFSTEP]
rw [Matrix.mul_assoc]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * (B * C)) i j = A i ⬝ᵥ mulVec B (Cᵀ j)
[PROOFSTEP]
simp only [mul_apply, dotProduct, mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ ∑ x : n, A i x * ∑ j_1 : n, B x j_1 * C j_1 j = ∑ x : n, A i x * ∑ x_1 : n, B x x_1 * Cᵀ j x_1
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ mulVec A 1 = fun i => ∑ j : n, A i j
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ mulVec A 1 x✝ = ∑ j : n, A x✝ j
[PROOFSTEP]
simp [mulVec, dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ vecMul 1 A = fun j => ∑ i : m, A i j
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ vecMul 1 A x✝ = ∑ i : m, A i x✝
[PROOFSTEP]
simp [vecMul, dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
v : m → α
⊢ mulVec 1 v = v
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ mulVec 1 v x✝ = v x✝
[PROOFSTEP]
rw [← diagonal_one, mulVec_diagonal, one_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
v : m → α
⊢ vecMul v 1 = v
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : NonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ vecMul v 1 x✝ = v x✝
[PROOFSTEP]
rw [← diagonal_one, vecMul_diagonal, mul_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ vecMul (-v) A = -vecMul v A
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ vecMul (-v) A x✝ = (-vecMul v A) x✝
[PROOFSTEP]
apply neg_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ vecMul v (-A) = -vecMul v A
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ vecMul v (-A) x✝ = (-vecMul v A) x✝
[PROOFSTEP]
apply dotProduct_neg
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ mulVec (-A) v = -mulVec A v
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ mulVec (-A) v x✝ = (-mulVec A v) x✝
[PROOFSTEP]
apply neg_dotProduct
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ mulVec A (-v) = -mulVec A v
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ mulVec A (-v) x✝ = (-mulVec A v) x✝
[PROOFSTEP]
apply dotProduct_neg
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ mulVec (A - B) x = mulVec A x - mulVec B x
[PROOFSTEP]
simp [sub_eq_add_neg, add_mulVec, neg_mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ vecMul x (A - B) = vecMul x A - vecMul x B
[PROOFSTEP]
simp [sub_eq_add_neg, vecMul_add, vecMul_neg]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
⊢ mulVec Aᵀ x = vecMul x A
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
x✝ : n
⊢ mulVec Aᵀ x x✝ = vecMul x A x✝
[PROOFSTEP]
apply dotProduct_comm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
⊢ vecMul x Aᵀ = mulVec A x
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
x✝ : m
⊢ vecMul x Aᵀ x✝ = mulVec A x x✝
[PROOFSTEP]
apply dotProduct_comm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ mulVec A (vecMul x B) = mulVec (A * Bᵀ) x
[PROOFSTEP]
rw [← mulVec_mulVec, mulVec_transpose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
⊢ vecMul (mulVec A x) B = vecMul x (Aᵀ * B)
[PROOFSTEP]
rw [← vecMul_vecMul, vecMul_transpose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : CommSemiring α
inst✝ : Fintype n
A : Matrix m n α
b : n → α
a : α
⊢ mulVec A (a • b) = a • mulVec A b
[PROOFSTEP]
ext
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : CommSemiring α
inst✝ : Fintype n
A : Matrix m n α
b : n → α
a : α
x✝ : m
⊢ mulVec A (a • b) x✝ = (a • mulVec A b) x✝
[PROOFSTEP]
apply dotProduct_smul
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
⊢ Mᵀᵀ = M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
x✝ : n
⊢ Mᵀᵀ i✝ x✝ = M i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Zero α
⊢ 0ᵀ = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Zero α
i✝ : n
x✝ : m
⊢ 0ᵀ i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ 1ᵀ = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ 1ᵀ i j = OfNat.ofNat 1 i j
[PROOFSTEP]
rw [transpose_apply, ← diagonal_one]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
h : i = j
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
[PROOFSTEP]
simp only [h, diagonal_apply_eq]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
h : ¬i = j
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
[PROOFSTEP]
simp only [diagonal_apply_ne _ h, diagonal_apply_ne' _ h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
M : Matrix n n α
⊢ M = 1ᵀ ↔ M = 1
[PROOFSTEP]
rw [transpose_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Add α
M N : Matrix m n α
⊢ (M + N)ᵀ = Mᵀ + Nᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Add α
M N : Matrix m n α
i✝ : n
x✝ : m
⊢ (M + N)ᵀ i✝ x✝ = (Mᵀ + Nᵀ) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Sub α
M N : Matrix m n α
⊢ (M - N)ᵀ = Mᵀ - Nᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Sub α
M N : Matrix m n α
i✝ : n
x✝ : m
⊢ (M - N)ᵀ i✝ x✝ = (Mᵀ - Nᵀ) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : AddCommMonoid α
inst✝¹ : CommSemigroup α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
⊢ (M * N)ᵀ = Nᵀ * Mᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : AddCommMonoid α
inst✝¹ : CommSemigroup α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
i✝ : l
x✝ : m
⊢ (M * N)ᵀ i✝ x✝ = (Nᵀ * Mᵀ) i✝ x✝
[PROOFSTEP]
apply dotProduct_comm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : SMul R α
c : R
M : Matrix m n α
⊢ (c • M)ᵀ = c • Mᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝ : SMul R α
c : R
M : Matrix m n α
i✝ : n
x✝ : m
⊢ (c • M)ᵀ i✝ x✝ = (c • Mᵀ) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Neg α
M : Matrix m n α
⊢ (-M)ᵀ = -Mᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Neg α
M : Matrix m n α
i✝ : n
x✝ : m
⊢ (-M)ᵀ i✝ x✝ = (-Mᵀ) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
f : α → β
M : Matrix m n α
⊢ map Mᵀ f = (map M f)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
f : α → β
M : Matrix m n α
i✝ : n
x✝ : m
⊢ map Mᵀ f i✝ x✝ = (map M f)ᵀ i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Algebra R α
src✝¹ : Matrix m m α ≃+ (Matrix m m α)ᵐᵒᵖ := AddEquiv.trans (transposeAddEquiv m m α) MulOpposite.opAddEquiv
src✝ : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ := transposeRingEquiv m α
r : R
⊢ Equiv.toFun
      { toFun := fun M => MulOpposite.op Mᵀ, invFun := src✝¹.invFun,
        left_inv := (_ : Function.LeftInverse src✝¹.invFun src✝¹.toFun),
        right_inv := (_ : Function.RightInverse src✝¹.invFun src✝¹.toFun) }
      (↑(algebraMap R (Matrix m m α)) r) =
    ↑(algebraMap R (Matrix m m α)ᵐᵒᵖ) r
[PROOFSTEP]
simp only [algebraMap_eq_diagonal, diagonal_transpose, MulOpposite.algebraMap_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : InvolutiveStar α
M : Matrix m n α
⊢ ∀ (i : m) (j : n), Mᴴᴴ i j = M i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
⊢ ∀ (i : n) (j : m), 0ᴴ i j = OfNat.ofNat 0 i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ Mᴴ = 0 ↔ M = 0
[PROOFSTEP]
rw [← conjTranspose_inj (A := M), conjTranspose_zero]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
⊢ 1ᴴ = 1
[PROOFSTEP]
simp [conjTranspose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
M : Matrix n n α
⊢ M = 1ᴴ ↔ M = 1
[PROOFSTEP]
rw [conjTranspose_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M + N)ᴴ i j = (Mᴴ + Nᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M - N)ᴴ i j = (Mᴴ - Nᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : SMul Rᵐᵒᵖ α
c : R
M : Matrix m n α
h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (MulOpposite.op (star c) • Mᴴ) i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Semiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Ring R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module ℚ α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype n
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
M : Matrix m n α
N : Matrix n l α
⊢ ∀ (i : l) (j : m), (M * N)ᴴ i j = (Nᴴ * Mᴴ) i j
[PROOFSTEP]
simp [mul_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (-M)ᴴ i j = (-Mᴴ) i j
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ submatrix (diagonal d) e e i j = diagonal (d ∘ e) i j
[PROOFSTEP]
rw [submatrix_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
[PROOFSTEP]
rw [h, diagonal_apply_eq, diagonal_apply_eq]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = (d ∘ e) j
[PROOFSTEP]
simp only [Function.comp_apply]
  -- Porting note: (simp) added this
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
[PROOFSTEP]
rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
⊢ M * submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
[PROOFSTEP]
cases nonempty_fintype o
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
⊢ M * submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
[PROOFSTEP]
let A := M.submatrix id e₁.symm
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
⊢ M * submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
[PROOFSTEP]
have : M = A.submatrix id e₁ := by
  simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
⊢ M = submatrix A id ↑e₁
[PROOFSTEP]
simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
this : M = submatrix A id ↑e₁
⊢ M * submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
[PROOFSTEP]
rw [this, submatrix_mul_equiv]
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
this : M = submatrix A id ↑e₁
⊢ submatrix (A * 1) id e₂ = submatrix (submatrix A id ↑e₁) id (↑e₁.symm ∘ e₂)
[PROOFSTEP]
simp only [Matrix.mul_one, submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
⊢ submatrix 1 e₁ ↑e₂ * M = submatrix M (↑e₂.symm ∘ e₁) id
[PROOFSTEP]
cases nonempty_fintype o
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
⊢ submatrix 1 e₁ ↑e₂ * M = submatrix M (↑e₂.symm ∘ e₁) id
[PROOFSTEP]
let A := M.submatrix e₂.symm id
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := submatrix M (↑e₂.symm) id
⊢ submatrix 1 e₁ ↑e₂ * M = submatrix M (↑e₂.symm ∘ e₁) id
[PROOFSTEP]
have : M = A.submatrix e₂ id := by
  simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := submatrix M (↑e₂.symm) id
⊢ M = submatrix A (↑e₂) id
[PROOFSTEP]
simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := submatrix M (↑e₂.symm) id
this : M = submatrix A (↑e₂) id
⊢ submatrix 1 e₁ ↑e₂ * M = submatrix M (↑e₂.symm ∘ e₁) id
[PROOFSTEP]
rw [this, submatrix_mul_equiv]
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := submatrix M (↑e₂.symm) id
this : M = submatrix A (↑e₂) id
⊢ submatrix (1 * A) e₁ id = submatrix (submatrix A (↑e₂) id) (↑e₂.symm ∘ e₁) id
[PROOFSTEP]
simp only [Matrix.one_mul, submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ (fun M => submatrix M ↑eₘ ↑eₙ) ((fun M => submatrix M ↑eₘ.symm ↑eₙ.symm) M) = M
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix l o α
⊢ (fun M => submatrix M ↑eₘ.symm ↑eₙ.symm) ((fun M => submatrix M ↑eₘ ↑eₙ) M) = M
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
e : m ≃ n
M : Matrix m n α
⊢ submatrix M id ↑e * submatrix Mᵀ (↑e) id = M * Mᵀ
[PROOFSTEP]
rw [submatrix_mul_equiv, submatrix_id_id]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Add α
v w : m → α
⊢ col (v + w) = col v + col w
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Add α
v w : m → α
i✝ : m
x✝ : Unit
⊢ col (v + w) i✝ x✝ = (col v + col w) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : SMul R α
x : R
v : m → α
⊢ col (x • v) = x • col v
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : SMul R α
x : R
v : m → α
i✝ : m
x✝ : Unit
⊢ col (x • v) i✝ x✝ = (x • col v) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Add α
v w : m → α
⊢ row (v + w) = row v + row w
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Add α
v w : m → α
i✝ : Unit
x✝ : m
⊢ row (v + w) i✝ x✝ = (row v + row w) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : SMul R α
x : R
v : m → α
⊢ row (x • v) = x • row v
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : SMul R α
x : R
v : m → α
i✝ : Unit
x✝ : m
⊢ row (x • v) i✝ x✝ = (x • row v) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
v : m → α
⊢ (col v)ᵀ = row v
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
v : m → α
i✝ : Unit
x✝ : m
⊢ (col v)ᵀ i✝ x✝ = row v i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
v : m → α
⊢ (row v)ᵀ = col v
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
v : m → α
i✝ : m
x✝ : Unit
⊢ (row v)ᵀ i✝ x✝ = col v i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Star α
v : m → α
⊢ (col v)ᴴ = row (star v)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Star α
v : m → α
i✝ : Unit
x✝ : m
⊢ (col v)ᴴ i✝ x✝ = row (star v) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Star α
v : m → α
⊢ (row v)ᴴ = col (star v)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : Star α
v : m → α
i✝ : m
x✝ : Unit
⊢ (row v)ᴴ i✝ x✝ = col (star v) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ row (vecMul v M) = row v * M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : Unit
x✝ : n
⊢ row (vecMul v M) i✝ x✝ = (row v * M) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ col (vecMul v M) = (row v * M)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : n
x✝ : Unit
⊢ col (vecMul v M) i✝ x✝ = (row v * M)ᵀ i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ col (mulVec M v) = M * col v
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : m
x✝ : Unit
⊢ col (mulVec M v) i✝ x✝ = (M * col v) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ row (mulVec M v) = (M * col v)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : Unit
x✝ : m
⊢ row (mulVec M v) i✝ x✝ = (M * col v)ᵀ i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
[PROOFSTEP]
by_cases i' = i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
[PROOFSTEP]
by_cases i' = i
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
[PROOFSTEP]
rw [h, updateRow_self, if_pos rfl]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
[PROOFSTEP]
rw [updateRow_ne h, if_neg h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
[PROOFSTEP]
by_cases j' = j
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
[PROOFSTEP]
by_cases j' = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
[PROOFSTEP]
rw [h, updateColumn_self, if_pos rfl]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
[PROOFSTEP]
rw [updateColumn_ne h, if_neg h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
⊢ updateColumn A i b = submatrix (col b) id (Function.const n ())
[PROOFSTEP]
ext x y
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ updateColumn A i b x y = submatrix (col b) id (Function.const n ()) x y
[PROOFSTEP]
simp [updateColumn_apply, Subsingleton.elim i y]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
⊢ updateRow A i b = submatrix (row b) (Function.const m ()) id
[PROOFSTEP]
ext x y
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ updateRow A i b x y = submatrix (row b) (Function.const m ()) id x y
[PROOFSTEP]
simp [updateColumn_apply, Subsingleton.elim i x]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
⊢ map (updateRow M i b) f = updateRow (map M f) i (f ∘ b)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
x✝ : n
⊢ map (updateRow M i b) f i✝ x✝ = updateRow (map M f) i (f ∘ b) i✝ x✝
[PROOFSTEP]
rw [updateRow_apply, map_apply, map_apply, updateRow_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
x✝ : n
⊢ f (if i✝ = i then b x✝ else M i✝ x✝) = if i✝ = i then (f ∘ b) x✝ else f (M i✝ x✝)
[PROOFSTEP]
exact apply_ite f _ _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
⊢ map (updateColumn M j c) f = updateColumn (map M f) j (f ∘ c)
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
x✝ : n
⊢ map (updateColumn M j c) f i✝ x✝ = updateColumn (map M f) j (f ∘ c) i✝ x✝
[PROOFSTEP]
rw [updateColumn_apply, map_apply, map_apply, updateColumn_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
x✝ : n
⊢ f (if x✝ = j then c i✝ else M i✝ x✝) = if x✝ = j then (f ∘ c) i✝ else f (M i✝ x✝)
[PROOFSTEP]
exact apply_ite f _ _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
⊢ updateRow Mᵀ j c = (updateColumn M j c)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
i✝ : n
x✝ : m
⊢ updateRow Mᵀ j c i✝ x✝ = (updateColumn M j c)ᵀ i✝ x✝
[PROOFSTEP]
rw [transpose_apply, updateRow_apply, updateColumn_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
i✝ : n
x✝ : m
⊢ (if i✝ = j then c x✝ else Mᵀ i✝ x✝) = if i✝ = j then c x✝ else M x✝ i✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
⊢ updateColumn Mᵀ i b = (updateRow M i b)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i✝ : n
x✝ : m
⊢ updateColumn Mᵀ i b i✝ x✝ = (updateRow M i b)ᵀ i✝ x✝
[PROOFSTEP]
rw [transpose_apply, updateRow_apply, updateColumn_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i✝ : n
x✝ : m
⊢ (if x✝ = i then b i✝ else Mᵀ i✝ x✝) = if x✝ = i then b i✝ else M x✝ i✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ updateRow Mᴴ j (star c) = (updateColumn M j c)ᴴ
[PROOFSTEP]
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateRow_transpose, map_updateColumn]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ (updateColumn (map M star) j (star c))ᵀ = (updateColumn (map M star) j (star ∘ c))ᵀ
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ updateColumn Mᴴ i (star b) = (updateRow M i b)ᴴ
[PROOFSTEP]
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateColumn_transpose, map_updateRow]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ (updateRow (map M star) i (star b))ᵀ = (updateRow (map M star) i (star ∘ b))ᵀ
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ updateColumn (diagonal v) i (Pi.single i x) = diagonal (Function.update v i x)
[PROOFSTEP]
ext j k
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = diagonal (Function.update v i x) j k
[PROOFSTEP]
obtain rfl | hjk := eq_or_ne j k
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = diagonal (Function.update v i x) j j
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = Function.update v i x j
[PROOFSTEP]
obtain rfl | hji := eq_or_ne j i
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ updateColumn (diagonal v) j (Pi.single j x) j j = Function.update v j x j
[PROOFSTEP]
rw [updateColumn_self, Pi.single_eq_same, Function.update_same]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = Function.update v i x j
[PROOFSTEP]
rw [updateColumn_ne hji, diagonal_apply_eq, Function.update_noteq hji]
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = diagonal (Function.update v i x) j k
[PROOFSTEP]
rw [diagonal_apply_ne _ hjk]
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = 0
[PROOFSTEP]
obtain rfl | hki := eq_or_ne k i
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) k (Pi.single k x) j k = 0
[PROOFSTEP]
rw [updateColumn_self, Pi.single_eq_of_ne hjk]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = 0
[PROOFSTEP]
rw [updateColumn_ne hki, diagonal_apply_ne _ hjk]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ updateRow (diagonal v) i (Pi.single i x) = diagonal (Function.update v i x)
[PROOFSTEP]
rw [← diagonal_transpose, updateRow_transpose, diagonal_updateColumn_single, diagonal_transpose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
⊢ updateRow (submatrix A ↑e ↑f) i r = submatrix (updateRow A (↑e i) fun j => r (↑f.symm j)) ↑e ↑f
[PROOFSTEP]
ext i' j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ updateRow (submatrix A ↑e ↑f) i r i' j = submatrix (updateRow A (↑e i) fun j => r (↑f.symm j)) (↑e) (↑f) i' j
[PROOFSTEP]
simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i✝ : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : m
r : n → α
e : l ≃ m
f : o ≃ n
⊢ submatrix (updateRow A i r) ↑e ↑f = submatrix (updateRow A (↑e (↑e.symm i)) fun j => r (↑f (↑f.symm j))) ↑e ↑f
[PROOFSTEP]
simp_rw [Equiv.apply_symm_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j✝ : n
b : n → α
c✝ : m → α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : o
c : l → α
e : l ≃ m
f : o ≃ n
⊢ updateColumn (submatrix A ↑e ↑f) j c = submatrix (updateColumn A (↑f j) fun i => c (↑e.symm i)) ↑e ↑f
[PROOFSTEP]
simpa only [← transpose_submatrix, updateRow_transpose] using congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
M : Matrix m n α
i : m
j✝ : n
b : n → α
c✝ : m → α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : l ≃ m
f : o ≃ n
⊢ submatrix (updateColumn A j c) ↑e ↑f = submatrix (updateColumn A (↑f (↑f.symm j)) fun i => c (↑e (↑e.symm i))) ↑e ↑f
[PROOFSTEP]
simp_rw [Equiv.apply_symm_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
M : Matrix m n α
N : Matrix n o α
i : m
j : o
f : α →+* β
⊢ ↑f ((M * N) i j) = (map M ↑f * map N ↑f) i j
[PROOFSTEP]
simp [Matrix.mul_apply, map_sum]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : Fintype n
inst✝³ : NonAssocSemiring α
inst✝² : NonAssocSemiring β
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
v w : n → R
⊢ ↑f (v ⬝ᵥ w) = ↑f ∘ v ⬝ᵥ ↑f ∘ w
[PROOFSTEP]
simp only [Matrix.dotProduct, f.map_sum, f.map_mul, Function.comp]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : Fintype n
inst✝³ : NonAssocSemiring α
inst✝² : NonAssocSemiring β
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix n m R
v : n → R
i : m
⊢ ↑f (vecMul v M i) = vecMul (↑f ∘ v) (map M ↑f) i
[PROOFSTEP]
simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝⁴ : Fintype n
inst✝³ : NonAssocSemiring α
inst✝² : NonAssocSemiring β
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix m n R
v : n → R
i : m
⊢ ↑f (mulVec M v i) = mulVec (map M ↑f) (↑f ∘ v) i
[PROOFSTEP]
simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp]