awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h₁ : m 0 • x + m 1 • y = 0
h0₁ : m 0 - 0 * r = 0
⊢ m 1 = 0

Tactic:
rw [h1] at h0 hm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - 0 * r = 0
h1 : m 1 = 0
⊢ m 0 = 0

Tactic:
rw [zero_mul, sub_zero] at h0

Premises used: sub_zero, MulZeroClass.zero_mul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - 0 * r = 0
h1 : m 1 = 0
h0₁ : m 0 = 0
⊢ m 1 = 0

Tactic:
rw [zero_mul, sub_zero] at h0

Premises used: sub_zero, MulZeroClass.zero_mul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 = 0
h1 : m 1 = 0
⊢ False

Tactic:
simp [h0] at hm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
pos : ∀ (h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)), (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
neg :
  ∀ (h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))), (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
⊢ (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 = π

Premises used: Orientation.oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
pos : (o.oangle x (r • x + y)).sign = 0
pos₁ : o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = (↑π : Real.Angle)
pos₂ pos₃ pos₄ pos₅ : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff,
      oangle_smul_add_right_eq_zero_or_eq_pi_iff]

Premises used: Iff.mpr, Real.Angle.sign_eq_zero_iff, Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
r' : ℝ
rwa :
  ∀ (h : ¬(o.oangle x (r' • x + y) = 0 ∨ o.oangle x (r' • x + y) = (↑π : Real.Angle))),
    o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : ¬o.oangle x (r' • x + y) = 0 ∧ ¬o.oangle x (r' • x + y) = (↑π : Real.Angle)),
    o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
⊢ o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)

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

Premises used: not_or, Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
⊢ ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)

Tactic:
have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := by
    intro r'
    rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
⊢ ContinuousOn.{0, u_1} (Y := V × V) (fun (r' : ℝ) ↦ (x, r' • x + y)) Set.univ

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
⊢ IsConnected s

Tactic:
have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
⊢ ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s

Tactic:
continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_

Premises used: continuousOn_of_forall_continuousAt, Orientation.continuousAt_oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
refine_1 : ∀ (z : V × V) (hz : z ∈ s), z.1 ≠ 0
refine_2 : ∀ (z : V × V) (hz : z ∈ s), z.2 ≠ 0
⊢ ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s

Tactic:
refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_

Premises used: continuousOn_of_forall_continuousAt, Orientation.continuousAt_oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : z ∈ s
⊢ ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z

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

Premises used: Set.mem_image
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z
refine_1 : ∀ (r' : ℝ), (x, r' • x + y).1 ≠ 0
⊢ z.1 ≠ 0

Tactic:
obtain ⟨r', -, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
refine_1 : x ≠ 0
⊢ (x, r' • x + y).1 ≠ 0

Tactic:
simp only
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z
refine_2 : ∀ (r' : ℝ), (x, r' • x + y).2 ≠ 0
⊢ z.2 ≠ 0

Tactic:
obtain ⟨r', -, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
refine_2 : r' • x + y ≠ 0
⊢ (x, r' • x + y).2 ≠ 0

Tactic:
simp only
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
hz : x = 0
⊢ False

Tactic:
simpa [hz] using (h' 0).1

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
hz : r' • x + y = 0
⊢ False

Tactic:
simpa [hz] using (h' r').1

Premises used: And.left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
⊢ ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s

Tactic:
have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := by
    refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
    all_goals
      simp_rw [s, Set.mem_image] at hz
      obtain ⟨r', -, rfl⟩ := hz
      simp only
      intro hz
    · simpa [hz] using (h' 0).1
    · simpa [hz] using (h' r').1
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
⊢ ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
⊢ ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)

Tactic:
have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := by grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
⊢ Membership.mem (γ := Set (V × V)) ((fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ) ((fun (r' : ℝ) ↦ (x, r' • x + y)) 0)

Tactic:
Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)

Premises used: Set.Mem, Prod.mk, HAdd.hAdd, Set.mem_image_of_mem, Set.mem_univ, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
h₁ : y = HSMul.hSMul (α := ℝ) 0 x + y
⊢ (x, y) ∈ s

Tactic:
convert! Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)

Premises used: Prod.mk, HAdd.hAdd, Set.mem_image_of_mem, Set.mem_univ, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
⊢ y = HSMul.hSMul (α := ℝ) 0 x + y

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
⊢ (x, y) ∈ s

Tactic:
have hx : (x, y) ∈ s := by
    convert! Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)
    simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
hx : (x, y) ∈ s
⊢ (x, r • x + y) ∈ s

Tactic:
have hy : (x, r • x + y) ∈ s := Set.mem_image_of_mem _ (Set.mem_univ _)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
hx : (x, y) ∈ s
hy : (x, r • x + y) ∈ s
⊢ (o.oangle (x, r • x + y).1 (x, r • x + y).2).sign = (o.oangle (x, y).1 (x, y).2).sign

Tactic:
Real.Angle.sign_eq_of_continuousOn hc hf hs hx hy

Premises used: Real.Angle.sign_eq_of_continuousOn
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
hx : (x, y) ∈ s
hy : (x, r • x + y) ∈ s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
convert! Real.Angle.sign_eq_of_continuousOn hc hf hs hx hy

Premises used: Real.Angle.sign_eq_of_continuousOn
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
simp_rw : (-o.oangle y (x + r • y)).sign = (-o.oangle y x).sign
simp_rw₁ : -(o.oangle y (x + r • y)).sign = -(o.oangle y x).sign
simp_rw₂ : -(o.oangle y (r • y + x)).sign = -(o.oangle y x).sign
⊢ (o.oangle (x + r • y) y).sign = (o.oangle x y).sign

Tactic:
simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right]

