awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd :
  HPow.hPow (β := ℕ) s.radius 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2
nlinarith :
  ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ ≤ 0 →
    -(HPow.hPow (β := ℕ) s.radius 2 -
              (HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2)) +
          2 * (⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ - 0) +
        (0 - HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2) =
      0
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
have nlinarith₁ : ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [sq_pos_of_pos (norm_pos_iff.mpr (vsub_ne_zero.mpr hp₁p₂.symm))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
have refine : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius →
  ∀ (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (hr : dist p₁ p₂ = 2 * s.radius), midpoint ℝ p₁ p₂ = s.center
Tactic: refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.dist_left_right⟩, fun ⟨h₁, h₂, hr⟩ ↦ ⟨h₁, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ midpoint ℝ p₁ p₂ = s.center
have rw : p₂ -ᵥ s.center = s.center -ᵥ p₁
Tactic: rw [midpoint_eq_iff, AffineEquiv.pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ p₂ -ᵥ s.center = s.center -ᵥ p₁
have h₃ : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖
Tactic: apply eq_of_norm_eq_of_norm_add_eq
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖
⊢ p₂ -ᵥ s.center = s.center -ᵥ p₁
have h₄ : ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖
Tactic: apply eq_of_norm_eq_of_norm_add_eq
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖
have h₃ : dist p₂ s.center = dist s.center p₁
Tactic: simp_rw [← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : dist p₂ s.center = dist s.center p₁
⊢ ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖
have h₄ : dist p₂ s.center = s.radius
Tactic: simp_rw [← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖
have h₃ : dist p₂ p₁ = s.radius + s.radius
Tactic: simp_rw [vsub_add_vsub_cancel, ← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ dist p₂ p₁ = s.radius + s.radius
have h₃ : dist p₁ p₂ = s.radius + s.radius
Tactic: rw [dist_comm, hr, two_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : dist p₁ p₂ = s.radius + s.radius
⊢ dist p₂ p₁ = s.radius + s.radius
have h₄ : 2 * s.radius = s.radius + s.radius
Tactic: rw [dist_comm, hr, two_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : dist p₁ p₂ = s.radius + s.radius
h₄ : 2 * s.radius = s.radius + s.radius
⊢ dist p₂ p₁ = s.radius + s.radius
have h₅ : s.radius + s.radius = s.radius + s.radius
Tactic: rw [dist_comm, hr, two_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
have refine : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂ → ∀ (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (hr : Wbtw ℝ p₁ s.center p₂), s.IsDiameter p₁ p₂
Tactic: refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.wbtw⟩, fun ⟨h₁, h₂, hr⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
⊢ s.IsDiameter p₁ p₂
have hd : dist p₁ s.center + dist s.center p₂ = dist p₁ p₂
Tactic: have hd := hr.dist_add_dist
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ s.center + dist s.center p₂ = dist p₁ p₂
⊢ s.IsDiameter p₁ p₂
have hd₁ : dist p₁ p₂ = 2 * s.radius
Tactic: rw [mem_sphere.1 h₁, mem_sphere'.1 h₂, ← two_mul, eq_comm] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p x : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
have rw : Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
Tactic: rw [orthRadius, mem_mk', Submodule.mem_orthogonal_singleton_iff_inner_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p x : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
have rw₁ : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (x -ᵥ p) ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
Tactic: rw [orthRadius, mem_mk', Submodule.mem_orthogonal_singleton_iff_inner_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p x : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
rw₁ : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (x -ᵥ p) ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
have rw₂ : ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
Tactic: rw [orthRadius, mem_mk', Submodule.mem_orthogonal_singleton_iff_inner_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p x : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
have rw : ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
Tactic: rw [mem_orthRadius_iff_inner_left, inner_eq_zero_symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p x : P
rw : ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
have rw₁ : ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0 ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
Tactic: rw [mem_orthRadius_iff_inner_left, inner_eq_zero_symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p : P
⊢ Eq (α := Submodule ℝ V) (direction (s.orthRadius p)) (ℝ ∙ (p -ᵥ s.center))ᗮ
have rw : Eq (α := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)) (ℝ ∙ (p -ᵥ s.center))ᗮ
Tactic: rw [orthRadius, direction_mk']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p : P
rw : Eq (α := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)) (ℝ ∙ (p -ᵥ s.center))ᗮ
⊢ Eq (α := Submodule ℝ V) (direction (s.orthRadius p)) (ℝ ∙ (p -ᵥ s.center))ᗮ
have rw₁ : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (p -ᵥ s.center))ᗮ
Tactic: rw [orthRadius, direction_mk']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p : P
⊢ Submodule.HasOrthogonalProjection (direction (s.orthRadius p))
have rw : Submodule.HasOrthogonalProjection (E := V) (ℝ ∙ (p -ᵥ s.center))ᗮ
Tactic: rw [direction_orthRadius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) s.center ↔ p = s.center
have rw : -⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0 ↔ p = s.center
Tactic: rw [mem_orthRadius_iff_inner_left, ← neg_vsub_eq_vsub_rev, inner_neg_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p : P
⊢ (↑((orthogonalProjection (s.orthRadius p) : (a : P) → ↥(s.orthRadius p)) s.center) : P) = p
have simp_rw : Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
  Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (s.center -ᵥ p)
Tactic: simp_rw [orthRadius, coe_orthogonalProjection_eq_iff_mem]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
    Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (s.center -ᵥ p)
have rw : Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
  Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (-(s.center -ᵥ p))
Tactic: rw [← Submodule.neg_mem_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q ∨ q = s.center
have refine_1 : ∀ (h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)), p = q ∨ q = s.center
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
refine_1 : ∀ (h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)), p = q ∨ q = s.center
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q ∨ q = s.center
have refine_2 : ∀ (h : p = q ∨ q = s.center), LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ p = q ∨ q = s.center
have h' : LE.le (α := Submodule ℝ V) (direction (s.orthRadius p)) (direction (s.orthRadius q))
Tactic: have h' := direction_le h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (direction (s.orthRadius p)) (direction (s.orthRadius q))
⊢ p = q ∨ q = s.center
have h'₁ : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
Tactic: simp only [direction_orthRadius] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
⊢ p = q ∨ q = s.center
have h'' : LE.le (α := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮᗮ (ℝ ∙ (p -ᵥ s.center))ᗮᗮ
Tactic: have h'' := Submodule.orthogonal_le h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
h'' : LE.le (α := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮᗮ (ℝ ∙ (p -ᵥ s.center))ᗮᗮ
⊢ p = q ∨ q = s.center
have h''₁ : ∃ (a : ℝ), a • (p -ᵥ s.center) = q -ᵥ s.center
Tactic: simp only [Submodule.orthogonal_orthogonal, Submodule.span_singleton_le_iff_mem,
      Submodule.mem_span_singleton] at h''
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
h'' : ∃ (a : ℝ), a • (p -ᵥ s.center) = q -ᵥ s.center
⊢ p = q ∨ q = s.center
have refine_1 : ∀ (r : ℝ) (hr : r • (p -ᵥ s.center) = q -ᵥ s.center), p = q ∨ q = s.center
Tactic: rcases h'' with ⟨r, hr⟩
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
⊢ p = q ∨ q = s.center
have hp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) p
Tactic: have hp : p ∈ s.orthRadius q := h (s.self_mem_orthRadius p)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) p
⊢ p = q ∨ q = s.center
have hp₁ : r - r * r = 0 ∨ ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0
Tactic: rw [mem_orthRadius_iff_inner_left, ← vsub_sub_vsub_cancel_right p q s.center, ← hr,
      inner_sub_left, real_inner_smul_left, real_inner_smul_right, ← mul_assoc, ← sub_mul,
      mul_eq_zero] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : r - r * r = 0 ∨ ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0
⊢ p = q ∨ q = s.center
have refine_1 : ∀ (hp : r - r * r = 0), p = q ∨ q = s.center
Tactic: rcases hp with hp | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : r - r * r = 0 ∨ ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0
refine_1 : ∀ (hp : r - r * r = 0), p = q ∨ q = s.center
⊢ p = q ∨ q = s.center
have refine_1₁ : ∀ (hp : ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0), p = q ∨ q = s.center
Tactic: rcases hp with hp | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : r - r * r = 0
⊢ p = q ∨ q = s.center
have hp₁ : 1 * r - r * r = 0
Tactic: nth_rw 1 [← one_mul r] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : 1 * r - r * r = 0
⊢ p = q ∨ q = s.center
have hp₁ : 1 - r = 0 ∨ r = 0
Tactic: rw [← sub_mul, mul_eq_zero] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : 1 - r = 0 ∨ r = 0
⊢ p = q ∨ q = s.center
have refine_1 : ∀ (hp : 1 - r = 0), p = q ∨ q = s.center
Tactic: rcases hp with hp | rfl
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : 1 - r = 0 ∨ r = 0
refine_1 : ∀ (hp : 1 - r = 0), p = q ∨ q = s.center
⊢ p = q ∨ q = s.center
have refine_1₁ : ∀ (hr : HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center) = q -ᵥ s.center), p = q ∨ q = s.center
Tactic: rcases hp with hp | rfl
Cleared hypotheses: r, hr, hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : 1 - r = 0
⊢ p = q ∨ q = s.center
have hp₁ : 1 = r
Tactic: rw [sub_eq_zero] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (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
s : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : 1 = r
⊢ p = q ∨ q = s.center
have hr₁ : p = q
Tactic: rw [← hp, one_smul, vsub_left_cancel_iff] at hr
Cleared hypotheses: hr, hp