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
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)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have 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)
Tactic: rcases h with h | h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have 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)
Tactic: rcases h with h | h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
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)
⊢ ∡ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) p' p =
    ∡ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
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
have h' : Collinear ℝ (P := P)
  {p', (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P), (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)}
Tactic: have h' := h.collinear
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne :
  Ne.{u_2 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
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
have h'₁ : 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'
Cleared hypotheses: 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
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))
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this : Nonempty.{u_2 + 1} ↥s₁
Tactic: haveI : Nonempty s₁ := ⟨p', hp'₁⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
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₁
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this₁ : Nonempty.{u_2 + 1} ↥s₂
Tactic: haveI : Nonempty s₂ := ⟨p', hp'₂⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
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₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have h' : ∡ (↑((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'₂)
-- 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
h₂ : p₁ ≠ p₂
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ 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)
have inl : ∀ (h₂ : p ≠ p₂) (h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p p) = HSMul.hSMul (α := ℤ) 2 (∡ p p p₃))
  (h' : (↑((orthogonalProjection (affineSpan ℝ {p, p₂}) : (a : P) → ↥(affineSpan ℝ {p, p₂})) p) : P) = p),
  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)
Tactic: obtain rfl | hp := eq_or_ne p p₁
Cleared hypotheses: p₁, h₂, h, h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
inl :
  ∀ (h₂ : p ≠ p₂) (h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p p) = HSMul.hSMul (α := ℤ) 2 (∡ p p p₃))
    (h' : (↑((orthogonalProjection (affineSpan ℝ {p, p₂}) : (a : P) → ↥(affineSpan ℝ {p, p₂})) p) : P) = p),
    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)
⊢ 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)
have inr : ∀ (hp : p ≠ p₁),
  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)
Tactic: obtain rfl | hp := eq_or_ne p p₁
-- 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
h₂ : p ≠ p₂
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p p) = HSMul.hSMul (α := ℤ) 2 (∡ p p p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p, p₂}) : (a : P) → ↥(affineSpan ℝ {p, p₂})) p) : P) = p
⊢ 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)
have inl : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, p₃}) p
Tactic: rw [h', dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff]
-- 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
h₂ : p₁ ≠ p₂
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ p₁
⊢ 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)
have h₁ : HSMul.hSMul (α := ℤ) 2
    (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
  HSMul.hSMul (α := ℤ) 2
    (∡ p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₃)
Tactic: rw [← h'] at h hp
Cleared hypotheses: 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
h₂ : p₁ ≠ p₂
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ p₁
h₁ :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₃)
h'₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ 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)
have hp₁ : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
Tactic: rw [← h'] at h hp
Cleared hypotheses: 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
h₂ : p₁ ≠ p₂
h :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : 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) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
have hpm : p ∉ affineSpan ℝ {p₁, p₂}
Tactic: have hpm : p ∉ line[ℝ, p₁, p₂] := orthogonalProjection_eq_self_iff.not.1 (Ne.symm 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
h₂ : p₁ ≠ p₂
h :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
⊢ 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)
have h₁ : Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
  Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)
Tactic: rw [two_zsmul_oangle_orthogonalProjection_self _ hpm (right_mem_affineSpan_pair _ _ _)
          (h'.symm ▸ h₂.symm), eq_comm, oangle, Real.Angle.two_zsmul_eq_pi_iff, h'] at h
Cleared hypotheses: h, h', hp, hpm
-- 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
h₂ : p₁ ≠ p₂
h :
  Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
    Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
⊢ 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)
have h₁ : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
Tactic: replace h := (Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero _).1 (.inr (.inr h))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
⊢ 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)
have inr : 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)
Tactic: congr 1
-- 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
h₂ : p₁ ≠ p₂
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
⊢ 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)
have inr : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₁ ∧
  Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)
Tactic: rw [h', eq_comm, coe_orthogonalProjection_eq_iff_mem]