awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
⊢ Eq (α := Set P) {-(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p}
    {-√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • ‖v‖⁻¹ • v +ᵥ p}

Tactic:
simp [div_eq_mul_inv, smul_smul]

Premises used: smul_smul, div_eq_mul_inv
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
⊢ ‖‖v‖⁻¹ • v‖ = 1

Tactic:
simp [norm_smul, norm_ne_zero_iff.2 hv0]

Premises used: Iff.mpr, norm_smul, norm_ne_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
⊢ Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V

Tactic:
have hf := finrank_orthRadius hpc
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
hf : Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V
⊢ ∃ (v : ↥(direction (s.orthRadius p))), v ≠ 0 ∧ ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w

Tactic:
simp only [hf2.out, Nat.reduceEqDiff, finrank_eq_one_iff'] at hf

Premises used: finrank_eq_one_iff', Nat.reduceEqDiff, Fact.out
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
hf : ∃ (v : ↥(direction (s.orthRadius p))), v ≠ 0 ∧ ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
obtain :
  ∀ (v : ↥(direction (s.orthRadius p))) (hv0 : v ≠ 0)
    (hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w),
    (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2

Tactic:
obtain ⟨v, hv0, hv⟩ := hf
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv0 : v ≠ 0
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
⊢ (↑v : V) ≠ 0

Tactic:
simpa using hv0
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv0 : v ≠ 0
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
⊢ (↑v : V) ≠ 0

Tactic:
replace hv0 : (v : V) ≠ 0 := by simpa using hv0
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (↑v : V)

Tactic:
simpa using v.property

Premises used: Subtype.property
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
rw :
  (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V) +ᵥ p ≠
    -((√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V)) +ᵥ p
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2

Tactic:
rw [inter_orthRadius_eq_of_dist_le_radius hp.le hpc (by simpa using v.property) hv0,
    Submodule.norm_coe, neg_smul, Set.ncard_pair]

Premises used: neg_smul, EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius, LT.lt.le, Set.ncard_pair, Submodule.norm_coe
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
rw : ¬√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) = 0
rw₁ : ‖v‖ ≠ 0
⊢ (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V) +ᵥ p ≠
    -((√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V)) +ᵥ p

Tactic:
rw [ne_eq, vadd_right_cancel_iff, ← add_eq_zero_iff_eq_neg, ← two_smul ℝ,
    smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_left hv0, div_eq_iff, zero_mul]

Premises used: Real, MulZeroClass.zero_mul, two_smul, add_eq_zero_iff_eq_neg, smul_eq_zero_iff_left, ne_eq, smul_eq_zero_iff_right, two_ne_zero, div_eq_iff, vadd_right_cancel_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
rw : dist p s.center < |s.radius|
⊢ 0 < √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)

Tactic:
rw [Real.sqrt_pos, sub_pos, sq_lt_sq, abs_of_nonneg dist_nonneg]

Premises used: sub_pos, dist_nonneg, sq_lt_sq, Real.sqrt_pos, abs_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ dist p s.center < |s.radius|

Tactic:
lt_abs.2 (.inl hp)

Premises used: Iff.mpr, lt_abs, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ dist p s.center < |s.radius|

Tactic:
exact lt_abs.2 (.inl hp)

Premises used: Iff.mpr, lt_abs, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ 0 < √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)

Tactic:
have hvp : 0 < √(s.radius ^ 2 - dist p s.center ^ 2) := by
      rw [Real.sqrt_pos, sub_pos, sq_lt_sq, abs_of_nonneg dist_nonneg]
      exact lt_abs.2 (.inl hp)
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
hvp : 0 < √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)
⊢ ¬√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) = 0

Tactic:
hvp.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
hvp : 0 < √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)
⊢ ¬√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) = 0

Tactic:
exact hvp.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ ‖v‖ ≠ 0

