-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) :
    (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (fun z => o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ ↑π
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
have hx : (x, y) ∈ s := by
  convert Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)
  simp

Result:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (fun z => o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ ↑π
hx : (x, y) ∈ s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
r' : ℝ
⊢ o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π

Tactic:
rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)

Result:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ

Result:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
⊢ ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π

Tactic:
intro r'

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
r' : ℝ
⊢ o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π

Proof state:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
⊢ (x, r' • x + y).2 ≠ 0

Tactic:
simp only [Prod.fst, Prod.snd]

Result:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
⊢ r' • x + y ≠ 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
by_cases h : o.oangle x y = 0 ∨ o.oangle x y = π

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : o.oangle x y = 0 ∨ o.oangle x y = ↑π
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (fun z => o.oangle z.1 z.2) s
⊢ ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ ↑π

Tactic:
intro z hz

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (fun z => o.oangle z.1 z.2) s
z : V × V
hz : z ∈ s
⊢ o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ ↑π

Proof state:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : z ∈ s
⊢ z.2 ≠ 0

Tactic:
simp_rw [s, Set.mem_image] at hz

Result:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' => (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : ∃ x_1 ∈ Set.univ, (x, x_1 • x + y) = z
⊢ z.2 ≠ 0