awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ p = p₁
have hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
          (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
        p) :
    P) =
  p₁
Tactic: rw [← orthogonalProjection_sup_of_orthogonalProjection_eq ho] at hp
Cleared hypotheses: 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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
hp :
  (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P) =
    p₁
⊢ p = p₁
have pos : Membership.mem (γ := AffineSubspace ℝ P) ⊤ p
Tactic: rw [← hp, eq_comm, orthogonalProjection_eq_self_iff, hsup]
-- 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have hp : ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
  ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
Tactic: have hp := oangle_eq_of_dist_orthogonalProjection_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) ho 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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have h₂₁ : p₂ ≠ p₁
Tactic: have h₂₁ : p₂ ≠ p₁ := ha.injective.ne (by decide : (1 : Fin 3) ≠ 0)
-- 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have h₃₁ : p₃ ≠ p₁
Tactic: have h₃₁ : p₃ ≠ p₁ := ha.injective.ne (by decide : (2 : Fin 3) ≠ 0)
-- 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ False
have h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
Tactic: rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h
Cleared hypotheses: h, ho, hp_1, h₂₁, h₃₁, 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁
Tactic: have hp₁ : orthogonalProjection line[ℝ, p₁, p₂] p ≠ p₁ := by
      intro hp
      rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
⊢ False
have h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
Tactic: rw [hp, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
          (left_mem_affineSpan_pair ℝ _ p₂)] at h
Cleared hypotheses: h, ho, hp_1, h₂₁, h₃₁, 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have hp₂ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) ≠ p₁
Tactic: have hp₂ : orthogonalProjection line[ℝ, p₁, p₃] p ≠ p₁ := by
      intro hp
      rw [hp, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
          (left_mem_affineSpan_pair ℝ _ p₂)] at h
      grind
-- 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₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁
hp₂ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) ≠ p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have neg : HSMul.hSMul (α := ℤ) 2
    (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
  HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
Tactic: rw [← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_left hp₁ h₂₁,
        ← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_right hp₂ h₃₁, 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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁
hp₂ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) ≠ p₁
neg :
  HSMul.hSMul (α := ℤ) 2
      (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have neg₁ : HSMul.hSMul (α := ℤ) 2
    (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
  HSMul.hSMul (α := ℤ) 2
    (∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P))
Tactic: rw [← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_left hp₁ h₂₁,
        ← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_right hp₂ h₃₁, 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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  ¬Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁
hp₂ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) ≠ p₁
neg :
  HSMul.hSMul (α := ℤ) 2
      (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
    HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
neg₁ :
  HSMul.hSMul (α := ℤ) 2
      (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have neg₂ : HSMul.hSMul (α := ℤ) 2
    (∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)) =
  HSMul.hSMul (α := ℤ) 2
    (∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P))
Tactic: rw [← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_left hp₁ h₂₁,
        ← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_right hp₂ h₃₁, hp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
⊢ ∃ (signs : Finset (Fin (n + 1))), s.ExcenterExists signs ∧ p = s.excenter signs
have rw : ∃ (r : ℝ),
  ∀ (i : Fin (n + 1)),
    dist p
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              p) :
          P) =
      r
Tactic: rw [← s.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter hp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
⊢ ∃ (r : ℝ),
    ∀ (i : Fin (n + 1)),
      dist p
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                p) :
            P) =
        r
have refine : ∀ (i : Fin (n + 1)),
  dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)
Tactic: refine ⟨dist p ((s.faceOpposite i₁).orthogonalProjectionSpan p), ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
i : Fin (n + 1)
⊢ dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)
have pos : ∀ (hi : i = i₁),
  dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)
Tactic: by_cases hi : i = i₁