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

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
hx : ¬x = 0
hy : y = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

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.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
· simp [hy]

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
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0
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
hx : ¬x = 0
hy : y = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle 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
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
· simp [hy]

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
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
u : V₂
⊢ u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction →
    inner 𝕜 u (f.linear (p -ᵥ ↑((orthogonalProjection s) p))) = 0

Tactic:
hu

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
u : V₂
hu : u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction
⊢ inner 𝕜 u (f.linear (p -ᵥ ↑((orthogonalProjection s) p))) = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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
θ : Real.Angle
⊢ x = (o.rotation θ) x ↔ x = 0 ∨ θ = 0

Tactic:
← rotation_eq_self_iff,

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
θ : Real.Angle
⊢ x = (o.rotation θ) x ↔ (rotation ?o θ) x = x

case o
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
⊢ Orientation ℝ V (Fin 2)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
· rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]
      simp [hx, hy]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a.refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ

Tactic:
← Submodule.inf_orthogonal,

Goal state after:
case a.refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ ⊓ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
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
hx : ¬x = 0
hy : y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

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.oangle x y).cos

Tactic:
· simp [hy]

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.oangle x y).cos
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:
· simp [hy]

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

Tactic:
rw [not_and_or] at h0

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

Tactic:
← norm_neg,

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‖ / Real.sin (angle x (x + -y)) = ‖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
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x + -y)) = ‖x‖

Tactic:
← norm_neg,

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‖ / Real.tan (angle x (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
⊢ (o.oangle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁)).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
← o.oangle_neg_neg,

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
⊢ (o.oangle (-(p₂ -ᵥ p₁)) (-(p₃ -ᵥ p₁))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).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
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ ⟪x, y⟫ = 0

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 = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ ⟪x, y⟫ = 0

Tactic:
· simp [hy]

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 = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ ⟪x, y⟫ = 0
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
hx : ¬x = 0
hy : y = 0
⊢ (o.oangle (-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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
· simp [hy]

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

Tactic:
· simp [hy]

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
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign
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:
rcases hr with ⟨r, rfl⟩

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
h : p₁ ≠ p₂
r : ℝ
⊢ dist p₁ (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂) =
    dist p₂ (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ 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)
x y : V
r : ℝ
⊢ (o.oangle (r • y - x) y).sign = (o.oangle (-x) y).sign

Tactic:
sub_eq_neg_add,

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
r : ℝ
⊢ (o.oangle (-x + r • y) y).sign = (o.oangle (-x) y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: 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 : ℝ
⊢ (o.oangle x (x + r • (o.rotation ↑(π / 2)) x)).tan = r

Tactic:
rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]

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

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Goal state after:
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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : y = 0
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

Tactic:
· simp [hy]

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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
Module: Mathlib.Geometry.Euclidean.SignedDist

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
v : V
p q r : P
⊢ ((signedDist v) p) q - ((signedDist v) p) r = ((signedDist v) r) q

Tactic:
rw [sub_eq_iff_eq_add', signedDist_triangle]

Goal state after:
Module: Mathlib.Geometry.Euclidean.PerpBisector

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
⊢ perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ perpBisector_self _⟩

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
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ = p₂
Module: Mathlib.Geometry.Euclidean.SignedDist

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
v : V
p q : P
⊢ ((signedDist v) p) q = dist p q ↔ ∃ a, a • v = q -ᵥ p

Tactic:
rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case refine_2
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
h : ∃ s, ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps

Tactic:
rcases h with ⟨s, h⟩

Goal state after:
case refine_2
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ ↑π
⊢ (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).sign

Tactic:
rw [hadd, ← oangle_swap₂₃_sign p₁ p₃ p₂, ← oangle_swap₂₃_sign p₁ p₄ p₂, neg_inj, eq_comm]

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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ ↑π
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case e_a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
hp : p ≠ ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hpm : p ∉ line[ℝ, p₁, p₂]
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
u : V
⊢ u ∈ line[ℝ, p₁, p₃].direction → inner ℝ (p -ᵥ p₁) u = 0

Tactic:
hu

Goal state after:
case e_a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
hp : p ≠ ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hpm : p ∉ line[ℝ, p₁, p₂]
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
u : V
hu : u ∈ line[ℝ, p₁, p₃].direction
⊢ inner ℝ (p -ᵥ p₁) u = 0
Module: Mathlib.Geometry.Euclidean.Basic

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
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hv : v ∈ s.direction
hu : Finset.univ = {0, 1}
⊢ ↑(Finset.image b Finset.univ) = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}

Tactic:
hu

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hv : v ∈ s.direction
hu : Finset.univ = {0, 1}
⊢ ↑(Finset.image b {0, 1}) = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : p' ∈ s.orthRadius p
⊢ p' = p

Tactic:
have h' := dist_sq_eq_of_mem_orthRadius hp'i

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
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : p' ∈ s.orthRadius p
h' : dist p' s.center ^ 2 = dist p s.center ^ 2 + dist p' p ^ 2
⊢ p' = p
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
⊢ q = p ∧ dist p s.center = s.radius

Tactic:
have hq' := (h' q).2 rfl

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
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
hq' : q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
⊢ q = p ∧ dist p s.center = s.radius