awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h' : p ∈ s₁ ∨ p ∈ s₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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)
have h'₁ : p ∉ s₁ ∧ p ∉ s₂
Tactic: rw [not_or] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
have 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')
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)))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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')
have 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')
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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')
⊢ 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')
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
⊢ 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')
have 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')
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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')
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have hp : p ≠ p'
Tactic: have hp : p ≠ p' := by
        rintro rfl
        exact h'.1 hp'₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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'
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have hpd : 0 < dist p p'
Tactic: have hpd : 0 < dist p p' := dist_pos.2 hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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'
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have neg : ∀
  (h :
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p' =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
  (hp : p ≠ p') (hpd : 0 < dist p p'),
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rw [Real.arcsin_inj (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity))
        ((div_le_one hpd).2 ?_)
        (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)] at h
Cleared hypotheses: h, hp, hpd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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'
neg :
  ∀
    (h :
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p' =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
    (hp : p ≠ p') (hpd : 0 < 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)
have rw : dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≤ dist p p'
Tactic: rw [Real.arcsin_inj (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity))
        ((div_le_one hpd).2 ?_)
        (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)] at h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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'
neg :
  ∀
    (h :
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) / dist p p' =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p')
    (hp : p ≠ p') (hpd : 0 < dist p p'),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
rw : 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)
have rw₁ : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ≤ dist p p'
Tactic: rw [Real.arcsin_inj (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity))
        ((div_le_one hpd).2 ?_)
        (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)] at h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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 p' =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) / dist p p'
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have neg : ∀
  (h :
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P))
  (hp : p ≠ p') (hpd : 0 < dist p p'),
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rwa [div_left_inj' hpd.ne'] at h
Cleared hypotheses: h, hp, hpd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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'
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≤ dist p p'
have rw : Metric.infDist p (↑s₁ : Set P) ≤ dist p p'
Tactic: rw [dist_orthogonalProjection_eq_infDist]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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'
⊢ dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ≤ dist p p'
have rw : Metric.infDist p (↑s₂ : Set P) ≤ dist p p'
Tactic: rw [dist_orthogonalProjection_eq_infDist]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hp₁ : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≠ p'
hp₂ : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ≠ p'
h :
  ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) 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)
have rw : ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∨
  Wbtw ℝ p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∨
    Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
Tactic: rw [dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂, angle_comm,
      angle_eq_iff_oangle_eq_or_wbtw hp₁ hp₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this : Nonempty.{u_2 + 1} ↥s₁
Tactic: haveI : Nonempty s₁ := ⟨p', hp'₁⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
this : Nonempty.{u_2 + 1} ↥s₁
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this₁ : Nonempty.{u_2 + 1} ↥s₂
Tactic: haveI : Nonempty s₂ := ⟨p', hp'₂⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this₁ : Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)
Tactic: haveI : Nonempty (s₁ ⊓ s₂ : AffineSubspace ℝ P) := ⟨p', hp'₁, hp'₂⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
this_1 : Nonempty.{u_2 + 1} ↥s₁
this_2 : Nonempty.{u_2 + 1} ↥s₂
this : Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)
hp : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) = p'
⊢ False
have h₁ : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = p'
Tactic: rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem hp'₂] at h
Cleared hypotheses: h, this_1, this_2, this, hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
this_1 : Nonempty.{u_2 + 1} ↥s₁
this_2 : Nonempty.{u_2 + 1} ↥s₂
this : Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have hp₁ : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≠ p'
Tactic: have hp₁ : orthogonalProjection s₁ p ≠ p' := by
    intro hp
    rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem hp'₂] at h
    grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
this_1 : Nonempty.{u_2 + 1} ↥s₁
this_2 : Nonempty.{u_2 + 1} ↥s₂
this : Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)
hp₁ : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≠ p'
hp : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = p'
⊢ False
have h₁ : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) = p'
Tactic: rw [hp, dist_orthogonalProjection_eq_dist_iff_eq_of_mem hp'₁] at h
Cleared hypotheses: h, this_1, this_2, this, hp₁, hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
this_1 : Nonempty.{u_2 + 1} ↥s₁
this_2 : Nonempty.{u_2 + 1} ↥s₂
this : Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)
hp₁ : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≠ p'
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have hp₂ : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ≠ p'
Tactic: have hp₂ : orthogonalProjection s₂ p ≠ p' := by
    intro hp
    rw [hp, dist_orthogonalProjection_eq_dist_iff_eq_of_mem hp'₁] at h
    grind