awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X))
                  {p : EuclideanSpace ℝ (Fin m) → X |
                    ∀ (d : DiffeologicalSpace X),
                      g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
                  (p ∘ f)
d : DiffeologicalSpace X
hd : g ⊆ d.toPlots
x : EuclideanSpace ℝ (Fin n)
⊢ ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
    IsOpen u ∧
      x ∈ u ∧
        ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
          (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
            ContDiff ℝ ∞ f → Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) (plots m) (p ∘ f)
have let : ∀ (u : Set (EuclideanSpace ℝ (Fin n))) (hxu : IsOpen u) (hu : x ∈ u)
  (hu' :
    ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
      (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
        ContDiff ℝ ∞ f →
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X))
            {p : EuclideanSpace ℝ (Fin m) → X |
              ∀ (d : DiffeologicalSpace X),
                g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
            (p ∘ f)),
  ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
    IsOpen u ∧
      x ∈ u ∧
        ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
          (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
            ContDiff ℝ ∞ f → Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) (plots m) (p ∘ f)
Tactic: let ⟨u, hxu, hu, hu'⟩ := hp x
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this : Nonempty.{u_2 + 1} ↥s₁
Tactic: have : 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ 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) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this₁ : Nonempty.{u_2 + 1} ↥s₂
Tactic: have : Nonempty s₂ := ⟨p', 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
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) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have refine_1 : ∀
  (h :
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
  ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: refine ⟨fun h ↦ ?_, fun 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
refine_1 :
  ∀
    (h :
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have refine_2 : ∀
  (h :
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: refine ⟨fun h ↦ ?_, fun 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have refine_1 : ∀ (h : dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
  ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rw [orthogonalProjection_eq_self_iff.2 h'] 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have h₁ : p ∈ s₂
Tactic: rw [dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff] at 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : p ∈ s₂
⊢ ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have refine_1 : ∠ p p' p = ∠ p p' p
Tactic: rw [orthogonalProjection_eq_self_iff.2 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h :
  ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have refine_2 : ∀ (h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
  dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rw [orthogonalProjection_eq_self_iff.2 h'] at 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have refine_2 : p ∈ s₂
Tactic: rw [dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff]
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ p ∈ s₂
have refine_2 : ∀ (hp'₁ : p ∈ s₁) (hp'₂ : p ∈ s₂) (h : ∠ p p p = ∠ p p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)), p ∈ s₂
Tactic: obtain rfl | hpp' := eq_or_ne p p'
Cleared hypotheses: p', hp'₁, hp'₂, 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
refine_2 :
  ∀ (hp'₁ : p ∈ s₁) (hp'₂ : p ∈ s₂) (h : ∠ p p p = ∠ p p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)), p ∈ s₂
⊢ p ∈ s₂
have refine_2₁ : ∀ (hpp' : p ≠ p'), p ∈ s₂
Tactic: obtain rfl | hpp' := 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
hpp' : p ≠ p'
⊢ p ∈ s₂
have refine_2 : ∀ (hn : p ∉ s₂), False
Tactic: by_contra hn
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
hpp' : p ≠ p'
hn : p ∉ s₂
⊢ False
have refine_2 : ∀ (h : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = 0 ∨ dist p p' = 0) (hpp' : p ≠ p') (hn : p ∉ s₂),
  False
Tactic: rw [angle_self_of_ne hpp', angle_comm,
        angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₂),
        Real.zero_eq_arcsin_iff, div_eq_zero_iff] at h
Cleared hypotheses: h, hpp', hn
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
hpp' : p ≠ p'
hn : p ∉ s₂
refine_2 :
  ∀ (h : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = 0 ∨ dist p p' = 0) (hpp' : p ≠ p') (hn : p ∉ s₂),
    False
⊢ False
have refine_2₁ : ∀ (h : 0 = ∠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) p' p) (hpp' : p ≠ p') (hn : p ∉ s₂),
  p ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∨ p' ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rw [angle_self_of_ne hpp', angle_comm,
        angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₂),
        Real.zero_eq_arcsin_iff, div_eq_zero_iff] at h
Cleared hypotheses: h, hpp', hn
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = 0 ∨ dist p p' = 0
hpp' : p ≠ p'
hn : p ∉ s₂
⊢ False
have h₁ : p = (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: simp only [dist_eq_zero, hpp', or_false] 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
hpp' : p ≠ p'
hn : p ∉ s₂
h : p = (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ False
have h₁ : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = p
Tactic: rw [eq_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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this : Nonempty.{u_2 + 1} ↥s₁
Tactic: have : 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ 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) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this₁ : Nonempty.{u_2 + 1} ↥s₂
Tactic: have : Nonempty s₂ := ⟨p', 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
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) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have inl : ∀ (h' : p ∈ s₁),
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rcases h' with 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
inl :
  ∀ (h' : p ∈ s₁),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have inr : ∀ (h' : p ∈ s₂),
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rcases h' with 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have inr : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
  ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: nth_rw 1 [eq_comm]
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h' : p ∈ s₂
⊢ dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have inr : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ↔
  ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
Tactic: nth_rw 2 [eq_comm]
-- 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this : Nonempty.{u_2 + 1} ↥s₁
Tactic: have : 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ 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) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have this₁ : Nonempty.{u_2 + 1} ↥s₂
Tactic: have : Nonempty s₂ := ⟨p', 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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
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) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have pos : ∀ (h' : p ∈ s₁ ∨ p ∈ s₂),
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: by_cases h' : p ∈ s₁ ∨ p ∈ s₂