-- Mathlib/Analysis/Convex/Side.lean
theorem _root_.Function.Injective.wSameSide_map_iff {s : AffineSubspace R P} {x y : P}
    {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    (s.map f).WSameSide (f x) (f y) ↔ s.WSameSide x y

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
⊢ (map f s).WSameSide (f x) (f y) ↔ s.WSameSide x y

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩

Result:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
h : (map f s).WSameSide (f x) (f y)
⊢ s.WSameSide x y

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ f p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
simp_rw [← linearMap_vsub, (f.linear_injective_iff.2 hf).sameRay_map_iff] at h

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : fp₁ ∈ map f s
fp₂ : P'
hfp₂ : fp₂ ∈ map f s
h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y

Tactic:
rw [mem_map] at hfp₁ hfp₂

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : ∃ y ∈ s, f y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
p₁ : P
hp₁ : p₁ ∈ s
h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y

Tactic:
rcases hfp₂ with ⟨p₂, hp₂, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ f p₂)
⊢ s.WSameSide x y

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
h : (map f s).WSameSide (f x) (f y)
⊢ s.WSameSide x y

Tactic:
rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : fp₁ ∈ map f s
fp₂ : P'
hfp₂ : fp₂ ∈ map f s
h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ f p₂)
⊢ s.WSameSide x y

Tactic:
refine ⟨p₁, hp₁, p₂, hp₂, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ f p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : ∃ y ∈ s, f y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y

Tactic:
rcases hfp₁ with ⟨p₁, hp₁, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
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'
hf : Function.Injective ⇑f
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
p₁ : P
hp₁ : p₁ ∈ s
h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y