ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ ∀ (x_1 : K) (x_2 : V), x_2 ∈ span K s → x = x_1 • y + x_2 → ¬x ∈ span K s → ∃ a z, z ∈ span K s ∧ y = a • x + z
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ x ∈ span K (insert y s) → ¬x ∈ span K s → y ∈ span K (insert x s)
simp [mem_span_insert]
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
⊢ ∃ a_1 z_1, z_1 ∈ span K s ∧ y = a_1 • (a • y + z) + z_1
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ ∀ (x_1 : K) (x_2 : V), x_2 ∈ span K s → x = x_1 • y + x_2 → ¬x ∈ span K s → ∃ a z, z ∈ span K s ∧ y = a • x + z
rintro a z hz rfl h
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
⊢ ∃ a_1 z_1, z_1 ∈ span K s ∧ y = a_1 • (a • y + z) + z_1
refine' ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, _⟩
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
a0 : a ≠ 0
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
have a0 : a ≠ 0 := by
  rintro rfl
  simp_all
no goals
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
a0 : a ≠ 0
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
simp [a0, smul_add, smul_smul]
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ z : V
hz : z ∈ span K s
h : ¬0 • y + z ∈ span K s
⊢ False
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ : V
a : K
z : V
hz : z ∈ span K s
h : ¬a • y + z ∈ span K s
⊢ a ≠ 0
rintro rfl
no goals
ι : Type u'
ι' : Type ?u.1192090
R : Type ?u.1192093
K : Type u_1
M : Type ?u.1192099
M' : Type ?u.1192102
M'' : Type ?u.1192105
V : Type u
V' : Type ?u.1192110
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z✝ z : V
hz : z ∈ span K s
h : ¬0 • y + z ∈ span K s
⊢ False
simp_all