mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

pp: case neg.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

pp: case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

Tactic:
·

Goal state after:
case neg.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

pp: case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

Tactic:
·

Goal state after:
case neg.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

Tactic:
·

Goal state after:
case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: 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 : ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
·

Goal state after:
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 : ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hr : ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
⊢ dist p₁ p = dist p₂ p

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: 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

pp: 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

Tactic:
·

Goal state after:
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
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: 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

Tactic:
Real.Angle.sign_eq_zero_iff.2 h,

Goal state after:
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 = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
⊢ o.oangle x (x + 0 • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan 0)

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hr : ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
⊢ dist p₁ p = dist p₂ p

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hr : ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
⊢ dist p₁ p = dist p₂ p
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
⊢ o.oangle x (x + 0 • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan 0)

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
·

Goal state after:
case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
⊢ o.oangle x (x + 0 • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan 0)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
·

Goal state after:
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case refine_1
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' : ℝ
hz : x = 0
⊢ False

pp: 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
r' : ℝ
hz : r' • x + y = 0
⊢ False

Tactic:
·

Goal state after:
case refine_1
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' : ℝ
hz : x = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: 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
r' : ℝ
hz : r' • x + y = 0
⊢ False

Tactic:
·

Goal state after:
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
r' : ℝ
hz : r' • x + y = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₅, p₁, p₂}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
·

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₅, p₁, p₂}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
·

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: 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₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

pp: 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₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
·

Goal state after:
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₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: 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₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
·

Goal state after:
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₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
⊢ ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
⊢ ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : p₂ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
·

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : p₂ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : p₁ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
·

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : p₁ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)