simp only [Finsupp.mem_support_iff, ne_eq, mem_range, not_exists, Sum.forall, not_false_eq_true,
  implies_true, fromBlocks_apply₁₂, forall_true_left, Sum.inr.injEq, forall_eq,
  fromBlocks_apply₂₂, IsEmpty.forall_iff, and_true]
case h.e'_2
l✝ : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁✝ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝¹ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B✝ : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
j : n₁
⊢ ∀ x ∈ l.support, x ∉ range Sum.inr → (fun i => l i * A.fromBlocks B 0 C i (Sum.inr j)) x = 0
case h.e'_2
l✝ : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁✝ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝¹ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B✝ : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
j : n₁
⊢ ∀ (a : m₀), ¬l (Sum.inl a) = 0 → l (Sum.inl a) * B a j = 0