case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1

case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
by_cases hf : FiniteDimensional k s.direction
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1

case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1

case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
swap
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
have : FiniteDimensional k s.direction := hf
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : ↑s = ∅
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1

case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
hf' : ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
have hf' : ¬FiniteDimensional k (vectorSpan k (insert p (s : Set P))) := by
  intro h
  have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
    conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
    exact vectorSpan_mono k (Set.subset_insert _ _)
  exact hf (Submodule.finiteDimensional_of_le h')
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
hf' : ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ 0 ≤ 1
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
hf' : ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]
no goals
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
hf' : ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ 0 ≤ 1
exact zero_le_one
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ False
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
intro h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
h' : direction s ≤ vectorSpan k (insert p ↑s)
⊢ False
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ False
have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
  conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
  exact vectorSpan_mono k (Set.subset_insert _ _)
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
h' : direction s ≤ vectorSpan k (insert p ↑s)
⊢ False
exact hf (Submodule.finiteDimensional_of_le h')
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ vectorSpan k ↑s ≤ vectorSpan k (insert p ↑s)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ direction s ≤ vectorSpan k (insert p ↑s)
conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ vectorSpan k ↑s ≤ vectorSpan k (insert p ↑s)
exact vectorSpan_mono k (Set.subset_insert _ _)
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : ↑s = ∅
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
rw [coe_eq_bot_iff] at hs
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } ≤ 1
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan, direction_bot, finrank_bot,
  zero_add]
case h.e'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } = 0
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } ≤ 1
convert zero_le_one' ℕ
case h.e'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } = finrank k { x // x ∈ ⊥ }
case h.e'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } = 0
rw [← finrank_bot k V]
no goals
case h.e'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } = finrank k { x // x ∈ ⊥ }
convert rfl <;> simp
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ Submodule.span k {p -ᵥ p₀} ⊔ direction s } ≤ 1 + finrank k { x // x ∈ direction s }
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ Submodule.span k {p -ᵥ p₀} } ≤ 1
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ Submodule.span k {p -ᵥ p₀} ⊔ direction s } ≤ 1 + finrank k { x // x ∈ direction s }
refine' (Submodule.finrank_add_le_finrank_add_finrank _ _).trans (add_le_add_right _ _)
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ Submodule.span k {p -ᵥ p₀} } ≤ 1
refine' finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => _
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
h : ↑v ∈ Submodule.span k {p -ᵥ p₀}
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
have h := v.property
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
h : ∃ a, a • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
h : ↑v ∈ Submodule.span k {p -ᵥ p₀}
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
rw [Submodule.mem_span_singleton] at h
case pos.inr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
h : ∃ a, a • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
rcases h with ⟨c, hc⟩
case pos.inr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
case pos.inr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
refine' ⟨c, _⟩
case pos.inr.intro.intro.a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ↑(c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) }) = ↑v
case pos.inr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
ext
no goals
case pos.inr.intro.intro.a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ↑(c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) }) = ↑v
exact hc