Theorem: Matrix.colBasis_iff_aux (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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
⊢ A₂.ColBasis tᶜ
Tactic:
refine ⟨by_contra fun hld ↦ ?_ , ?_⟩
State after:
case refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
hld : ¬LinearIndependent (ι := ↑tᶜ) K (A₂ᵀ.rowSubmatrix tᶜ).rowFun
⊢ False

case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
⊢ (A₂ᵀ.rowSubmatrix tᶜ).rowSpace = A₂ᵀ.rowSpace

State before:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
⊢ (A₂ᵀ.rowSubmatrix tᶜ).rowSpace = A₂ᵀ.rowSpace
Tactic:
rw [rowSpace_transpose, ← colSubmatrix_transpose, rowSpace_transpose,
  colSpace_eq_top_iff_linearIndependent_rows.2 h₂, colSpace_eq_top_iff_linearIndependent_rows,
  Fintype.linearIndependent_iff]
State after:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
⊢ ∀ (g : m₂ → K), ∑ i : m₂, g i • (A₂.colSubmatrix tᶜ).rowFun i = 0 → ∀ (i : m₂), g i = 0

State before:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
⊢ ∀ (g : m₂ → K), ∑ i : m₂, g i • (A₂.colSubmatrix tᶜ).rowFun i = 0 → ∀ (i : m₂), g i = 0
Tactic:
intro c hc0
State after:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
⊢ ∀ (i : m₂), c i = 0

State before:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
⊢ ∀ (i : m₂), c i = 0
Tactic:
have h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace := by
  rw [← rowSpace_eq_lin_range, ← orthSpace_rowSpace_eq_nullSpace, h,
    orthSpace_nullSpace_eq_rowSpace]
State after:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
⊢ ∀ (i : m₂), c i = 0

State before:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
⊢ ∀ (i : m₂), c i = 0
Tactic:
have h0 := mem_nullSpace_iff.1 <| h₂₁.le (LinearMap.mem_range_self A₂.vecMulLinear c)
State after:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : A₁ *ᵥ A₂.vecMulLinear c = 0
⊢ ∀ (i : m₂), c i = 0

State before:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : A₁ *ᵥ A₂.vecMulLinear c = 0
⊢ ∀ (i : m₂), c i = 0
Tactic:
simp_rw [mulVec_eq_sum, vecMulLinear_apply, vecMul, dotProduct] at h0
State after:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∀ (i : m₂), c i = 0

State before:
case refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∀ (i : m₂), c i = 0
Tactic:
have h01 := Fintype.linearIndependent_iff.1 ht.linearIndependent (fun x ↦ vecMul c A₂ x) ?_
State after:
case refine_2.refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
⊢ ∀ (i : m₂), c i = 0

case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ i : ↑t, (fun x => (c ᵥ* A₂) ↑x) i • (A₁.colSubmatrix t).colFun i = 0

State before:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ i : ↑t, (fun x => (c ᵥ* A₂) ↑x) i • (A₁.colSubmatrix t).colFun i = 0
Tactic:
rw [← h0]
State after:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ i : ↑t, (fun x => (c ᵥ* A₂) ↑x) i • (A₁.colSubmatrix t).colFun i =
    ∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x

State before:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ i : ↑t, (fun x => (c ᵥ* A₂) ↑x) i • (A₁.colSubmatrix t).colFun i =
    ∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x
Tactic:
simp only [colSubmatrix_transpose, rowSubmatrix_apply, ← Finset.sum_fn]
State after:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ x : ↑t, (c ᵥ* A₂) ↑x • A₁ᵀ ↑x = ∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x

State before:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ x : ↑t, (c ᵥ* A₂) ↑x • A₁ᵀ ↑x = ∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x
Tactic:
rw [← Finset.sum_subset (s₁ := t.toFinset) (by simp)]
State after:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∑ x : ↑t, (c ᵥ* A₂) ↑x • A₁ᵀ ↑x = ∑ x ∈ t.toFinset, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x

case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∀ x ∈ Finset.univ, x ∉ t.toFinset → ((∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0

State before:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∀ x ∈ Finset.univ, x ∉ t.toFinset → ((∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
Tactic:
simp only [Finset.mem_univ, mem_toFinset, forall_true_left, smul_eq_zero]
State after:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∀ x ∉ t, ∑ x_1 : m₂, c x_1 * A₂ x_1 x = 0 ∨ (fun x_1 => A₁ x_1 x) = 0

State before:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ ∀ x ∉ t, ∑ x_1 : m₂, c x_1 * A₂ x_1 x = 0 ∨ (fun x_1 => A₁ x_1 x) = 0
Tactic:
rintro x hxt
State after:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x : n
hxt : x ∉ t
⊢ ∑ x_1 : m₂, c x_1 * A₂ x_1 x = 0 ∨ (fun x_1 => A₁ x_1 x) = 0

State before:
case refine_2.refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x : n
hxt : x ∉ t
⊢ ∑ x_1 : m₂, c x_1 * A₂ x_1 x = 0 ∨ (fun x_1 => A₁ x_1 x) = 0
Tactic:
left
State after:
case refine_2.refine_1.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x : n
hxt : x ∉ t
⊢ ∑ x_1 : m₂, c x_1 * A₂ x_1 x = 0

State before:
case refine_2.refine_1.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x : n
hxt : x ∉ t
⊢ ∑ x_1 : m₂, c x_1 * A₂ x_1 x = 0
Tactic:
simpa using congr_fun hc0 ⟨x, hxt⟩
State after:
no goals

State before:
case refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
hld : ¬LinearIndependent (ι := ↑tᶜ) K (A₂ᵀ.rowSubmatrix tᶜ).rowFun
⊢ False
Tactic:
rw [rowFun_rowSubmatrix_eq, Fintype.not_linearIndependent_restrict_iff'] at hld
State after:
case refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
hld : ∃ c, ∑ i : n, c i • A₂ᵀ.rowFun i = 0 ∧ (∃ i ∈ tᶜ, c i ≠ 0) ∧ ∀ i ∉ tᶜ, c i = 0
⊢ False

State before:
case refine_1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
hld : ∃ c, ∑ i : n, c i • A₂ᵀ.rowFun i = 0 ∧ (∃ i ∈ tᶜ, c i ≠ 0) ∧ ∀ i ∉ tᶜ, c i = 0
⊢ False
Tactic:
obtain ⟨c, hc0, hcex, hct⟩ := hld
State after:
case refine_1.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
⊢ False

State before:
case refine_1.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
⊢ False
Tactic:
have hnull : c ∈ A₂.nullSpace := by
  rw [mem_nullSpace_iff, mulVec_eq_sum]
  ext i
  convert congr_fun hc0 i
State after:
case refine_1.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
hnull : c ∈ A₂.nullSpace
⊢ False

State before:
case refine_1.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
hnull : c ∈ A₂.nullSpace
⊢ False
Tactic:
rw [← h, rowSpace_eq_lin_range, LinearMap.mem_range] at hnull
State after:
case refine_1.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
hnull : ∃ y, A₁.vecMulLinear y = c
⊢ False

State before:
case refine_1.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
hnull : ∃ y, A₁.vecMulLinear y = c
⊢ False
Tactic:
obtain ⟨d, rfl⟩ := hnull
State after:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
⊢ False

State before:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
⊢ False
Tactic:
have hker : d ∈ LinearMap.ker (vecMulLinear (A₁.colSubmatrix t)) := by
  ext j
  convert congr_fun (submatrix_vecMul_equiv A₁ d (Equiv.refl _) _) j
  simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_id]
  ext ⟨i,hi⟩
  exact (hct i (by simpa)).symm
State after:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
hker : d ∈ LinearMap.ker (A₁.colSubmatrix t).vecMulLinear
⊢ False

State before:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
hker : d ∈ LinearMap.ker (A₁.colSubmatrix t).vecMulLinear
⊢ False
Tactic:
rw [← transpose_transpose A₁, ← rowSubmatrix_transpose, rows_linearIndependent_iff.1, mem_bot]
  at hker
State after:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
hker : d = 0
⊢ False

case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
hker : d ∈ LinearMap.ker (A₁ᵀ.rowSubmatrix t)ᵀ.vecMulLinear
⊢ LinearIndependent K (A₁ᵀ.rowSubmatrix t)ᵀ.rowFun

State before:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
hker : d ∈ LinearMap.ker (A₁ᵀ.rowSubmatrix t)ᵀ.vecMulLinear
⊢ LinearIndependent K (A₁ᵀ.rowSubmatrix t)ᵀ.rowFun
Tactic:
rwa [rowSubmatrix_transpose, transpose_transpose, ← colSpace_eq_top_iff_linearIndependent_rows,
  ht.colSpace_eq, colSpace_eq_top_iff_linearIndependent_rows]
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
⊢ c ∈ A₂.nullSpace
Tactic:
rw [mem_nullSpace_iff, mulVec_eq_sum]
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
⊢ (∑ i : n, c i • fun x => A₂ x i) = 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
⊢ (∑ i : n, c i • fun x => A₂ x i) = 0
Tactic:
ext i
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
i : m₂
⊢ (∑ i : n, c i • fun x => A₂ x i) i = 0 i

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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : n → K
hc0 : ∑ i : n, c i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, c i ≠ 0
hct : ∀ i ∉ tᶜ, c i = 0
i : m₂
⊢ (∑ i : n, c i • fun x => A₂ x i) i = 0 i
Tactic:
convert congr_fun hc0 i
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
⊢ d ∈ LinearMap.ker (A₁.colSubmatrix t).vecMulLinear
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
⊢ (A₁.colSubmatrix t).vecMulLinear d 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
⊢ (A₁.colSubmatrix t).vecMulLinear d j = 0 j
Tactic:
convert congr_fun (submatrix_vecMul_equiv A₁ d (Equiv.refl _) _) j
State after:
case h.e'_3.h.e
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
⊢ 0 = (d ∘ ⇑(Equiv.refl m₁).symm ᵥ* A₁) ∘ Subtype.val

State before:
case h.e'_3.h.e
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
⊢ 0 = (d ∘ ⇑(Equiv.refl m₁).symm ᵥ* A₁) ∘ Subtype.val
Tactic:
simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_id]
State after:
case h.e'_3.h.e
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
⊢ 0 = (d ᵥ* A₁) ∘ Subtype.val

State before:
case h.e'_3.h.e
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
⊢ 0 = (d ᵥ* A₁) ∘ Subtype.val
Tactic:
ext ⟨i,hi⟩
State after:
case h.e'_3.h.e.h.mk
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
i : n
hi : i ∈ t
⊢ 0 ⟨i, hi⟩ = ((d ᵥ* A₁) ∘ Subtype.val) ⟨i, hi⟩

State before:
case h.e'_3.h.e.h.mk
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
i : n
hi : i ∈ t
⊢ 0 ⟨i, hi⟩ = ((d ᵥ* A₁) ∘ Subtype.val) ⟨i, hi⟩
Tactic:
exact (hct i (by simpa)).symm
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
j : ↑t
i : n
hi : i ∈ t
⊢ i ∉ tᶜ
Tactic:
simpa
State after:
no goals

State before:
case refine_1.intro.intro.intro.intro
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
d : m₁ → K
hc0 : ∑ i : n, A₁.vecMulLinear d i • A₂ᵀ.rowFun i = 0
hcex : ∃ i ∈ tᶜ, A₁.vecMulLinear d i ≠ 0
hct : ∀ i ∉ tᶜ, A₁.vecMulLinear d i = 0
hker : d = 0
⊢ False
Tactic:
simp [hker] at hcex
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
⊢ LinearMap.range A₂.vecMulLinear = A₁.nullSpace
Tactic:
rw [← rowSpace_eq_lin_range, ← orthSpace_rowSpace_eq_nullSpace, h,
  orthSpace_nullSpace_eq_rowSpace]
State after:
no goals

State before:
case refine_2.refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
⊢ ∀ (i : m₂), c i = 0
Tactic:
refine Fintype.linearIndependent_iff.1 h₂ c <| funext fun j ↦ ?_
State after:
case refine_2.refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j

State before:
case refine_2.refine_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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j
Tactic:
obtain (hjt | hjt) := em (j ∈ t)
State after:
case refine_2.refine_2.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∈ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j

case refine_2.refine_2.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∉ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j

State before:
case refine_2.refine_2.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∉ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j
Tactic:
convert congr_fun hc0 ⟨j,hjt⟩
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∉ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = (∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i) ⟨j, hjt⟩

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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∉ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = (∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i) ⟨j, hjt⟩
Tactic:
simp
State after:
no goals

State before:
case refine_2.refine_2.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∈ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j
Tactic:
convert h01 ⟨j,hjt⟩ using 1
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∈ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = (c ᵥ* A₂) ↑⟨j, hjt⟩

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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
h01 : ∀ (i : ↑t), (c ᵥ* A₂) ↑i = 0
j : n
hjt : j ∈ t
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = (c ᵥ* A₂) ↑⟨j, hjt⟩
Tactic:
simp [vecMul, dotProduct]
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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
⊢ t.toFinset ⊆ Finset.univ
Tactic:
simp
State after:
no goals

State before:
case h.e'_2.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x✝ : ↑t
a✝ : x✝ ∈ Finset.univ
⊢ (c ᵥ* A₂) ↑x✝ • A₁ᵀ ↑x✝ = (∑ x : m₂, c x * A₂ x ↑x✝) • fun x => A₁ x ↑x✝
Tactic:
ext
State after:
case h.e'_2.a.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x✝¹ : ↑t
a✝ : x✝¹ ∈ Finset.univ
x✝ : m₁
⊢ ((c ᵥ* A₂) ↑x✝¹ • A₁ᵀ ↑x✝¹) x✝ = ((∑ x : m₂, c x * A₂ x ↑x✝¹) • fun x => A₁ x ↑x✝¹) x✝

State before:
case h.e'_2.a.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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
h₁ : LinearIndependent K A₁.rowFun
h₂ : LinearIndependent K A₂.rowFun
ht : A₁.ColBasis t
c : m₂ → K
hc0 : ∑ i : m₂, c i • (A₂.colSubmatrix tᶜ).rowFun i = 0
h₂₁ : LinearMap.range A₂.vecMulLinear = A₁.nullSpace
h0 : (∑ x : n, (∑ x_1 : m₂, c x_1 * A₂ x_1 x) • fun x_1 => A₁ x_1 x) = 0
x✝¹ : ↑t
a✝ : x✝¹ ∈ Finset.univ
x✝ : m₁
⊢ ((c ᵥ* A₂) ↑x✝¹ • A₁ᵀ ↑x✝¹) x✝ = ((∑ x : m₂, c x * A₂ x ↑x✝¹) • fun x => A₁ x ↑x✝¹) x✝
Tactic:
simp [mul_comm, vecMul, dotProduct]
State after:
no goals