Tactic:
simpa using hv0
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hpc : p ≠ s.center
inl : ∀ (h : dist p s.center < s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
inr : ∀ (h : dist p s.center = s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
inr₁ : ∀ (h : s.radius < dist p s.center), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2

Tactic:
rcases lt_trichotomy (dist p s.center) s.radius with h | h | h

Premises used: EuclideanGeometry.Sphere.center, Dist.dist, lt_trichotomy, EuclideanGeometry.Sphere.radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hpc : p ≠ s.center
h : dist p s.center < s.radius
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2

Tactic:
(ncard_inter_orthRadius_eq_two_of_dist_lt_radius h hpc).le

Premises used: EuclideanGeometry.Sphere.ncard_inter_orthRadius_eq_two_of_dist_lt_radius, Eq.le
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hpc : p ≠ s.center
h : dist p s.center < s.radius
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2

Tactic:
exact (ncard_inter_orthRadius_eq_two_of_dist_lt_radius h hpc).le

Premises used: EuclideanGeometry.Sphere.ncard_inter_orthRadius_eq_two_of_dist_lt_radius, Eq.le
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hpc : p ≠ s.center
h : dist p s.center = s.radius
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2

Tactic:
simp [inter_orthRadius_eq_singleton_of_dist_eq_radius h]

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_of_dist_eq_radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hpc : p ≠ s.center
h : s.radius < dist p s.center
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2

Tactic:
simp [inter_orthRadius_eq_empty_of_radius_lt_dist h]

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_radius_lt_dist
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₁ : ∃ (k : ℝ), x = k • y
h₃ : ‖z - y‖ = ‖z + y‖
obtain : ∀ (r : ℝ) (hr : x = r • y), ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|

Tactic:
obtain ⟨r, hr⟩ := h₁
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
rwa : angle z y = π / 2
rwa₁ : ‖z + y‖ = ‖z - y‖
rwa₂ rwa₃ rwa₄ rwa₅ : ‖z - y‖ = ‖z + y‖
⊢ ⟪z, y⟫ = 0

Tactic:
rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]

Premises used: InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, eq_comm, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ⟪z, y⟫ = 0

Tactic:
have hzy : ⟪z, y⟫ = 0 := by
    rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
rw : ⟪z, r • y⟫ = 0
rw₁ : r * ⟪z, y⟫ = 0
rw₂ : r * 0 = 0
rw₃ rw₄ : Eq (α := ℝ) 0 0
⊢ ⟪z, x⟫ = 0

Tactic:
rw [hr, inner_smul_right, hzy, mul_zero]

Premises used: MulZeroClass.mul_zero, inner_smul_right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
⊢ ⟪z, x⟫ = 0

Tactic:
have hzx : ⟪z, x⟫ = 0 := by rw [hr, inner_smul_right, hzy, mul_zero]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖

Tactic:
simp [sub_smul, add_smul, hr]

Premises used: sub_smul, add_smul
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)

Tactic:
simp_rw [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2 = |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2|

Tactic:
simp [abs_mul]

Premises used: abs_mul
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|

Tactic:
ring_nf
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|

Tactic:
simp [hr, norm_smul, mul_pow, sq_abs]

Premises used: norm_smul, sq_abs, mul_pow
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|

Tactic:
simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]

Premises used: norm_sub_sq_real, norm_add_sq_real, abs_sub_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
by₂ : ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2
by₃ : ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2 = |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2|
by₄ :
  |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
by₅ :
  |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
by₆ :
  |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|

Tactic:
calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
⊢ m -ᵥ p - (m -ᵥ a) = a -ᵥ p

Tactic:
have h1 := vsub_sub_vsub_cancel_left a p m
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
⊢ m -ᵥ a - (m -ᵥ p) = p -ᵥ a

Tactic:
have h1' := vsub_sub_vsub_cancel_left p a m
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
⊢ m -ᵥ q - (m -ᵥ p) = p -ᵥ q

Tactic:
have h2 := vsub_sub_vsub_cancel_left p q m
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
⊢ m -ᵥ q - (m -ᵥ a) = a -ᵥ q

Tactic:
have h3 := vsub_sub_vsub_cancel_left a q m
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
rw : b -ᵥ r = m -ᵥ r + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)
rw₁ : b -ᵥ r = m -ᵥ r + (b -ᵥ midpoint ℝ a b)
rw₂ : b -ᵥ r = b -ᵥ midpoint ℝ a b + (m -ᵥ r)
rw₃ rw₄ : b -ᵥ r = b -ᵥ r
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)

Tactic:
rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]

Premises used: vsub_add_vsub_cancel, midpoint_vsub_left, add_comm, right_vsub_midpoint
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
⊢ ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)

Tactic:
have h : ∀ r, b -ᵥ r = m -ᵥ r + (m -ᵥ a) := fun r => by
    rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
rw : ‖a -ᵥ p‖ * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|

Tactic:
rw [dist_eq_norm_vsub V]

Premises used: dist_eq_norm_vsub