mathlib-initiative/mathlib-tactics huggingface dataset:
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)
x y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π
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)
x : V
hn : x ≠ 0
h : x = 0
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hn : x ≠ 0
h : x = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - ‖x‖ ^ 2) / ‖x + y‖ ^ 2) = Real.arcsin (‖y‖ / ‖x + y‖)

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - ‖x‖ ^ 2) / ‖x + y‖ ^ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
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)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle (f.symm (f x)) (f.symm (f y))

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle (f.symm (f x)) (f.symm (f y))
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)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle x (f.symm (f y))

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle x (f.symm (f y))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (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)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle x y

Tactic:
]

Goal state after:
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)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg

Tactic:
by
  rw [← Complex.oangle, ← hf, o.oangle_map]
  iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ Real.arcsin (‖y‖ / ‖x + y‖) = Real.arcsin (‖y‖ / ‖x + y‖)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + (‖y‖ / ‖x‖) ^ 2)))

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + (‖y‖ / ‖x‖) ^ 2)))
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
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent ℝ ((fun i ↦ ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1))

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
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent ℝ ((fun i ↦ ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (√(‖x‖ ^ 2) * √(1 + (‖y‖ / ‖x‖) ^ 2)))

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (√(‖x‖ ^ 2) * √(1 + (‖y‖ / ‖x‖) ^ 2)))
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
hx : ¬x = 0
hy : ¬y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.kahler x) y ≠ 0

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
hx : ¬x = 0
hy : ¬y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖x‖ * ‖y‖))

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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.kahler x) y ≠ 0
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0

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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0
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
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent ℝ ((fun i ↦ ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1))

Tactic:
convert! Iff.rfl

Goal state after:
case e'_2.e'_4
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
⊢ (fun i ↦ ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1) = ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ r, 0 < r ∧ p₃ -ᵥ p₁ = r • (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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ r, 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ p₃ -ᵥ p₁ = p₃ -ᵥ p₁

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) = ⟪x, y⟫ / (‖x‖ * ‖y‖)

Tactic:
]

Goal state after:
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
⊢ ¬Collinear ℝ {p₁, p₂, p₃} ↔ ¬Collinear ℝ {p₁, p₂, p₃}

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ ∠ p₂ p₁ p₃ = ∠ p₂ p₁ p₃

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mp
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
⊢ (p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r, 0 < r ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
]

Goal state after:
case mp
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
⊢ (p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r, 0 < r ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
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
⊢ Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₁, p₂, p₃}

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ / ‖x + y‖ = ‖x‖ / ‖x + y‖

pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ ≤ ‖x + y‖

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ ≤ ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mp.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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
⊢ p₁ = p₁

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = ↑(InnerProductGeometry.angle x y)
⊢ 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π

Tactic:
]

Goal state after:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = ↑(InnerProductGeometry.angle x y)
⊢ 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mp.inr.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₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0

Tactic:
]

Goal state after:
case mp.inr.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₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ / ‖x + y‖ = ‖y‖ / ‖x + y‖

pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ ≤ ‖x + y‖

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ ≤ ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mp.inr.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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ p₃ = p₃

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π

Tactic:
]

Goal state after:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ 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
p₁ p₂ p₃ : P
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬x = 0
⊢ ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
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₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ 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₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hxy : ‖x + y‖ = 0
h' : ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
]

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hxy : ‖x + y‖ = 0
h' : ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
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
h : (o.oangle x y).sign = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π

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

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
h : o.oangle x y = 0 ∨ o.oangle x y = ↑π
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) + ∠ p₁ p₂ p₃ = π

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
p₁ p₂ p₃ : P
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) + ∠ p₁ p₂ p₃ = π