internlm/Lean-Github huggingface dataset:
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 : 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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⟩
Proof state after:
no goals
Theorem: Matrix.colBasis_iff_aux
Proof 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
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 : ∃ c, ∑ i : n, c i • A₂ᵀ.rowFun i = 0 ∧ (∃ i ∈ tᶜ, c i ≠ 0) ∧ ∀ i ∉ tᶜ, c i = 0
⊢ False
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof state after:
no goals
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
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]
Proof 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
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
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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof state after:
no goals
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
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
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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