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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∃ x_1, p x x_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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ p x h
refine' Exists.elim _ fun (hx : x ∈ affineSpan k s) (hc : p x hx) => hc
case 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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∀ (x : P), x ∈ s → (fun y => ∃ z, p y z) x

case 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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (fun y => ∃ z, p y z) u →
      (fun y => ∃ z, p y z) v → (fun y => ∃ z, p y z) w → (fun y => ∃ z, p y z) (c • (u -ᵥ v) +ᵥ w)
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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∃ x_1, p x x_1
refine' @affineSpan_induction k V P _ _ _ _ _ _ (fun y => ∃ z, p y z) h _ _
no goals
case 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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∀ (x : P), x ∈ s → (fun y => ∃ z, p y z) x
exact fun y hy => ⟨subset_affineSpan _ _ hy, Hs y hy⟩
no goals
case 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.343274
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (fun y => ∃ z, p y z) u →
      (fun y => ∃ z, p y z) v → (fun y => ∃ z, p y z) w → (fun y => ∃ z, p y z) (c • (u -ᵥ v) +ᵥ w)
exact fun c u v w hu hv hw =>
  Exists.elim hu fun hu' hu =>
    Exists.elim hv fun hv' hv =>
      Exists.elim hw fun hw' hw =>
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw', Hc _ _ _ _ _ _ _ hu hv hw⟩