-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem BlockTriangular.mul [Fintype m] [NonUnitalNonAssocSemiring R]
    {M N : Matrix m m R} (hM : BlockTriangular M b)
    (hN : BlockTriangular N b) : BlockTriangular (M * N) b

Proof state:
case neg
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : ¬b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0

Tactic:
simp_rw [hN (lt_of_lt_of_le hij (le_of_not_lt hki)), mul_zero]

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
⊢ (M * N) i j = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case h
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
⊢ ∀ x ∈ univ, (fun j => M i j) x * (fun j_1 => N j_1 j) x = 0

Proof state:
case h
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0

Tactic:
by_cases hki : b k < b i

Result:
case pos
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0

case neg
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : ¬b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0

Proof state:
case pos
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0

Tactic:
simp_rw [hM hki, zero_mul]

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
⊢ (M * N).BlockTriangular b

Tactic:
intro i j hij

Result:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
⊢ (M * N) i j = 0

Proof state:
case h
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
⊢ ∀ x ∈ univ, (fun j => M i j) x * (fun j_1 => N j_1 j) x = 0

Tactic:
intro k _

Result:
case h
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0