ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ↑b)
⊢ ∑ i : ι, ↑(coord b i) q = 1
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
q : P
⊢ ∑ i : ι, ↑(coord b i) q = 1
have hq : q ∈ affineSpan k (range b) := by
  rw [b.tot]
  exact AffineSubspace.mem_top k V q
case intro.intro
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
w : ι → k
hw : ∑ i : ι, w i = 1
hq : ↑(Finset.affineCombination k Finset.univ ↑b) w ∈ affineSpan k (range ↑b)
⊢ ∑ i : ι, ↑(coord b i) (↑(Finset.affineCombination k Finset.univ ↑b) w) = 1
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ↑b)
⊢ ∑ i : ι, ↑(coord b i) q = 1
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
case h.e'_2.a
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
w : ι → k
hw : ∑ i : ι, w i = 1
hq : ↑(Finset.affineCombination k Finset.univ ↑b) w ∈ affineSpan k (range ↑b)
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ↑(coord b x✝) (↑(Finset.affineCombination k Finset.univ ↑b) w) = w x✝
case intro.intro
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
w : ι → k
hw : ∑ i : ι, w i = 1
hq : ↑(Finset.affineCombination k Finset.univ ↑b) w ∈ affineSpan k (range ↑b)
⊢ ∑ i : ι, ↑(coord b i) (↑(Finset.affineCombination k Finset.univ ↑b) w) = 1
convert hw
no goals
case h.e'_2.a
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
w : ι → k
hw : ∑ i : ι, w i = 1
hq : ↑(Finset.affineCombination k Finset.univ ↑b) w ∈ affineSpan k (range ↑b)
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ↑(coord b x✝) (↑(Finset.affineCombination k Finset.univ ↑b) w) = w x✝
exact b.coord_apply_combination_of_mem (Finset.mem_univ _) hw
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
q : P
⊢ q ∈ ⊤
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
q : P
⊢ q ∈ affineSpan k (range ↑b)
rw [b.tot]
no goals
ι : Type u_1
ι' : Type ?u.112987
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
q : P
⊢ q ∈ ⊤
exact AffineSubspace.mem_top k V q