obtain ⟨k, d, g, h_eq⟩ := hrs
case intro.intro.intro.intro.intro.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
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
hrs : ∃ n_1 f g, ∑ i : Fin n_1, f i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
case intro.intro.intro.intro.intro.h.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
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0