case intro
ι : Type u_1
ι' : Type ?u.127186
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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), ↑(coord b i) q₁ = ↑(coord b i) q₂
val✝ : Fintype ι
⊢ q₁ = q₂
ι : Type u_1
ι' : Type ?u.127186
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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), ↑(coord b i) q₁ = ↑(coord b i) q₂
⊢ q₁ = q₂
cases nonempty_fintype ι
case intro
ι : Type u_1
ι' : Type ?u.127186
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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), ↑(coord b i) q₁ = ↑(coord b i) q₂
val✝ : Fintype ι
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q₁) =
    ↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q₂
case intro
ι : Type u_1
ι' : Type ?u.127186
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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), ↑(coord b i) q₁ = ↑(coord b i) q₂
val✝ : Fintype ι
⊢ q₁ = q₂
rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]
no goals
case intro
ι : Type u_1
ι' : Type ?u.127186
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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), ↑(coord b i) q₁ = ↑(coord b i) q₂
val✝ : Fintype ι
⊢ (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q₁) =
    ↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) q₂
simp only [h]