𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
⊢ ConvexIndependent 𝕜 Subtype.val
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 Subtype.val
let f : Set.range p → ι := fun x => x.property.choose
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ ConvexIndependent 𝕜 Subtype.val
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
⊢ ConvexIndependent 𝕜 Subtype.val
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
⊢ ConvexIndependent 𝕜 Subtype.val
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ ConvexIndependent 𝕜 Subtype.val
let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
case h.e'_7
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
⊢ Subtype.val = p ∘ ↑fe
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
⊢ ConvexIndependent 𝕜 Subtype.val
convert hc.comp_embedding fe
case h.e'_7.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
x✝ : { x // x ∈ Set.range p }
⊢ ↑x✝ = (p ∘ ↑fe) x✝
case h.e'_7
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
⊢ Subtype.val = p ∘ ↑fe
ext
no goals
case h.e'_7.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
x✝ : { x // x ∈ Set.range p }
⊢ ↑x✝ = (p ∘ ↑fe) x✝
rw [Embedding.coeFn_mk, comp_apply, hf]