Theorem: Matrix.linearIndependent_rows_of_upper_tri (Matroid/ForMathlib/LinearAlgebra/Matrix/Rowspace.lean)

State before:
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
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ LinearIndependent R (A.fromBlocks B 0 C).rowFun
Tactic:
simp_rw [linearIndependent_iff, Finsupp.total_apply] at *
State after:
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
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
⊢ ∀ (l : m₀ ⊕ m₁ →₀ R), (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0 → l = 0

State before:
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
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
⊢ ∀ (l : m₀ ⊕ m₁ →₀ R), (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0 → l = 0
Tactic:
intro l hl
State after:
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
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
⊢ l = 0

State before:
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
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
⊢ l = 0
Tactic:
specialize hA (l.comapDomain Sum.inl Sum.inl_injective.injOn)
State after:
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
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
⊢ l = 0

State before:
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
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
⊢ l = 0
Tactic:
specialize hC (l.comapDomain Sum.inr Sum.inr_injective.injOn)
State after:
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
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ((Finsupp.comapDomain Sum.inr l ⋯).sum fun i a => a • C.rowFun i) = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
⊢ l = 0

State before:
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
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ((Finsupp.comapDomain Sum.inr l ⋯).sum fun i a => a • C.rowFun i) = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
⊢ l = 0
Tactic:
simp only [Finsupp.sum, Finsupp.comapDomain_support, Finsupp.comapDomain_apply] at hA hC hl
State after:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
⊢ l = 0

State before:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
⊢ l = 0
Tactic:
specialize hA ?_
State after:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0

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
⊢ l = 0

State before:
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
⊢ l = 0
Tactic:
ext (i | i)
State after:
case h.inl
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₀
⊢ l (Sum.inl i) = 0 (Sum.inl i)

case h.inr
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₁
⊢ l (Sum.inr i) = 0 (Sum.inr i)

State before:
case h.inr
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₁
⊢ l (Sum.inr i) = 0 (Sum.inr i)
Tactic:
refine DFunLike.congr_fun (hC ?_) i
State after:
case h.inr
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₁
⊢ ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0

State before:
case h.inr
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₁
⊢ ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0
Tactic:
ext j
State after:
case h.inr.h
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.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j = 0 j

State before:
case h.inr.h
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.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j = 0 j
Tactic:
convert congr_fun hl (Sum.inr j)
State after:
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.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j =
    (∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x) (Sum.inr j)

State before:
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.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j =
    (∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x) (Sum.inr j)
Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
State after:
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.preimage Sum.inr ⋯, l (Sum.inr x) * C.rowFun x j =
    ∑ x ∈ l.support, l x * (A.fromBlocks B 0 C).rowFun x (Sum.inr j)

State before:
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.preimage Sum.inr ⋯, l (Sum.inr x) * C.rowFun x j =
    ∑ x ∈ l.support, l x * (A.fromBlocks B 0 C).rowFun x (Sum.inr j)
Tactic:
convert Finset.sum_preimage Sum.inr l.support Sum.inr_injective.injOn
  (fun (i : m₀ ⊕ m₁) ↦ l i * ((Matrix.fromBlocks A B 0 C) i (Sum.inr j))) ?_
State after:
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

State before:
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
Tactic:
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]
State after:
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

State before:
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
Tactic:
exact fun i₀ hi₀ ↦ (hi₀ (DFunLike.congr_fun hA i₀)).elim
State after:
no goals

State before:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0
Tactic:
ext j
State after:
case h
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ (∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x) j = 0 j

State before:
case h
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ (∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x) j = 0 j
Tactic:
convert congr_fun hl (Sum.inl j)
State after:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ (∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x) j =
    (∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x) (Sum.inl j)

State before:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ (∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x) j =
    (∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x) (Sum.inl j)
Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
State after:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) * A.rowFun x j =
    ∑ x ∈ l.support, l x * (A.fromBlocks B 0 C).rowFun x (Sum.inl j)

State before:
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) * A.rowFun x j =
    ∑ x ∈ l.support, l x * (A.fromBlocks B 0 C).rowFun x (Sum.inl j)
Tactic:
convert Finset.sum_preimage Sum.inl l.support Sum.inl_injective.injOn
  (fun (i : m₀ ⊕ m₁) ↦ l i * ((Matrix.fromBlocks A B 0 C) i (Sum.inl j)))
State after:
case a
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) * A.rowFun x j =
      ∑ x ∈ l.support, l x * (A.fromBlocks B 0 C).rowFun x (Sum.inl j) ↔
    (∀ x ∈ l.support, x ∉ range Sum.inl → l x * A.fromBlocks B 0 C x (Sum.inl j) = 0) →
      ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) * A.fromBlocks B 0 C (Sum.inl x) (Sum.inl j) =
        ∑ x ∈ l.support, l x * A.fromBlocks B 0 C x (Sum.inl j)

State before:
case a
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
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
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
j : n₀
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) * A.rowFun x j =
      ∑ x ∈ l.support, l x * (A.fromBlocks B 0 C).rowFun x (Sum.inl j) ↔
    (∀ x ∈ l.support, x ∉ range Sum.inl → l x * A.fromBlocks B 0 C x (Sum.inl j) = 0) →
      ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) * A.fromBlocks B 0 C (Sum.inl x) (Sum.inl j) =
        ∑ x ∈ l.support, l x * A.fromBlocks B 0 C x (Sum.inl j)
Tactic:
simp
State after:
no goals

State before:
case h.inl
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₀
⊢ l (Sum.inl i) = 0 (Sum.inl i)
Tactic:
exact DFunLike.congr_fun hA i
State after:
no goals