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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
have h₂ : (orthogonalProjection s₂ p : P) ∈ line[ℝ, p', (orthogonalProjection s₁ p : P)] :=
      hc.mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) (by grind)
-- 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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
h₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂

Tactic:
have h₂' : (orthogonalProjection s₂ p : P) ∈ s₁ ⊓ s₂ :=
      ⟨SetLike.le_def.1 (affineSpan_pair_le_of_mem_of_mem hp'₁ (orthogonalProjection_mem _)) h₂,
        orthogonalProjection_mem _⟩
-- 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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
h₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h₂' : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂
rw : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂
⊢ Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)

Tactic:
rw [← orthogonalProjection_orthogonalProjection_of_le inf_le_right, eq_comm,
        orthogonalProjection_eq_self_iff]

Premises used: EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, inf_le_right, eq_comm, 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
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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
h₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h₂' : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂
⊢ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂

Tactic:
grind
-- 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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
h₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h₂' : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂
⊢ Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)

Tactic:
have h₂'' : (orthogonalProjection s₂ p : P) = (orthogonalProjection (s₁ ⊓ s₂) p : P) := by
      rw [← orthogonalProjection_orthogonalProjection_of_le inf_le_right, eq_comm,
        orthogonalProjection_eq_self_iff]
      grind
-- 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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
h₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h₂' : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂
h₂'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
apply :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ False

Tactic:
apply hne
-- 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)}
h₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)})
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
h₁' : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊓ s₂
h₁'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
h₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p', (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)})
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
h₂' : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∈ s₁ ⊓ s₂
h₂'' :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
rw :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
    (↑((orthogonalProjection (s₁ ⊓ s₂) : (a : P) → ↥(s₁ ⊓ s₂)) p) : P)
⊢ Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

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

Tactic:
have hc : ¬ Collinear ℝ {p', (orthogonalProjection s₁ p : P),
      (orthogonalProjection s₂ p : P)} := by
    intro hc
    have h₁ : (orthogonalProjection s₁ p : P) ∈ line[ℝ, p', (orthogonalProjection s₂ p : P)] :=
      hc.mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) (by grind)
    have h₁' : (orthogonalProjection s₁ p : P) ∈ s₁ ⊓ s₂ :=
      ⟨orthogonalProjection_mem _,
        SetLike.le_def.1 (affineSpan_pair_le_of_mem_of_mem hp'₂ (orthogonalProjection_mem _)) h₁⟩
    have h₁'' : (orthogonalProjection s₁ p : P) = (orthogonalProjection (s₁ ⊓ s₂) p : P) := by
      rw [← orthogonalProjection_orthogonalProjection_of_le inf_le_left, eq_comm,
        orthogonalProjection_eq_self_iff]
      grind
    have h₂ : (orthogonalProjection s₂ p : P) ∈ line[ℝ, p', (orthogonalProjection s₁ p : P)] :=
      hc.mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) (by grind)
    have h₂' : (orthogonalProjection s₂ p : P) ∈ s₁ ⊓ s₂ :=
      ⟨SetLike.le_def.1 (affineSpan_pair_le_of_mem_of_mem hp'₁ (orthogonalProjection_mem _)) h₂,
        orthogonalProjection_mem _⟩
    have h₂'' : (orthogonalProjection s₂ p : P) = (orthogonalProjection (s₁ ⊓ s₂) p : P) := by
      rw [← orthogonalProjection_orthogonalProjection_of_le inf_le_right, eq_comm,
        orthogonalProjection_eq_self_iff]
      grind
    apply hne
    rw [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)
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)}
⊢ Nonempty.{u_2 + 1} ↥s₁

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₁
⊢ Nonempty.{u_2 + 1} ↥s₂

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₂
⊢ ∡ (↑((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₂] 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)
⊢ Nonempty.{u_2 + 1} ↥(s₁ ⊓ s₂)

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₂)
⊢ (↑((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