mathlib-initiative/mathlib-tactics huggingface dataset:
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 = 0
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ 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 = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ 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 = 0
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₂ p₃ p p₁ : P
h : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
hp₃p : p₃ = p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p

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₁ : P
h : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
hp₃p : ¬p₃ = p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p

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
p₂ p₃ p p₁ : P
h : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
hp₃p : p₃ = p
⊢ ∠ p₁ p₂ p₃ = ∠ 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
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
·

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h₃₂ : p₃ = p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ p₁ p₂ p₃

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 pos
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₃
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
h0 : x = 0 ∧ y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

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)
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∧ y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖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)
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

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 pos
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.Basic

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

pp: case inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
⊢ (o.oangle w 0).sign = 0 ∧ (o.oangle y z).sign = 0

pp: case inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle 0 z).sign = 0

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
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y 0).sign = 0

Tactic:
·

Goal state after:
case inl.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : InnerProductGeometry.angle 0 x = InnerProductGeometry.angle y z
hs : (o.oangle 0 x).sign = (o.oangle y z).sign
⊢ (o.oangle 0 x).sign = 0 ∧ (o.oangle y z).sign = 0
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
h : Collinear ℝ {p₁, p₂, p₃}
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ 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
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_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
h : Collinear ℝ {p₁, p₂, p₃}
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : p₁ = p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

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 : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : ¬p₁ = p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : p₁ = p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

pp: case inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle 0 z).sign = 0

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
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y 0).sign = 0

Tactic:
·

Goal state after:
case inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
⊢ (o.oangle w 0).sign = 0 ∧ (o.oangle y z).sign = 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : ¬p₁ = p₂
h₃₂ : p₃ = p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

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 : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

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
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : ¬p₁ = p₂
h₃₂ : p₃ = p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

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
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y 0).sign = 0

Tactic:
·

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

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

pp: case neg.h.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
·

Goal state after:
case neg.h.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬x = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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

Tactic:
·

Goal state after:
case neg.h.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
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
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y 0).sign = 0

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
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y 0).sign = 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Tactic:
·

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

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

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

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

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 inl.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hsyz : (o.oangle y z).sign = 0
h : InnerProductGeometry.angle 0 x = InnerProductGeometry.angle y z
hs : (o.oangle 0 x).sign = (o.oangle y z).sign
hswx : (o.oangle 0 x).sign = 0
⊢ InnerProductGeometry.angle 0 x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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

Tactic:
·

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ 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
p₁ p₂ p₃ : P
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ 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
p₁ p₂ p₃ : P
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

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

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 inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
hsyz : (o.oangle y z).sign = 0
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
hswx : (o.oangle w 0).sign = 0
⊢ InnerProductGeometry.angle w 0 = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ 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
p₁ p₂ p₃ : P
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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

Tactic:
·

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

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.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
hsyz : (o.oangle 0 z).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle 0 z = π / 2