-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem surjective_coord [Nontrivial ι] (i : ι) : Function.Surjective <| b.coord i

Proof state:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ ∃ a, (b.coord i) a = x

Tactic:
let w : ι → k := fun j' => if j' = i then x else 1 - x

Result:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ ∃ a, (b.coord i) a = x

Proof state:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
hw : s.sum w = 1
⊢ ∃ a, (b.coord i) a = x

Tactic:
use s.affineCombination k b w

Result:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = x

Proof state:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = x

Tactic:
simp [w, b.coord_apply_combination_of_mem hi 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ i ∈ s

Tactic:
simp [s]

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✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ⇑(b.coord i)

Tactic:
intro x

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✝ : Nontrivial ι
i : ι
x : k
⊢ ∃ a, (b.coord i) a = x

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✝ : Nontrivial ι
i : ι
x : k
⊢ ∃ a, (b.coord i) a = x

Tactic:
obtain ⟨j, hij⟩ := exists_ne i

Result:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
⊢ ∃ a, (b.coord i) a = x

Proof state:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ ∃ a, (b.coord i) a = x

Tactic:
have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
  Finset.filter_true_of_mem, Finset.filter_false_of_mem]

Result:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
hw : s.sum w = 1
⊢ ∃ a, (b.coord i) a = x

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✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ⇑(b.coord i)

Tactic:
classical
  intro x
  obtain ⟨j, hij⟩ := exists_ne i
  let s : Finset ι := {i, j}
  have hi : i ∈ s := by simp [s]
  let w : ι → k := fun j' => if j' = i then x else 1 - x
  have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
    Finset.filter_true_of_mem, Finset.filter_false_of_mem]
  use s.affineCombination k b w
  simp [w, b.coord_apply_combination_of_mem hi hw]

Result:
no goals

Proof state:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ a, (b.coord i) a = x

Tactic:
have hi : i ∈ s := by simp [s]

Result:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ ∃ a, (b.coord i) a = x

Proof state:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
⊢ ∃ a, (b.coord i) a = x

Tactic:
let s : Finset ι := {i, j}

Result:
case 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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ a, (b.coord i) a = x

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✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' => if j' = i then x else 1 - x
⊢ s.sum w = 1

Tactic:
simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
Finset.filter_true_of_mem, Finset.filter_false_of_mem]

Result:
no goals