internlm/Lean-Github huggingface dataset:
Theorem: Matrix.colBasis_iff_aux
Proof 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]
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 ᵥ* A₁) ∘ Subtype.val
Theorem: Matrix.colBasis_iff_aux
Proof 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⟩
Proof 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⟩
Theorem: Matrix.colBasis_iff_aux
Proof 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
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
j : ↑t
i : n
hi : i ∈ t
⊢ i ∉ tᶜ
Tactic:
simpa
Proof state after:
no goals
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 = 0
⊢ False
Tactic:
simp [hker] at hcex
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 : 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]
Proof state after:
no goals
Theorem: Matrix.colBasis_iff_aux
Proof 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 ↦ ?_
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
j : n
⊢ (∑ i : m₂, c i • A₂.rowFun i) j = 0 j
Theorem: Matrix.colBasis_iff_aux
Proof 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)
Proof 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
Theorem: Matrix.colBasis_iff_aux
Proof 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⟩
Proof 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⟩
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof state after:
no goals
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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⟩
Theorem: Matrix.colBasis_iff_aux
Proof 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]
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 : 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
Proof state after:
no goals
Theorem: Matrix.colBasis_iff_aux
Proof 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
Proof 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✝
Theorem: Matrix.colBasis_iff_aux
Proof 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]
Proof state after:
no goals
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
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
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ
Tactic:
obtain ⟨b₁, hb₁⟩ := A₁.exists_rowBasis
Proof state after:
case 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
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ
Tactic:
obtain ⟨b₂, hb₂⟩ := A₂.exists_rowBasis
Proof state after:
case 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
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
hb₂ : A₂.RowBasis b₂
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