[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
⊢ affineSpan k (range id) = ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
f g : AffineBasis ι k P
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
g : AffineBasis ι k P
toFun✝ : ι → P
ind'✝ : AffineIndependent k toFun✝
tot'✝ : affineSpan k (range toFun✝) = ⊤
h : { toFun := toFun✝, ind' := ind'✝, tot' := tot'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, ind' := ind'✝, tot' := tot'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
toFun✝¹ : ι → P
ind'✝¹ : AffineIndependent k toFun✝¹
tot'✝¹ : affineSpan k (range toFun✝¹) = ⊤
toFun✝ : ι → P
ind'✝ : AffineIndependent k toFun✝
tot'✝ : affineSpan k (range toFun✝) = ⊤
h : { toFun := toFun✝¹, ind' := ind'✝¹, tot' := tot'✝¹ }.toFun = { toFun := toFun✝, ind' := ind'✝, tot' := tot'✝ }.toFun
⊢ { toFun := toFun✝¹, ind' := ind'✝¹, tot' := tot'✝¹ } = { toFun := toFun✝, ind' := ind'✝, tot' := tot'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
hι : IsEmpty ι
⊢ False
[PROOFSTEP]
simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e✝ e : ι ≃ ι'
⊢ affineSpan k (range (↑b ∘ ↑e.symm)) = ⊤
[PROOFSTEP]
rw [e.symm.surjective.range_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e✝ e : ι ≃ ι'
⊢ affineSpan k (range ↑b) = ⊤
[PROOFSTEP]
exact b.3
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ ⊤ ≤ Submodule.span k (range fun i_1 => ↑b ↑i_1 -ᵥ ↑b i)
[PROOFSTEP]
suffices Submodule.span k (range fun j : { x // x ≠ i } => b ↑j -ᵥ b i) = vectorSpan k (range b) by
  rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
this : Submodule.span k (range fun j => ↑b ↑j -ᵥ ↑b i) = vectorSpan k (range ↑b)
⊢ ⊤ ≤ Submodule.span k (range fun i_1 => ↑b ↑i_1 -ᵥ ↑b i)
[PROOFSTEP]
rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j => ↑b ↑j -ᵥ ↑b i) = vectorSpan k (range ↑b)
[PROOFSTEP]
conv_rhs => rw [← image_univ]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
| vectorSpan k (range ↑b)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
| vectorSpan k (range ↑b)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
| vectorSpan k (range ↑b)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j => ↑b ↑j -ᵥ ↑b i) = vectorSpan k (↑b '' univ)
[PROOFSTEP]
rw [vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j => ↑b ↑j -ᵥ ↑b i) = Submodule.span k ((fun x => x -ᵥ ↑b i) '' (↑b '' (univ \ {i})))
[PROOFSTEP]
congr
[GOAL]
case e_s
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ (range fun j => ↑b ↑j -ᵥ ↑b i) = (fun x => x -ᵥ ↑b i) '' (↑b '' (univ \ {i}))
[PROOFSTEP]
ext v
[GOAL]
case e_s.h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
v : V
⊢ (v ∈ range fun j => ↑b ↑j -ᵥ ↑b i) ↔ v ∈ (fun x => x -ᵥ ↑b i) '' (↑b '' (univ \ {i}))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
i : ι
j : { j // j ≠ i }
⊢ ↑(basisOf b i) j = ↑b ↑j -ᵥ ↑b i
[PROOFSTEP]
simp [basisOf]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι'
⊢ basisOf (reindex b e) i =
    Basis.reindex (basisOf b (↑e.symm i)) (Equiv.subtypeEquiv e (_ : ∀ (x : ι), ¬x = ↑e.symm i ↔ ¬↑e x = i))
[PROOFSTEP]
ext j
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
i : ι'
j : { j // j ≠ i }
⊢ ↑(basisOf (reindex b e) i) j =
    ↑(Basis.reindex (basisOf b (↑e.symm i)) (Equiv.subtypeEquiv e (_ : ∀ (x : ι), ¬x = ↑e.symm i ↔ ¬↑e x = i))) j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
⊢ (fun q => 1 - ↑(Basis.sumCoords (basisOf b i)) (q -ᵥ ↑b i)) (v +ᵥ q) =
    ↑(-Basis.sumCoords (basisOf b i)) v +ᵥ (fun q => 1 - ↑(Basis.sumCoords (basisOf b i)) (q -ᵥ ↑b i)) q
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
⊢ 1 - ↑(Basis.sumCoords (basisOf b i)) (v +ᵥ q -ᵥ ↑b i) =
    ↑(-Basis.sumCoords (basisOf b i)) v +ᵥ (1 - ↑(Basis.sumCoords (basisOf b i)) (q -ᵥ ↑b i))
[PROOFSTEP]
rw [vadd_vsub_assoc, LinearMap.map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap, add_comm,
  sub_eq_add_neg]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι'
⊢ coord (reindex b e) i = coord b (↑e.symm i)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι'
p✝ : P
⊢ ↑(coord (reindex b e) i) p✝ = ↑(coord b (↑e.symm i)) p✝
[PROOFSTEP]
classical simp [AffineBasis.coord]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι'
p✝ : P
⊢ ↑(coord (reindex b e) i) p✝ = ↑(coord b (↑e.symm i)) p✝
[PROOFSTEP]
simp [AffineBasis.coord]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ ↑(coord b i) (↑b i) = 1
[PROOFSTEP]
simp only [coord, Basis.coe_sumCoords, LinearEquiv.map_zero, LinearEquiv.coe_coe, sub_zero, AffineMap.coe_mk,
  Finsupp.sum_zero_index, vsub_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
h : i ≠ j
⊢ ↑(coord b i) (↑b j) = 0
[PROOFSTEP]
rw [coord, AffineMap.coe_mk, ← @Subtype.coe_mk _ (fun j => j ≠ i) j h.symm, ← b.basisOf_apply,
  Basis.sumCoords_self_apply, sub_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(coord b i) (↑b j) = if i = j then 1 else 0
[PROOFSTEP]
cases' eq_or_ne i j with h h
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : DecidableEq ι
i j : ι
h : i = j
⊢ ↑(coord b i) (↑b j) = if i = j then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ ↑(coord b i) (↑b j) = if i = j then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
hi : i ∈ s
w : ι → k
hw : Finset.sum s w = 1
⊢ ↑(coord b i) (↑(Finset.affineCombination k s ↑b) w) = w i
[PROOFSTEP]
classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_true, mul_boole, hw,
  Function.comp_apply, smul_eq_mul, s.sum_ite_eq, s.map_affineCombination b w hw]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
hi : i ∈ s
w : ι → k
hw : Finset.sum s w = 1
⊢ ↑(coord b i) (↑(Finset.affineCombination k s ↑b) w) = w i
[PROOFSTEP]
simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_true, mul_boole, hw, Function.comp_apply,
  smul_eq_mul, s.sum_ite_eq, s.map_affineCombination b w hw]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
hi : ¬i ∈ s
w : ι → k
hw : Finset.sum s w = 1
⊢ ↑(coord b i) (↑(Finset.affineCombination k s ↑b) w) = 0
[PROOFSTEP]
classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false, mul_boole, hw,
  Function.comp_apply, smul_eq_mul, s.sum_ite_eq, s.map_affineCombination b w hw]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
hi : ¬i ∈ s
w : ι → k
hw : Finset.sum s w = 1
⊢ ↑(coord b i) (↑(Finset.affineCombination k s ↑b) w) = 0
[PROOFSTEP]
simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false, mul_boole, hw,
  Function.comp_apply, smul_eq_mul, s.sum_ite_eq, s.map_affineCombination b w hw]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
have hq : q ∈ affineSpan k (range b) := by
  rw [b.tot]
  exact AffineSubspace.mem_top k V q
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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)
[PROOFSTEP]
rw [b.tot]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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 ∈ ⊤
[PROOFSTEP]
exact AffineSubspace.mem_top k V q
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
convert hw
[GOAL]
case h.e'_2.a
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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✝
[PROOFSTEP]
exact b.coord_apply_combination_of_mem (Finset.mem_univ _) hw
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
have hq : q ∈ affineSpan k (range b) := by
  rw [b.tot]
  exact AffineSubspace.mem_top k V q
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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)
[PROOFSTEP]
rw [b.tot]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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 ∈ ⊤
[PROOFSTEP]
exact AffineSubspace.mem_top k V q
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
congr
[GOAL]
case intro.intro.h.e_6.h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
ext i
[GOAL]
case intro.intro.h.e_6.h.h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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
[PROOFSTEP]
exact b.coord_apply_combination_of_mem (Finset.mem_univ i) hw
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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 ι
b : AffineBasis ι k V
v : V
⊢ ∑ i : ι, ↑(coord b i) v • ↑b i = v
[PROOFSTEP]
have hb := b.affineCombination_coord_eq_self v
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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 ι
b : AffineBasis ι k V
v : V
hb : (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) v) = v
⊢ ∑ i : ι, ↑(coord b i) v • ↑b i = v
[PROOFSTEP]
rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb 
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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₂
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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₂
[PROOFSTEP]
rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
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₂
[PROOFSTEP]
simp only [h]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
⊢ ↑(coord b i) = 1
[PROOFSTEP]
ext q
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
have hp : (range b).Subsingleton := by
  rw [← image_univ]
  apply Subsingleton.image
  apply subsingleton_of_subsingleton
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton (range ↑b)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton (↑b '' univ)
[PROOFSTEP]
apply Subsingleton.image
[GOAL]
case hs
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton univ
[PROOFSTEP]
apply subsingleton_of_subsingleton
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
haveI := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
let s : Finset ι := { i }
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
have hi : i ∈ s := by simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
⊢ i ∈ s
[PROOFSTEP]
simp
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ Finset.sum s (Function.const ι 1) = 1
[PROOFSTEP]
simp
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Finset.sum s (Function.const ι 1) = 1
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Finset.sum s (Function.const ι 1) = 1
⊢ q = ↑(Finset.affineCombination k s ↑b) (Function.const ι 1)
[PROOFSTEP]
simp
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton (range ↑b)
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Finset.sum s (Function.const ι 1) = 1
hq : q = ↑(Finset.affineCombination k s ↑b) (Function.const ι 1)
⊢ ↑(coord b i) q = OfNat.ofNat 1 q
[PROOFSTEP]
rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ↑(coord b i)
[PROOFSTEP]
classical
intro x
obtain ⟨j, hij⟩ := exists_ne i
let s : Finset ι := { i, j }
have hi : i ∈ s := by simp
have _ : j ∈ s := by simp
let w : ι → k := fun j' => if j' = i then x else 1 - x
have hw : s.sum w = 1 := by
  -- Porting note: previously this subgoal worked just by:
        -- simp [hij, Finset.sum_ite, Finset.filter_insert, Finset.filter_eq']
        -- I'm not sure why `simp` can not successfully use `Finset.filter_eq'`.
  simp [Finset.sum_ite, Finset.filter_insert, hij]
  erw [Finset.filter_eq']
  simp [hij.symm]
use s.affineCombination k b w
simp [b.coord_apply_combination_of_mem hi hw]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ↑(coord b i)
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
obtain ⟨j, hij⟩ := exists_ne i
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
let s : Finset ι := { i, j }
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
have hi : i ∈ s := by simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ i ∈ s
[PROOFSTEP]
simp
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
have _ : j ∈ s := by simp
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ j ∈ s
[PROOFSTEP]
simp
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
let w : ι → k := fun j' => if j' = i then x else 1 - x
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
have hw : s.sum w = 1 := by
  -- Porting note: previously this subgoal worked just by:
        -- simp [hij, Finset.sum_ite, Finset.filter_insert, Finset.filter_eq']
        -- I'm not sure why `simp` can not successfully use `Finset.filter_eq'`.
  simp [Finset.sum_ite, Finset.filter_insert, hij]
  erw [Finset.filter_eq']
  simp [hij.symm]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ Finset.sum s w = 1
[PROOFSTEP]
simp [Finset.sum_ite, Finset.filter_insert, hij]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ ↑(Finset.card (insert i (Finset.filter (fun x => x = i) {j}))) * x + (1 - x) = 1
[PROOFSTEP]
erw [Finset.filter_eq']
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ ↑(Finset.card (insert i (if i ∈ {j} then {i} else ∅))) * x + (1 - x) = 1
[PROOFSTEP]
simp [hij.symm]
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
hw : Finset.sum s w = 1
⊢ ∃ a, ↑(coord b i) a = x
[PROOFSTEP]
use s.affineCombination k b w
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s✝ : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
hw : Finset.sum s w = 1
⊢ ↑(coord b i) (↑(Finset.affineCombination k s ↑b) w) = x
[PROOFSTEP]
simp [b.coord_apply_combination_of_mem hi hw]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
v w : V
⊢ (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v + (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
v w : V
i : ι
⊢ (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) i =
    ((fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v + (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) i
[PROOFSTEP]
simp only [LinearMap.map_add, Pi.add_apply, neg_add]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
t : k
v : V
⊢ AddHom.toFun
      { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
        map_add' :=
          (_ :
            ∀ (v w : V),
              (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
      (t • v) =
    ↑(RingHom.id k) t •
      AddHom.toFun
        { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
          map_add' :=
            (_ :
              ∀ (v w : V),
                (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
        v
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
t : k
v : V
i : ι
⊢ AddHom.toFun
      { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
        map_add' :=
          (_ :
            ∀ (v w : V),
              (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
      (t • v) i =
    (↑(RingHom.id k) t •
        AddHom.toFun
          { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
            map_add' :=
              (_ :
                ∀ (v w : V),
                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                      (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
          v)
      i
[PROOFSTEP]
simp only [LinearMap.map_smul, Pi.smul_apply, smul_neg, RingHom.id_apply, mul_neg]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
p : P
v : V
⊢ (fun q i => ↑(coord b i) q) (v +ᵥ p) =
    ↑{
            toAddHom :=
              { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
                map_add' :=
                  (_ :
                    ∀ (v w : V),
                      (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                        (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                          (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) },
            map_smul' :=
              (_ :
                ∀ (t : k) (v : V),
                  AddHom.toFun
                      { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
                        map_add' :=
                          (_ :
                            ∀ (v w : V),
                              (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                                (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
                      (t • v) =
                    ↑(RingHom.id k) t •
                      AddHom.toFun
                        { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
                          map_add' :=
                            (_ :
                              ∀ (v w : V),
                                (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                                    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
                        v) }
        v +ᵥ
      (fun q i => ↑(coord b i) q) p
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
p : P
v : V
i : ι
⊢ (fun q i => ↑(coord b i) q) (v +ᵥ p) i =
    (↑{
              toAddHom :=
                { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
                  map_add' :=
                    (_ :
                      ∀ (v w : V),
                        (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                          (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                            (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) },
              map_smul' :=
                (_ :
                  ∀ (t : k) (v : V),
                    AddHom.toFun
                        { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
                          map_add' :=
                            (_ :
                              ∀ (v w : V),
                                (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                                    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
                        (t • v) =
                      ↑(RingHom.id k) t •
                        AddHom.toFun
                          { toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
                            map_add' :=
                              (_ :
                                ∀ (v w : V),
                                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                                    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                                      (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
                          v) }
          v +ᵥ
        (fun q i => ↑(coord b i) q) p)
      i
[PROOFSTEP]
rw [LinearMap.coe_mk, Pi.vadd_apply']
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
p : P
v : V
i : ι
⊢ (fun q i => ↑(coord b i) q) (v +ᵥ p) i =
    ↑{ toFun := fun v i => -↑(Basis.sumCoords (basisOf b i)) v,
            map_add' :=
              (_ :
                ∀ (v w : V),
                  (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) (v + w) =
                    (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) v +
                      (fun v i => -↑(Basis.sumCoords (basisOf b i)) v) w) }
        v i +ᵥ
      (fun q i => ↑(coord b i) q) p i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
p : P
v : V
i : ι
⊢ ↑(coord b i) (v +ᵥ p) = (-Finsupp.sum (↑(basisOf b i).repr v) fun x => id) + ↑(coord b i) p
[PROOFSTEP]
rw [AffineMap.map_vadd, linear_eq_sumCoords, LinearMap.neg_apply]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
p : P
v : V
i : ι
⊢ -↑(Basis.sumCoords (basisOf b i)) v +ᵥ ↑(coord b i) p =
    (-Finsupp.sum (↑(basisOf b i).repr v) fun x => id) + ↑(coord b i) p
[PROOFSTEP]
simp only [ne_eq, Basis.coe_sumCoords, vadd_eq_add]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ ↑(coord b i) (Finset.centroid k s ↑b) = (↑(Finset.card s))⁻¹
[PROOFSTEP]
rw [Finset.centroid, b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
  Finset.centroidWeights, Function.const_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
⊢ ∃ s x b, ↑b = Subtype.val
[PROOFSTEP]
obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ ∃ s x b, ↑b = Subtype.val
[PROOFSTEP]
refine' ⟨s, hst, ⟨(↑), h_ind, _⟩, rfl⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ affineSpan k (range Subtype.val) = ⊤
[PROOFSTEP]
rw [Subtype.range_coe, h_tot, ht]
