k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
have : s = Set.range ((↑) : s → P) := by simp
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
conv_rhs =>
  rw [this]
no goals
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)
apply le_antisymm
  <;> intro q hq
  <;> erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
  <;> obtain ⟨t, μ, rfl⟩ := hq
  <;> use t
  <;> [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]
  <;> simp [smul_smul]
no goals
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
⊢ s = Set.range Subtype.val
simp