awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
hpp' : p ≠ p'
hn : p ∉ s₂
h : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = p
⊢ False

Tactic:
simp [orthogonalProjection_eq_self_iff, hn] at h

Premises used: EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : 0 = ∠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) p' p
hpp' : p ≠ p'
hn : p ∉ s₂
⊢ p ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∨ p' ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 hn))

Premises used: Iff.not, Ne.symm, Iff.mp, Or.inl, EuclideanGeometry.orthogonalProjection_eq_self_iff, Iff.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : 0 = ∠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) p' p
hpp' : p ≠ p'
hn : p ∉ s₂
⊢ p ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∨ p' ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
exact .inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 hn))
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
⊢ Nonempty.{u_2 + 1} ↥s₁

Tactic:
have : Nonempty s₁ := ⟨p', hp'₁⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
this : Nonempty.{u_2 + 1} ↥s₁
⊢ Nonempty.{u_2 + 1} ↥s₂

Tactic:
have : Nonempty s₂ := ⟨p', hp'₂⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
inl :
  ∀ (h' : p ∈ s₁),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inr :
  ∀ (h' : p ∈ s₂),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rcases h' with h' | h'
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₁
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
dist_orthogonalProjection_eq_iff_angle_eq_aux₁ hp'₁ hp'₂ h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux₁
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₁
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
exact dist_orthogonalProjection_eq_iff_angle_eq_aux₁ hp'₁ hp'₂ h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux₁
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₂
inr :
  dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
nth_rw 1 [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₂
inr :
  dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
⊢ dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
nth_rw 2 [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)

Tactic:
dist_orthogonalProjection_eq_iff_angle_eq_aux₁ hp'₂ hp'₁ h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux₁
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)

Tactic:
exact dist_orthogonalProjection_eq_iff_angle_eq_aux₁ hp'₂ hp'₁ h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux₁
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
⊢ Nonempty.{u_2 + 1} ↥s₁

Tactic:
have : Nonempty s₁ := ⟨p', hp'₁⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this : Nonempty.{u_2 + 1} ↥s₁
⊢ Nonempty.{u_2 + 1} ↥s₂

Tactic:
have : Nonempty s₂ := ⟨p', hp'₂⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
pos :
  ∀ (h' : p ∈ s₁ ∨ p ∈ s₂),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
neg :
  ∀ (h' : ¬(p ∈ s₁ ∨ p ∈ s₂)),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
by_cases h' : p ∈ s₁ ∨ p ∈ s₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₁ ∨ p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
dist_orthogonalProjection_eq_iff_angle_eq_aux hp'₁ hp'₂ h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₁ ∨ p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
exact dist_orthogonalProjection_eq_iff_angle_eq_aux hp'₁ hp'₂ h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : ¬(p ∈ s₁ ∨ p ∈ s₂)
⊢ p ∉ s₁ ∧ p ∉ s₂

Tactic:
rw [not_or] at h'

Premises used: not_or
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
neg :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
      Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [angle_comm,
    angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₁)
      (.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 h'.1))),
    angle_comm,
    angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₂)
      (.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 h'.2)))]

Premises used: EuclideanGeometry.angle_comm, Iff.not, Ne.symm, And.right, And.left, EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two, Iff.mp, Or.inl, EuclideanGeometry.angle_self_orthogonalProjection, EuclideanGeometry.orthogonalProjection_eq_self_iff, Iff.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
      Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
neg :
  ∀
    (h :
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
    Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
      Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
neg₁ :
  ∀
    (h :
      Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
        Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
      Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
neg neg₁ :
  Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
⊢ Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')

Tactic:
rw [h]
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
hp'₁ : p ∈ s₁
hp'₂ : p ∈ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p) =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p)
⊢ False

Tactic:
h'.1 hp'₁

Premises used: And.left
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
hp'₁ : p ∈ s₁
hp'₂ : p ∈ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p) =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p)
⊢ False

Tactic:
exact h'.1 hp'₁

Premises used: And.left
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
⊢ p ≠ p'

Tactic:
have hp : p ≠ p' := by
        rintro rfl
        exact h'.1 hp'₁
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
hp : p ≠ p'
⊢ 0 < dist p p'

Tactic:
have hpd : 0 < dist p p' := dist_pos.2 hp
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ LE.le (α := ℝ) (-1) 0

Tactic:
norm_num
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ 0 ≤ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p'

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p') =
    Real.arcsin (dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ 0 ≤ dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p'

Tactic:
positivity