rintro rfl
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
c : K
h' : c • f i = f j
⊢ c ≠ 0
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
h' : 0 • f i = f j
⊢ False