-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem affineCombination_coord_eq_self [Fintype ι] (q : P) :
    (Finset.univ.affineCombination k b fun i => b.coord i q) = q

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
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q

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)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q

Proof state:
case intro.intro.h.e_6.h
ι : 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)
⊢ (fun i => (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w)) = w

Tactic:
ext i

Result:
case intro.intro.h.e_6.h.h
ι : 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) = w i

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:
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)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w)) =
    (Finset.affineCombination k Finset.univ ⇑b) w

Tactic:
congr

Result:
case intro.intro.h.e_6.h
ι : 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)
⊢ (fun i => (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w)) = w

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)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q

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)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w)) =
    (Finset.affineCombination k Finset.univ ⇑b) w

Proof state:
case intro.intro.h.e_6.h.h
ι : 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) = w i

Tactic:
exact b.coord_apply_combination_of_mem (Finset.mem_univ i) 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 ∈ ⊤