-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem finrank_vectorSpan_insert_le (s : AffineSubspace k P) (p : P) :
    finrank k (vectorSpan k (insert p (s : Set P))) ≤ finrank k s.direction + 1

Proof state:
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 ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
v : ↥(Submodule.span k {p -ᵥ p₀})
h : ↑v ∈ Submodule.span k {p -ᵥ p₀}
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

Tactic:
rw [Submodule.mem_span_singleton] at h

Result:
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 ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
v : ↥(Submodule.span k {p -ᵥ p₀})
h : ∃ a, a • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

Proof state:
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 ↥s.direction
hs : ↑s = ∅
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Tactic:
rw [coe_eq_bot_iff] at hs

Result:
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 ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Proof state:
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 ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
have : FiniteDimensional k s.direction := hf

Result:
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 ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Proof state:
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 ↥s.direction
h : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ s.direction ≤ vectorSpan k (insert p ↑s)

Tactic:
conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]

Result:
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 ↥s.direction
h : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ vectorSpan k ↑s ≤ vectorSpan k (insert p ↑s)

Proof state:
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 ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Tactic:
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan, direction_bot, finrank_bot,
  zero_add]

Result:
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 ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) ≤ 1

Proof state:
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 ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
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')

Result:
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 ↥s.direction
hf' : ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Proof state:
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 ↥s.direction
hf' : ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]

Result:
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 ↥s.direction
hf' : ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ 0 ≤ 1

Proof state:
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 ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(Submodule.span k {p -ᵥ p₀} ⊔ s.direction) ≤ 1 + finrank k ↥s.direction

Tactic:
refine (Submodule.finrank_add_le_finrank_add_finrank _ _).trans (add_le_add_right ?_ _)

Result:
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 ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(Submodule.span k {p -ᵥ p₀}) ≤ 1

Proof state:
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 ↥s.direction
⊢ ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))

Tactic:
intro h

Result:
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 ↥s.direction
h : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ False

Proof state:
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 ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
v : ↥(Submodule.span k {p -ᵥ p₀})
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

Tactic:
refine ⟨c, ?_⟩

Result:
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 ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
v : ↥(Submodule.span k {p -ᵥ p₀})
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ c • ⟨p -ᵥ p₀, ⋯⟩ = v