ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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)
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q) = q
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q) = q
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.118805
k : Type u_4
V : Type u_3
P : Type u_2
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)
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i =>
      ↑(coord b i) (↑(Finset.affineCombination k Finset.univ ↑b) w)) =
    ↑(Finset.affineCombination k Finset.univ ↑b) w
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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)
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q) = q
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
case intro.intro.h.e_6.h
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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)
⊢ (fun i => ↑(coord b i) (↑(Finset.affineCombination k Finset.univ ↑b) w)) = w
case intro.intro
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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)
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i =>
      ↑(coord b i) (↑(Finset.affineCombination k Finset.univ ↑b) w)) =
    ↑(Finset.affineCombination k Finset.univ ↑b) w
congr
case intro.intro.h.e_6.h.h
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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) = w i
case intro.intro.h.e_6.h
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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)
⊢ (fun i => ↑(coord b i) (↑(Finset.affineCombination k Finset.univ ↑b) w)) = w
ext i
no goals
case intro.intro.h.e_6.h.h
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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) = w i
exact b.coord_apply_combination_of_mem (Finset.mem_univ i) hw
ι : Type u_1
ι' : Type ?u.118805
k : Type u_4
V : Type u_3
P : Type u_2
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.118805
k : Type u_4
V : Type u_3
P : Type u_2
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.118805
k : Type u_4
V : Type u_3
P : Type u_2
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