internlm/Lean-Github huggingface dataset:
Theorem: Matrix.colBasis_iff_aux
Proof 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 ↦ ?_ , ?_⟩
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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)
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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) ?_
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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)]
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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