k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
⊢ centroid k s p = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
⊢ centroid k s p = centroid k univ fun x => ↑x
let f : p '' ↑s → ι := fun x => x.property.choose
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
⊢ centroid k s p = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
⊢ centroid k s p = centroid k univ fun x => ↑x
have hf : ∀ x, f x ∈ s ∧ p (f x) = x := fun x => x.property.choose_spec
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
⊢ centroid k s p = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
⊢ centroid k s p = centroid k univ fun x => ↑x
let f' : ps → ι := fun x => f ⟨x, hps ▸ x.property⟩
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
⊢ centroid k s p = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
⊢ centroid k s p = centroid k univ fun x => ↑x
have hf' : ∀ x, f' x ∈ s ∧ p (f' x) = x := fun x => hf ⟨x, hps ▸ x.property⟩
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
⊢ centroid k s p = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
⊢ centroid k s p = centroid k univ fun x => ↑x
have hf'i : Function.Injective f' := by
  intro x y h
  rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
⊢ centroid k s p = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
⊢ centroid k s p = centroid k univ fun x => ↑x
let f'e : ps ↪ ι := ⟨f', hf'i⟩
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k univ (p ∘ ↑f'e) = centroid k univ fun x => ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k s p = centroid k univ fun x => ↑x
rw [← hu, centroid_map]
case e_p.h
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : ↑ps
⊢ (p ∘ ↑f'e) x = ↑x
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k univ (p ∘ ↑f'e) = centroid k univ fun x => ↑x
congr with x
case e_p.h
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : ↑ps
⊢ p (f' x) = ↑x
case e_p.h
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : ↑ps
⊢ (p ∘ ↑f'e) x = ↑x
change p (f' x) = ↑x
no goals
case e_p.h
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : ↑ps
⊢ p (f' x) = ↑x
rw [(hf' x).2]
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ x = y
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
⊢ Function.Injective f'
intro x y h
no goals
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ x = y
rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
case a
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ map f'e univ ↔ x ∈ s
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
⊢ map f'e univ = s
ext x
case a
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ a, a ∈ univ ∧ ↑f'e a = x) ↔ x ∈ s
case a
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ map f'e univ ↔ x ∈ s
rw [mem_map]
case a.mp
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ a, a ∈ univ ∧ ↑f'e a = x) → x ∈ s

case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ s → ∃ a, a ∈ univ ∧ ↑f'e a = x
case a
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ a, a ∈ univ ∧ ↑f'e a = x) ↔ x ∈ s
constructor
case a.mp.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
i : ↑ps
left✝ : i ∈ univ
⊢ ↑f'e i ∈ s
case a.mp
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ a, a ∈ univ ∧ ↑f'e a = x) → x ∈ s
rintro ⟨i, _, rfl⟩
no goals
case a.mp.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
i : ↑ps
left✝ : i ∈ univ
⊢ ↑f'e i ∈ s
exact (hf' i).1
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ∃ a, a ∈ univ ∧ ↑f'e a = x
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ s → ∃ a, a ∈ univ ∧ ↑f'e a = x
intro hx
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ↑f'e { val := p x, property := (_ : p x ∈ ps) } = x
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ∃ a, a ∈ univ ∧ ↑f'e a = x
use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ p (f' { val := p x, property := (_ : p x ∈ ps) }) = p x
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ↑f'e { val := p x, property := (_ : p x ∈ ps) } = x
refine' hi _ (hf' _).1 _ hx _
no goals
case a.mpr
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.521615
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ p (f' { val := p x, property := (_ : p x ∈ ps) }) = p x
rw [(hf' _).2]