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
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 pos : p = p₁
Tactic: suffices p = p₁ by simp [this]
-- 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)
⊢ p = p₁
have 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)
Tactic: have hs := orthogonalProjection_sup_of_orthogonalProjection_eq ho
-- 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)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
have h₁ : {p₁, p₂} = ![p₁, p₂, p₃] '' {0, 1}
Tactic: convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 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
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)
h₁ : {p₁, p₂} = ![p₁, p₂, p₃] '' {0, 1}
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
have h₂ : {p₁, p₃} = ![p₁, p₂, p₃] '' {0, 2}
Tactic: convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 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
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)
h₁ : {p₁, p₂} = ![p₁, p₂, p₃] '' {0, 1}
h₂ : {p₁, p₃} = ![p₁, p₂, p₃] '' {0, 2}
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
have h₃ : {p₁} = ![p₁, p₂, p₃] '' ({0, 1} ∩ {0, 2})
Tactic: convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 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
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)
⊢ {p₁} = ![p₁, p₂, p₃] '' ({0, 1} ∩ {0, 2})
have h₁ : {p₁} = ![p₁, p₂, p₃] '' {0}
Tactic: suffices {p₁} = ![p₁, p₂, p₃] '' {0} by 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)
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)
⊢ p = p₁
have hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
Tactic: have hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁} := by
      convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 2})
      · simp [Set.image_insert_eq]
      · simp [Set.image_insert_eq]
      · suffices {p₁} = ![p₁, p₂, p₃] '' {0} by grind
        simp
-- 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₁})
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
have rw : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ ({p₁, p₂} ∪ {p₁, p₃})) ⊤
Tactic: rw [← AffineSubspace.span_union]
-- 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₁})
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ ({p₁, p₂} ∪ {p₁, p₃})) ⊤
have h₁ : {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]
Tactic: convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.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
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₁})
h₁ : {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ ({p₁, p₂} ∪ {p₁, p₃})) ⊤
have convert! : Fintype.card (Fin (Nat.succ 0).succ.succ) = finrank ℝ V + 1
Tactic: convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.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
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₁})
⊢ {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]
have h₁ : Eq (α := Set P) {p₃, p₁, p₂} {p₃, p₂, p₁}
Tactic: simp
-- 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₁})
⊢ p = p₁
have hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
Tactic: have hsup : line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃] = ⊤ := by
      rw [← AffineSubspace.span_union]
      convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_
      · simp
        grind
      · simpa using Fact.out
-- 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₃}) ⊤
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
have suffices : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
  (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
Tactic: suffices (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈ affineSpan ℝ {p₁} by
        simpa using this
-- 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₃}) ⊤
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
have hi : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃})
  (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
Tactic: have hi : (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈
          line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] :=
        ⟨orthogonalProjection_mem _, ho ▸ orthogonalProjection_mem _⟩
-- 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₃}) ⊤
hi :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
have rwa : ∀
  (hi :
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)),
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
Tactic: rwa [hinf] at hi
Cleared hypotheses: hi
-- 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₃}) ⊤
⊢ 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
      suffices (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈ affineSpan ℝ {p₁} by
        simpa using this
      have hi : (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈
          line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] :=
        ⟨orthogonalProjection_mem _, ho ▸ orthogonalProjection_mem _⟩
      rwa [hinf] at hi