-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top {s : Set V} (p : P)
    (h : Submodule.span k (Set.range ((↑) : s → V)) = ⊤) :
    affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤

Proof state:
case convert_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ Submodule.span k (range Subtype.val) ≤ Submodule.span k ((fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s))

Tactic:
apply Submodule.span_mono

Result:
case convert_1.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ range Subtype.val ⊆ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)

Proof state:
case convert_1.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ range Subtype.val ⊆ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)

Tactic:
rintro v ⟨v', rfl⟩

Result:
case convert_1.h.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' ∈ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)

Proof state:
case convert_1.h.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' ∈ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)

Tactic:
use (v' : V) +ᵥ p

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' +ᵥ p ∈ {p} ∪ (fun v => v +ᵥ p) '' s ∧ (fun x => x -ᵥ p) (↑v' +ᵥ p) = ↑v'

Proof state:
case convert_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ (affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s)).direction = ⊤.direction

Tactic:
rw [direction_affineSpan, direction_top,
  vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ (Set.mem_singleton _) : p ∈ _),
  eq_top_iff, ← h]

Result:
case convert_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ Submodule.span k (range Subtype.val) ≤ Submodule.span k ((fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s))

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' +ᵥ p ∈ {p} ∪ (fun v => v +ᵥ p) '' s ∧ (fun x => x -ᵥ p) (↑v' +ᵥ p) = ↑v'

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤

Tactic:
convert ext_of_direction_eq _
    ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩

Result:
case convert_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ (affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s)).direction = ⊤.direction