case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
ext q
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
have hp : (range b).Subsingleton := by
  rw [← image_univ]
  apply Subsingleton.image
  apply subsingleton_of_subsingleton
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
haveI := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
let s : Finset ι := {i}
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
have hi : i ∈ s := by simp
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by simp
no goals
case h
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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)
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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)
rw [← image_univ]
case hs
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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)
apply Subsingleton.image
no goals
case hs
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
apply subsingleton_of_subsingleton
no goals
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
simp
no goals
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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
simp
no goals
ι : Type u_1
ι' : Type ?u.129150
k : Type u_2
V : Type u_4
P : Type u_3
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)
simp