k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
⊢ AffineIndependent k fun x => ↑x
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
⊢ AffineIndependent k fun x => ↑x
let f : Set.range p → ι := fun x => x.property.choose
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ AffineIndependent k fun x => ↑x
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
⊢ AffineIndependent k fun x => ↑x
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k 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₂) }
⊢ AffineIndependent k fun x => ↑x
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ AffineIndependent k fun x => ↑x
let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
case h.e'_9.h.h.e
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k 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✝ : ↑(Set.range p)
⊢ Subtype.val = p ∘ ↑fe
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k 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₂) }
⊢ AffineIndependent k fun x => ↑x
convert ha.comp_embedding fe
case h.e'_9.h.h.e.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k 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✝¹ : ↑(Set.range p)
x✝ : { x // x ∈ Set.range p }
⊢ ↑x✝ = (p ∘ ↑fe) x✝
case h.e'_9.h.h.e
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k 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✝ : ↑(Set.range p)
⊢ Subtype.val = p ∘ ↑fe
ext
no goals
case h.e'_9.h.h.e.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k 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✝¹ : ↑(Set.range p)
x✝ : { x // x ∈ Set.range p }
⊢ ↑x✝ = (p ∘ ↑fe) x✝
simp [hf]