-- 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₀})
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

Tactic:
have h := v.property

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 : ↑v ∈ Submodule.span k {p -ᵥ p₀}
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

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

Tactic:
rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]

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₀} ⊔ s.direction) ≤ 1 + finrank k ↥s.direction

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₀}) ≤ 1

Tactic:
refine finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => ?_

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₀})
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

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))
⊢ False

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

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

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))
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

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

Tactic:
exact hf (Submodule.finiteDimensional_of_le h')

Result:
no goals