mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : n
val✝ : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : n
val✝ : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : o
val✝ : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : o
val✝ : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j)

pp: ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j) = ((w i)⁻¹ • e.coord i) (e j)

Tactic:
·

Goal state after:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j

pp: case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j

Tactic:
·

Goal state after:
case pos
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j

Tactic:
·

Goal state after:
case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : l
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
i j : l ⊕ m
⊢ fromBlocks 1 0 0 1 i j = 1 i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inl val✝) = 1 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : l
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inr val✝) = 1 (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inl val✝) = 1 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inr val✝) = 1 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
⊢ vecMulVec x 1 = replicateCol m x

Tactic:
ext; simp [vecMulVec_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
⊢ vecMulVec 1 x = replicateRow m x

Tactic:
ext; simp [vecMulVec_apply]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M i✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1

pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0

Tactic:
·

Goal state after:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M i✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0

Tactic:
·

Goal state after:
case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
·

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
·

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
·

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
·

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateCol j c).map f i✝ j✝ = (M.map f).updateCol j (f ∘ c) i✝ j✝

Tactic:
updateCol_apply,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateCol j c).map f i✝ j✝ = if j✝ = j then (f ∘ c) i✝ else M.map f i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = diagonal (Function.update v i x) j j

pp: case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Tactic:
·

Goal state after:
case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = diagonal (Function.update v i x) j j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ (diagonal v).updateCol j (Pi.single j x) j j = Function.update v j x j

pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
·

Goal state after:
case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ (diagonal v).updateCol j (Pi.single j x) j j = Function.update v j x j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
·

Goal state after:
case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Tactic:
·

Goal state after:
case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single k x) j k = 0

pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
·

Goal state after:
case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single k x) j k = 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
·

Goal state after:
case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i ↦ d (i, k)) i i

pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j

Tactic:
·

Goal state after:
case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i ↦ d (i, k)) i i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j

Tactic:
·

Goal state after:
case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
c v : m → α
i' : l
⊢ (A.updateRow i' c *ᵥ v) i' = Function.update (A *ᵥ v) i' (c ⬝ᵥ v) i'

pp: case inr
l : Type u_1
m : Type u_2
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
c v : m → α
i' : l
hi : i' ≠ i
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (A *ᵥ v) i (c ⬝ᵥ v) i'

Tactic:
·

Goal state after:
case inl
l : Type u_1
m : Type u_2
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
c v : m → α
i' : l
⊢ (A.updateRow i' c *ᵥ v) i' = Function.update (A *ᵥ v) i' (c ⬝ᵥ v) i'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
c v : m → α
i' : l
hi : i' ≠ i
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (A *ᵥ v) i (c ⬝ᵥ v) i'

Tactic:
·

Goal state after:
case inr
l : Type u_1
m : Type u_2
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
c v : m → α
i' : l
hi : i' ≠ i
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (A *ᵥ v) i (c ⬝ᵥ v) i'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
r : m → α
j' : n
⊢ (v ᵥ* B.updateCol j' r) j' = Function.update (v ᵥ* B) j' (v ⬝ᵥ r) j'

pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
hj : j' ≠ j
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'

Tactic:
·

Goal state after:
case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
r : m → α
j' : n
⊢ (v ᵥ* B.updateCol j' r) j' = Function.update (v ᵥ* B) j' (v ⬝ᵥ r) j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
hj : j' ≠ j
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'

Tactic:
·

Goal state after:
case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
hj : j' ≠ j
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
a : α
i' : m
j : n
⊢ vecMulVec (Function.update u i' a) v i' j = (vecMulVec u v).updateRow i' (a • v) i' j

pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
hi : i' ≠ i
⊢ vecMulVec (Function.update u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j

Tactic:
·

Goal state after:
case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
a : α
i' : m
j : n
⊢ vecMulVec (Function.update u i' a) v i' j = (vecMulVec u v).updateRow i' (a • v) i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
hi : i' ≠ i
⊢ vecMulVec (Function.update u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j

Tactic:
·

Goal state after:
case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
hi : i' ≠ i
⊢ vecMulVec (Function.update u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
a : α
i : m
j' : n
⊢ vecMulVec u (Function.update v j' a) i j' = (vecMulVec u v).updateCol j' (MulOpposite.op a • u) i j'

pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
j : n
a : α
i : m
j' : n
hi : j' ≠ j
⊢ vecMulVec u (Function.update v j a) i j' = (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'

Tactic:
·

Goal state after:
case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
a : α
i : m
j' : n
⊢ vecMulVec u (Function.update v j' a) i j' = (vecMulVec u v).updateCol j' (MulOpposite.op a • u) i j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
j : n
a : α
i : m
j' : n
hi : j' ≠ j
⊢ vecMulVec u (Function.update v j a) i j' = (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'

Tactic:
·

Goal state after:
case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
j : n
a : α
i : m
j' : n
hi : j' ≠ j
⊢ vecMulVec u (Function.update v j a) i j' = (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
r : m → α
B : Matrix m n α
i' : l
j' : n
⊢ (A.updateRow i' r * B) i' j' = (A * B).updateRow i' (r ᵥ* B) i' j'

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
hi : i' ≠ i
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'

Tactic:
·

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
r : m → α
B : Matrix m n α
i' : l
j' : n
⊢ (A.updateRow i' r * B) i' j' = (A * B).updateRow i' (r ᵥ* B) i' j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
hi : i' ≠ i
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'

Tactic:
·

Goal state after:
case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
hi : i' ≠ i
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
c : m → α
i' : l
j' : n
⊢ (A * B.updateCol j' c) i' j' = (A * B).updateCol j' (A *ᵥ c) i' j'

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
i' : l
j' : n
hj : j' ≠ j
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'

Tactic:
·

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
c : m → α
i' : l
j' : n
⊢ (A * B.updateCol j' c) i' j' = (A * B).updateCol j' (A *ᵥ c) i' j'