no goals
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ↑(coord b i)
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
    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]
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
⊢ ∃ a, ↑(coord b i) a = x
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ↑(coord b i)
intro x
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
⊢ ∃ a, ↑(coord b i) a = x
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
⊢ ∃ a, ↑(coord b i) a = x
obtain ⟨j, hij⟩ := exists_ne i
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ a, ↑(coord b i) a = x
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
⊢ ∃ a, ↑(coord b i) a = x
let s : Finset ι := {i, j}
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ ∃ a, ↑(coord b i) a = x
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ a, ↑(coord b i) a = x
have hi : i ∈ s := by simp
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
⊢ ∃ a, ↑(coord b i) a = x
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ ∃ a, ↑(coord b i) a = x
have _ : j ∈ s := by simp
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
x✝ : j ∈ s
⊢ ∃ a, ↑(coord b i) a = x
let w : ι → k := fun j' => if j' = i then x else 1 - x
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
have hw : s.sum w = 1 := by
  simp [Finset.sum_ite, Finset.filter_insert, hij]
  erw [Finset.filter_eq']
  simp [hij.symm]
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
use s.affineCombination k b w
no goals
case intro
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
simp [b.coord_apply_combination_of_mem hi hw]
no goals
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ i ∈ s
simp
no goals
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ j ∈ s
simp
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
simp [Finset.sum_ite, Finset.filter_insert, hij]
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
erw [Finset.filter_eq']
no goals
ι : Type u_1
ι' : Type ?u.141682
k : Type u_3
V : Type u_4
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✝ : 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
simp [hij.symm]