-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem sum_coord_apply_eq_one [Fintype ι] (q : P) : ∑ i, b.coord i q = 1

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ⇑b)
⊢ ∑ i : ι, (b.coord i) q = 1

Tactic:
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq

Result:
case intro.intro
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
w : ι → k
hw : ∑ i : ι, w i = 1
hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)
⊢ ∑ i : ι, (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w) = 1

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
⊢ q ∈ ⊤

Tactic:
exact AffineSubspace.mem_top k V q

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
⊢ ∑ i : ι, (b.coord i) q = 1

Tactic:
have hq : q ∈ affineSpan k (range b) := by
  rw [b.tot]
  exact AffineSubspace.mem_top k V q

Result:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ⇑b)
⊢ ∑ i : ι, (b.coord i) q = 1

Proof state:
case intro.intro
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
w : ι → k
hw : ∑ i : ι, w i = 1
hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)
⊢ ∑ i : ι, (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w) = 1

Tactic:
convert hw

Result:
case h.e'_2.a
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
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
⊢ (b.coord x✝) ((Finset.affineCombination k Finset.univ ⇑b) w) = w x✝

Proof state:
case h.e'_2.a
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
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
⊢ (b.coord x✝) ((Finset.affineCombination k Finset.univ ⇑b) w) = w x✝

Tactic:
exact b.coord_apply_combination_of_mem (Finset.mem_univ _) hw

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
⊢ q ∈ affineSpan k (range ⇑b)

Tactic:
rw [b.tot]

Result:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
⊢ q ∈ ⊤