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
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
this₁ : Nonempty.{u_2 + 1} ↥s₁
this₂ : Nonempty.{u_2 + 1} ↥s₂
h₁ :
  ∡ (↑((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)
this₃ : Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)
hp₃ : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≠ p'
⊢ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ≠ p'

Tactic:
rw [dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂, angle_comm,
    angle_eq_iff_oangle_eq_or_wbtw hp₁ hp₂] at h

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_iff_oangle_eq_or_wbtw, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq
-- 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
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
this₁ : Nonempty.{u_2 + 1} ↥s₁
this₂ : Nonempty.{u_2 + 1} ↥s₂
h₁ :
  ∡ (↑((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)
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'
⊢ ¬Collinear ℝ (P := P)
      {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₂] at h

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_iff_oangle_eq_or_wbtw, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq
-- 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
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)
this_1 : Nonempty.{u_2 + 1} ↥s₁
this_2 : Nonempty.{u_2 + 1} ↥s₂
h :
  ∡ (↑((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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
inl :
  ∀
    (h :
      ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
        ∡ p 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)
inr :
  ∀
    (h :
      Wbtw ℝ p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : 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)
inr₁ :
  ∀
    (h :
      Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : 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)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rcases h with h | 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h :
  ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p 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)

Tactic:
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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h :
  ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p 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)

Tactic:
exact 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inr : False
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
exfalso
-- 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ False

Tactic:
hc h.collinear

Premises used: Wbtw.collinear
-- 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ False

Tactic:
exact hc h.collinear

Premises used: Wbtw.collinear
-- 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
inr : False
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
exfalso
-- 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
⊢ Collinear ℝ (P := P)
    {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P), (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)}

Tactic:
have h' := h.collinear
-- 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h' :
  Collinear ℝ (P := P)
    {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P), (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)}
⊢ Collinear ℝ (P := P)
    {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}

Tactic:
rw [Set.pair_comm] at h'

Premises used: Set.pair_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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h' :
  Collinear ℝ (P := P)
    {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
⊢ False

Tactic:
hc 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
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)
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'
hc :
  ¬Collinear ℝ (P := P)
      {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
h : Wbtw ℝ p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h' :
  Collinear ℝ (P := P)
    {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P), (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)}
⊢ False

Tactic:
exact hc 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
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₂
⊢ Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) →
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ≠ p' →
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ≠ p' →
        (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))

Tactic:
fun hne hp₁ hp₂ ↦ ⟨oangle_eq_of_dist_orthogonalProjection_eq hp'₁ hp'₂ hne,
   dist_orthogonalProjection_eq_of_oangle_eq hp'₁ hp'₂ hp₁ hp₂⟩

Premises used: EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, 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
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 :
  HSMul.hSMul (α := ℤ) 2 (∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P))
⊢ Nonempty.{u_2 + 1} ↥s₁

Tactic:
haveI : 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
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 :
  HSMul.hSMul (α := ℤ) 2 (∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P))
this : Nonempty.{u_2 + 1} ↥s₁
⊢ Nonempty.{u_2 + 1} ↥s₂

Tactic:
haveI : 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
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 :
  HSMul.hSMul (α := ℤ) 2 (∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p 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)

Tactic:
have h' : ∡ (orthogonalProjection s₁ p : P) p' p = ∡ p p' (orthogonalProjection s₂ p) :=
    oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two h
      (angle_self_orthogonalProjection _ hp'₁) (angle_self_orthogonalProjection _ 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
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 :
  HSMul.hSMul (α := ℤ) 2 (∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P))
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
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)

Tactic:
dist_orthogonalProjection_eq_of_oangle_eq hp'₁ hp'₂ hp₁ hp₂ h'

Premises used: EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq
-- 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
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 :
  HSMul.hSMul (α := ℤ) 2 (∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P))
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
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)

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

Premises used: EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq