k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤
rw [eq_top_iff]
case mk
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
⊢ { val := x, property := hx } ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)
rintro ⟨x, hx⟩ -
case mk.refine'_1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
y : P
hy : y ∈ A
⊢ (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) y (_ : y ∈ ↑(affineSpan k A))

case mk.refine'_2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) u hu →
    (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) v hv →
      (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) w hw →
        (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) (c • (u -ᵥ v) +ᵥ w)
          (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k A).carrier)
case mk
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
⊢ { val := x, property := hx } ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
refine' affineSpan_induction' (fun y hy => _) (fun c u hu v hv w hw => _) hx
    (p := fun y hy => ⟨y, hy⟩ ∈ (affineSpan k (((↑) : {z // z ∈ affineSpan k A} → P) ⁻¹' A)))
no goals
case mk.refine'_1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
y : P
hy : y ∈ A
⊢ (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) y (_ : y ∈ ↑(affineSpan k A))
exact subset_affineSpan _ _ hy
no goals
case mk.refine'_2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.347568
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) u hu →
    (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) v hv →
      (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) w hw →
        (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) (c • (u -ᵥ v) +ᵥ w)
          (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k A).carrier)
exact AffineSubspace.smul_vsub_vadd_mem _ _