case mp
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag (fromBlocks A B C D) → IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D

case mpr
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D → IsDiag (fromBlocks A B C D)
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag (fromBlocks A B C D) ↔ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
constructor
case mp
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
⊢ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
case mp
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag (fromBlocks A B C D) → IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
intro h
case mp.refine'_1
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i j : m
hij : i ≠ j
⊢ A i j = 0

case mp.refine'_2
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i : m
j : n
⊢ B i j = OfNat.ofNat 0 i j

case mp.refine'_3
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i : n
j : m
⊢ C i j = OfNat.ofNat 0 i j

case mp.refine'_4
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i j : n
hij : i ≠ j
⊢ D i j = 0
case mp
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
⊢ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
refine' ⟨fun i j hij => _, ext fun i j => _, ext fun i j => _, fun i j hij => _⟩
no goals
case mp.refine'_1
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i j : m
hij : i ≠ j
⊢ A i j = 0
exact h (Sum.inl_injective.ne hij)
no goals
case mp.refine'_2
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i : m
j : n
⊢ B i j = OfNat.ofNat 0 i j
exact h Sum.inl_ne_inr
no goals
case mp.refine'_3
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i : n
j : m
⊢ C i j = OfNat.ofNat 0 i j
exact h Sum.inr_ne_inl
no goals
case mp.refine'_4
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i j : n
hij : i ≠ j
⊢ D i j = 0
exact h (Sum.inr_injective.ne hij)
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
ha : IsDiag A
hb : B = 0
hc : C = 0
hd : IsDiag D
⊢ IsDiag (fromBlocks A B C D)
case mpr
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D → IsDiag (fromBlocks A B C D)
rintro ⟨ha, hb, hc, hd⟩
no goals
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.22462
R : Type ?u.22465
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
ha : IsDiag A
hb : B = 0
hc : C = 0
hd : IsDiag D
⊢ IsDiag (fromBlocks A B C D)
convert IsDiag.fromBlocks ha hd