Premises used: Orientation.oangle_sign_smul_add_right, Real.Angle.sign_neg, add_comm, Orientation.oangle_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
rw : (o.oangle x (y + -(r • x))).sign = (o.oangle x y).sign
rw₁ : (o.oangle x (y + -r • x)).sign = (o.oangle x y).sign
rw₂ : (o.oangle x (-r • x + y)).sign = (o.oangle x y).sign
rw₃ rw₄ : (o.oangle x y).sign = (o.oangle x y).sign
⊢ (o.oangle x (y - r • x)).sign = (o.oangle x y).sign

Tactic:
rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right]

Premises used: Orientation.oangle_sign_smul_add_right, neg_smul, sub_eq_add_neg, add_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
rw : (o.oangle (x + -(r • y)) y).sign = (o.oangle x y).sign
rw₁ : (o.oangle (x + -r • y) y).sign = (o.oangle x y).sign
rw₂ rw₃ : (o.oangle x y).sign = (o.oangle x y).sign
⊢ (o.oangle (x - r • y) y).sign = (o.oangle x y).sign

Tactic:
rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left]

Premises used: neg_smul, sub_eq_add_neg, Orientation.oangle_sign_add_smul_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : (o.oangle x (x + y)).sign = (o.oangle x (HSMul.hSMul (α := ℝ) 1 x + y)).sign
rw₁ rw₂ : (o.oangle x (x + y)).sign = (o.oangle x (x + y)).sign
⊢ (o.oangle x (x + y)).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_add_right x y 1, one_smul]

Premises used: Orientation.oangle_sign_smul_add_right, one_smul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : (o.oangle (x + y) y).sign = (o.oangle (x + HSMul.hSMul (α := ℝ) 1 y) y).sign
rw₁ rw₂ : (o.oangle (x + y) y).sign = (o.oangle (x + y) y).sign
⊢ (o.oangle (x + y) y).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_add_smul_left x y 1, one_smul]

Premises used: one_smul, Orientation.oangle_sign_add_smul_left, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : (o.oangle x (y - x)).sign = (o.oangle x (y - HSMul.hSMul (α := ℝ) 1 x)).sign
rw₁ rw₂ : (o.oangle x (y - x)).sign = (o.oangle x (y - x)).sign
⊢ (o.oangle x (y - x)).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_sub_smul_right x y 1, one_smul]

Premises used: Orientation.oangle_sign_sub_smul_right, one_smul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : (o.oangle (x - y) y).sign = (o.oangle (x - HSMul.hSMul (α := ℝ) 1 y) y).sign
rw₁ rw₂ : (o.oangle (x - y) y).sign = (o.oangle (x - y) y).sign
⊢ (o.oangle (x - y) y).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_sub_smul_left x y 1, one_smul]

Premises used: Orientation.oangle_sign_sub_smul_left, one_smul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
rw : (o.oangle x (r • x - y)).sign = (o.oangle x (-y)).sign
rw₁ : (o.oangle x (r • x + -y)).sign = (o.oangle x (-y)).sign
rw₂ rw₃ : (o.oangle x (-y)).sign = (o.oangle x (-y)).sign
⊢ (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign

Tactic:
rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]

Premises used: Orientation.oangle_sign_smul_add_right, sub_eq_add_neg, Orientation.oangle_sign_neg_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
rw : (o.oangle (r • y - x) y).sign = (o.oangle (-x) y).sign
rw₁ : (o.oangle (-x + r • y) y).sign = (o.oangle (-x) y).sign
rw₂ rw₃ : (o.oangle (-x) y).sign = (o.oangle (-x) y).sign
⊢ (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign

Tactic:
rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]

Premises used: sub_eq_neg_add, Orientation.oangle_sign_neg_left, Orientation.oangle_sign_add_smul_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : (o.oangle x (x - y)).sign = (o.oangle x (HSMul.hSMul (α := ℝ) 1 x - y)).sign
rw₁ rw₂ : (o.oangle x (x - y)).sign = (o.oangle x (x - y)).sign
⊢ (o.oangle x (x - y)).sign = -(o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_sub_right x y 1, one_smul]

Premises used: one_smul, OfNat.ofNat, Orientation.oangle_sign_smul_sub_right