k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
⊢ AffineIndependent k (p ∘ ↑e) → AffineIndependent k p
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
⊢ AffineIndependent k (p ∘ ↑e) ↔ AffineIndependent k p
refine' ⟨_, AffineIndependent.comp_embedding e.toEmbedding⟩
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
⊢ AffineIndependent k p
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
⊢ AffineIndependent k (p ∘ ↑e) → AffineIndependent k p
intro h
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
this : p = p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)
⊢ AffineIndependent k p
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
⊢ AffineIndependent k p
have : p = p ∘ e ∘ e.symm.toEmbedding := by
  ext
  simp
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
this : p = p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)
⊢ AffineIndependent k (p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm))
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
this : p = p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)
⊢ AffineIndependent k p
rw [this]
no goals
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
this : p = p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)
⊢ AffineIndependent k (p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm))
exact h.comp_embedding e.symm.toEmbedding
case h
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
x✝ : ι'
⊢ p x✝ = (p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)) x✝
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
⊢ p = p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)
ext
no goals
case h
k : Type u_3
V : Type u_4
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
ι' : Type u_1
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ↑e)
x✝ : ι'
⊢ p x✝ = (p ∘ ↑e ∘ ↑(Equiv.toEmbedding e.symm)) x✝
simp