mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, 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
p₁ p₂ p₃ : P
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
hsyz : (o.oangle y 0).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y 0 = π / 2

Tactic:
·

Goal state after:
case inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
hsyz : (o.oangle y 0).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y 0 = π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₁, p₃}

pp: case refine_2.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₃, p₃}

pp: case refine_2.inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

pp: case refine_2.inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
·

Goal state after:
case refine_2.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₁, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₃, p₃}

pp: case refine_2.inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

pp: case refine_2.inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
·

Goal state after:
case refine_2.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₃, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

pp: case refine_2.inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
·

Goal state after:
case refine_2.inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ Collinear ℝ {p₁, p₂, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inr.inl.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₃
⊢ Collinear ℝ {p₁, p₂, p₃}

pp: case refine_2.inr.inr.inl.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
·

Goal state after:
case refine_2.inr.inr.inl.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₃
⊢ Collinear ℝ {p₁, p₂, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inr.inl.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
·

Goal state after:
case refine_2.inr.inr.inl.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ {p₁, p₂, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π = 0
⊢ False

pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0

Tactic:
·

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
·

Goal state after:
case refine_2.inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0

Tactic:
·

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case 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₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : r < 0
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))

pp: case 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₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : 0 < r
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))

Tactic:
·

Goal state after:
case 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₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : r < 0
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case 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₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : 0 < r
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))

Tactic:
·

Goal state after:
case 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₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : 0 < r
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0
⊢ o.oangle w x = o.oangle y z

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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0
⊢ o.oangle w x = o.oangle y z
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case e'_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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = o.oangle (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)

pp: case e'_3
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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)

pp: 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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃

Tactic:
·

Goal state after:
case e'_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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = o.oangle (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case e'_3
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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)

pp: 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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃

Tactic:
·

Goal state after:
case e'_3
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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: 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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃

Tactic:
·

Goal state after:
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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ 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
h : (o.oangle x y).sign = 1
hx : x = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = 1
hx : x = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)
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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case inl.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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = ↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = ↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

pp: case inl.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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = ↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = -↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

pp: case 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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = ↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

pp: case 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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = -↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
·

Goal state after:
case inl.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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = ↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = ↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ 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
h : (o.oangle x y).sign = -1
hx : x = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = -1
hx : ¬x = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = -1
hx : x = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)
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
h : (o.oangle x y).sign = -1
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = -1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)

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
h : (o.oangle x y).sign = -1
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case inl.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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = ↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = -↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

pp: case 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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = ↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

pp: case 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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = -↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
·

Goal state after:
case inl.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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = ↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = -↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