k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑(restrict φ hEF) x = ↑(restrict φ hEF) y
⊢ x = y
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ Function.Injective ↑(restrict φ hEF)
intro x y h
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑φ ↑x = ↑φ ↑y
⊢ ↑x = ↑y
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑(restrict φ hEF) x = ↑(restrict φ hEF) y
⊢ x = y
simp only [Subtype.ext_iff, Subtype.coe_mk, AffineMap.restrict.coe_apply] at h⊢
no goals
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑φ ↑x = ↑φ ↑y
⊢ ↑x = ↑y
exact hφ h