case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ WSameSide (AffineSubspace.map f s) (↑f x) (↑f y)
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
h : WSameSide s x y
f : P →ᵃ[R] P'
⊢ WSameSide (AffineSubspace.map f s) (↑f x) (↑f y)
rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (↑f x -ᵥ ↑f p₁) (↑f y -ᵥ ↑f p₂)
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ WSameSide (AffineSubspace.map f s) (↑f x) (↑f y)
refine' ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, _⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (↑f.linear (x -ᵥ p₁)) (↑f.linear (y -ᵥ p₂))
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (↑f x -ᵥ ↑f p₁) (↑f y -ᵥ ↑f p₂)
simp_rw [← linearMap_vsub]
no goals
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (↑f.linear (x -ᵥ p₁)) (↑f.linear (y -ᵥ p₂))
exact h.map f.linear