[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
R : Type u_4
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H R
inst✝ : SmoothRing I R
⊢ Smooth I I fun a => -a
[PROOFSTEP]
simpa only [neg_one_mul] using @smooth_mul_left 𝕜 _ H _ E _ _ I R _ _ _ _ (-1)
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
⊢ Smooth (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) 𝓘(𝕜, 𝕜) fun p => p.fst * p.snd
[PROOFSTEP]
rw [smooth_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
⊢ (Continuous fun p => p.fst * p.snd) ∧
    ∀ (x : 𝕜 × 𝕜) (y : 𝕜),
      ContDiffOn 𝕜 ⊤
        (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘
          (fun p => p.fst * p.snd) ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)))
        ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
          ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)) ⁻¹'
            ((fun p => p.fst * p.snd) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source))
[PROOFSTEP]
refine' ⟨continuous_mul, fun x y => _⟩
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 ⊤
    (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘
      (fun p => p.fst * p.snd) ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)))
    ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
      ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)) ⁻¹'
        ((fun p => p.fst * p.snd) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source))
[PROOFSTEP]
simp only [Prod.mk.eta, mfld_simps]
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 ⊤ (fun p => p.fst * p.snd) Set.univ
[PROOFSTEP]
rw [contDiffOn_univ]
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiff 𝕜 ⊤ fun p => p.fst * p.snd
[PROOFSTEP]
exact contDiff_mul


[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
⊢ oangle o y z = 2 • oangle o (y - x) (z - x)
[PROOFSTEP]
have hy : y ≠ 0 := by
  rintro rfl
  rw [norm_zero, norm_eq_zero] at hxy
  exact hxyne hxy
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : ‖x‖ = ‖0‖
⊢ False
[PROOFSTEP]
rw [norm_zero, norm_eq_zero] at hxy
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : x = 0
⊢ False
[PROOFSTEP]
exact hxyne hxy
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
⊢ oangle o y z = 2 • oangle o (y - x) (z - x)
[PROOFSTEP]
have hx : x ≠ 0 := norm_ne_zero_iff.1 (hxy.symm ▸ norm_ne_zero_iff.2 hy)
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
⊢ oangle o y z = 2 • oangle o (y - x) (z - x)
[PROOFSTEP]
have hz : z ≠ 0 := norm_ne_zero_iff.1 (hxz ▸ norm_ne_zero_iff.2 hx)
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ oangle o y z = 2 • oangle o (y - x) (z - x)
[PROOFSTEP]
calc
  o.oangle y z = o.oangle x z - o.oangle x y := (o.oangle_sub_left hx hy hz).symm
  _ = π - (2 : ℤ) • o.oangle (x - z) x - (π - (2 : ℤ) • o.oangle (x - y) x) := by
    rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
      o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
  _ = (2 : ℤ) • (o.oangle (x - y) x - o.oangle (x - z) x) := by abel
  _ = (2 : ℤ) • o.oangle (x - y) (x - z) := by
    rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
  _ = (2 : ℤ) • o.oangle (y - x) (z - x) := by rw [← oangle_neg_neg, neg_sub, neg_sub]
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ oangle o x z - oangle o x y = ↑π - 2 • oangle o (x - z) x - (↑π - 2 • oangle o (x - y) x)
[PROOFSTEP]
rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
  o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ ↑π - 2 • oangle o (x - z) x - (↑π - 2 • oangle o (x - y) x) = 2 • (oangle o (x - y) x - oangle o (x - z) x)
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ ↑π - 2 • oangle o (x - z) x - (↑π - 2 • oangle o (x - y) x) = 2 • (oangle o (x - y) x - oangle o (x - z) x)
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ 2 • (oangle o (x - y) x - oangle o (x - z) x) = 2 • oangle o (x - y) (x - z)
[PROOFSTEP]
rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
[GOAL]
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ 2 • oangle o (x - y) (x - z) = 2 • oangle o (y - x) (z - x)
[PROOFSTEP]
rw [← oangle_neg_neg, neg_sub, neg_sub]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
[PROOFSTEP]
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
[PROOFSTEP]
rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ 2 • Orientation.oangle o (p₁ -ᵥ s.center - (p₂ -ᵥ s.center)) (p₃ -ᵥ s.center - (p₂ -ᵥ s.center)) =
    2 • Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
[PROOFSTEP]
simp [hp₂p₁, hp₂p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₂ -ᵥ s.center ≠ p₁ -ᵥ s.center
[PROOFSTEP]
simp [hp₂p₁, hp₂p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₂ -ᵥ s.center ≠ p₃ -ᵥ s.center
[PROOFSTEP]
simp [hp₂p₁, hp₂p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₄ : p₄ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
[PROOFSTEP]
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
[PROOFSTEP]
rw [oangle, oangle, ← vsub_sub_vsub_cancel_right p₁ p₂ s.center, ← vsub_sub_vsub_cancel_right p₄ p₂ s.center,
  o.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq _ _ _ _ hp₂ hp₃ hp₁ hp₄]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • Orientation.oangle o (p₁ -ᵥ s.center - (p₃ -ᵥ s.center)) (p₄ -ᵥ s.center - (p₃ -ᵥ s.center)) =
    2 • Orientation.oangle o (p₁ -ᵥ p₃) (p₄ -ᵥ p₃)
[PROOFSTEP]
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ p₂ -ᵥ s.center ≠ p₁ -ᵥ s.center
[PROOFSTEP]
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ p₂ -ᵥ s.center ≠ p₄ -ᵥ s.center
[PROOFSTEP]
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ p₃ -ᵥ s.center ≠ p₁ -ᵥ s.center
[PROOFSTEP]
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ p₃ -ᵥ s.center ≠ p₄ -ᵥ s.center
[PROOFSTEP]
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
[PROOFSTEP]
obtain ⟨s, hs⟩ := cospherical_iff_exists_sphere.1 h
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
s : Sphere P
hs : {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
[PROOFSTEP]
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff, Sphere.mem_coe] at hs
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
s : Sphere P
hs : p₁ ∈ s ∧ p₂ ∈ s ∧ p₃ ∈ s ∧ p₄ ∈ s
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
[PROOFSTEP]
exact Sphere.two_zsmul_oangle_eq hs.1 hs.2.1 hs.2.2.1 hs.2.2.2 hp₂p₁ hp₂p₄ hp₃p₁ hp₃p₄
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ∡ p₁ s.center p₂ = ↑π - 2 • ∡ s.center p₂ p₁
[PROOFSTEP]
rw [oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq h.symm (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ∡ p₁ s.center p₂ = ↑π - 2 • ∡ p₂ p₁ s.center
[PROOFSTEP]
rw [oangle_eq_pi_sub_two_zsmul_oangle_center_left hp₁ hp₂ h,
  oangle_eq_oangle_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₁p₃ : p₁ ≠ p₃
⊢ 2 • ∡ p₃ p₁ s.center + 2 • ∡ p₁ p₂ p₃ = ↑π
[PROOFSTEP]
rw [← oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃,
  oangle_eq_pi_sub_two_zsmul_oangle_center_right hp₁ hp₃ hp₁p₃, add_sub_cancel'_right]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (Real.Angle.tan (∡ p₂ p₁ s.center) / 2) • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
[PROOFSTEP]
obtain ⟨r, hr⟩ :=
  (dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint h).1 (dist_center_eq_dist_center_of_mem_sphere hp₁ hp₂)
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ (Real.Angle.tan (∡ p₂ p₁ s.center) / 2) • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
[PROOFSTEP]
rw [← hr, ← oangle_midpoint_rev_left, oangle, vadd_vsub_assoc]
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ (Real.Angle.tan
            (Orientation.oangle o (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))) /
          2) •
        ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
[PROOFSTEP]
nth_rw 1 [show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ p₂ -ᵥ p₁ = 2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)
[PROOFSTEP]
simp
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ (Real.Angle.tan
            (Orientation.oangle o (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (r • ↑(Orientation.rotation o ↑(π / 2)) (2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)) + (midpoint ℝ p₁ p₂ -ᵥ p₁))) /
          2) •
        ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
[PROOFSTEP]
rw [map_smul, smul_smul, add_comm, o.tan_oangle_add_right_smul_rotation_pi_div_two, mul_div_cancel _ (two_ne_zero' ℝ)]
[GOAL]
case intro.h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
[PROOFSTEP]
simpa using h.symm
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ ((Real.Angle.tan (∡ p₁ p₂ p₃))⁻¹ / 2) • ↑(Orientation.rotation o ↑(π / 2)) (p₃ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₃ = s.center
[PROOFSTEP]
convert tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₃ hp₁p₃
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_5
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ (Real.Angle.tan (∡ p₁ p₂ p₃))⁻¹ = Real.Angle.tan (∡ p₃ p₁ s.center)
[PROOFSTEP]
convert (Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi _).symm
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_5.convert_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ 2 • ∡ p₁ p₂ p₃ + 2 • ∡ p₃ p₁ s.center = ↑π
[PROOFSTEP]
rw [add_comm, two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ dist p₁ p₂ / Real.Angle.cos (∡ p₂ p₁ s.center) / 2 = s.radius
[PROOFSTEP]
rw [div_right_comm, div_eq_mul_inv _ (2 : ℝ), mul_comm,
  show (2 : ℝ)⁻¹ * dist p₁ p₂ = dist p₁ (midpoint ℝ p₁ p₂) by simp, ← mem_sphere.1 hp₁, ←
  tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₂ h, ← oangle_midpoint_rev_left, oangle,
  vadd_vsub_assoc, show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp, map_smul, smul_smul,
  div_mul_cancel _ (two_ne_zero' ℝ), @dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, vadd_vsub_assoc, add_comm,
  o.oangle_add_right_smul_rotation_pi_div_two, Real.Angle.cos_coe, Real.cos_arctan]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ 2⁻¹ * dist p₁ p₂ = dist p₁ (midpoint ℝ p₁ p₂)
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ p₂ -ᵥ p₁ = 2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (↑1 / Real.sqrt (↑1 + Real.Angle.tan (∡ p₂ p₁ s.center) ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        Real.Angle.tan (∡ p₂ p₁ s.center) • ↑(Orientation.rotation o ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖
case h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / Real.sqrt (1 + Real.Angle.tan (∡ p₂ p₁ s.center) ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        Real.Angle.tan (∡ p₂ p₁ s.center) • ↑(Orientation.rotation o ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖
case h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
[PROOFSTEP]
rw [one_div, div_inv_eq_mul, ← mul_self_inj (mul_nonneg (norm_nonneg _) (Real.sqrt_nonneg _)) (norm_nonneg _),
  norm_add_sq_eq_norm_sq_add_norm_sq_real (o.inner_smul_rotation_pi_div_two_right _ _), ← mul_assoc, mul_comm,
  mul_comm _ (Real.sqrt _), ← mul_assoc, ← mul_assoc, Real.mul_self_sqrt (add_nonneg zero_le_one (sq_nonneg _)),
  norm_smul, LinearIsometryEquiv.norm_map]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + Real.Angle.tan (∡ p₂ p₁ s.center) ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
        (‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
case h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
[PROOFSTEP]
swap
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
[PROOFSTEP]
simpa using h.symm
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + Real.Angle.tan (∡ p₂ p₁ s.center) ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
        (‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
[PROOFSTEP]
conv_rhs => rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, abs_mul_abs_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
| ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
    ‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
      (‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
[PROOFSTEP]
rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, abs_mul_abs_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
| ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
    ‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
      (‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
[PROOFSTEP]
rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, abs_mul_abs_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
| ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
    ‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
      (‖Real.Angle.tan (∡ p₂ p₁ s.center)‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
[PROOFSTEP]
rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, abs_mul_abs_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + Real.Angle.tan (∡ p₂ p₁ s.center) ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      Real.Angle.tan (∡ p₂ p₁ s.center) * Real.Angle.tan (∡ p₂ p₁ s.center) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
        ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ dist p₁ p₂ / Real.Angle.cos (∡ p₂ p₁ s.center) = 2 * s.radius
[PROOFSTEP]
rw [← dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₂ h, mul_div_cancel' _ (two_ne_zero' ℝ)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₁ p₃ / |Real.Angle.sin (∡ p₁ p₂ p₃)| / 2 = s.radius
[PROOFSTEP]
convert dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₃ hp₁p₃
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |Real.Angle.sin (∡ p₁ p₂ p₃)| = Real.Angle.cos (∡ p₃ p₁ s.center)
[PROOFSTEP]
rw [←
  Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi
    (two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃),
  _root_.abs_of_nonneg (Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two.2 _)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |Real.Angle.toReal (∡ p₃ p₁ s.center)| ≤ π / 2
[PROOFSTEP]
exact (abs_oangle_center_right_toReal_lt_pi_div_two hp₁ hp₃).le
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₁ p₃ / |Real.Angle.sin (∡ p₁ p₂ p₃)| = 2 * s.radius
[PROOFSTEP]
rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃, mul_div_cancel' _ (two_ne_zero' ℝ)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : Simplex.points t₁ i₁ = Simplex.points t₂ i₁
h₃ : Simplex.points t₁ i₃ = Simplex.points t₂ i₃
h₂ :
  2 • ∡ (Simplex.points t₁ i₁) (Simplex.points t₁ i₂) (Simplex.points t₁ i₃) =
    2 • ∡ (Simplex.points t₂ i₁) (Simplex.points t₂ i₂) (Simplex.points t₂ i₃)
⊢ Simplex.circumsphere t₁ = Simplex.circumsphere t₂
[PROOFSTEP]
rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃, t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
  -- Porting note: was `congrm ⟨((_ : ℝ)⁻¹ / 2) • _ +ᵥ _, _ / _ / 2⟩` and five more linesReal.Angle.tan_eq_of_two_zsmul_eq
    h₂,
  Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
let t'p : Fin 3 → P := Function.update t.points i₂ p
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h₁ : t'p i₁ = t.points i₁ := by simp [h₁₂]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
⊢ t'p i₁ = Simplex.points t i₁
[PROOFSTEP]
simp [h₁₂]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h₂ : t'p i₂ = p := by simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
⊢ t'p i₂ = p
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h₃ : t'p i₃ = t.points i₃ := by simp [h₂₃.symm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
⊢ t'p i₃ = Simplex.points t i₃
[PROOFSTEP]
simp [h₂₃.symm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have ha : AffineIndependent ℝ t'p :=
  by
  rw [affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃, h₁, h₂, h₃, collinear_iff_of_two_zsmul_oangle_eq h, ←
    affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃]
  exact t.Independent
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
⊢ AffineIndependent ℝ t'p
[PROOFSTEP]
rw [affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃, h₁, h₂, h₃, collinear_iff_of_two_zsmul_oangle_eq h, ←
  affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
⊢ AffineIndependent ℝ t.points
[PROOFSTEP]
exact t.Independent
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
let t' : Triangle ℝ P := ⟨t'p, ha⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h₁' : t'.points i₁ = t.points i₁ := h₁
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
h₁' : Simplex.points t' i₁ = Simplex.points t i₁
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h₂' : t'.points i₂ = p := h₂
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
h₁' : Simplex.points t' i₁ = Simplex.points t i₁
h₂' : Simplex.points t' i₂ = p
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h₃' : t'.points i₃ = t.points i₃ := h₃
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
h₁' : Simplex.points t' i₁ = Simplex.points t i₁
h₂' : Simplex.points t' i₂ = p
h₃' : Simplex.points t' i₃ = Simplex.points t i₃
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
have h' :
  (2 : ℤ) • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) = (2 : ℤ) • ∡ (t.points i₁) (t.points i₂) (t.points i₃) := by
  rwa [h₁', h₂', h₃']
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
h₁' : Simplex.points t' i₁ = Simplex.points t i₁
h₂' : Simplex.points t' i₂ = p
h₃' : Simplex.points t' i₃ = Simplex.points t i₃
⊢ 2 • ∡ (Simplex.points t' i₁) (Simplex.points t' i₂) (Simplex.points t' i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
[PROOFSTEP]
rwa [h₁', h₂', h₃']
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
h₁' : Simplex.points t' i₁ = Simplex.points t i₁
h₂' : Simplex.points t' i₂ = p
h₃' : Simplex.points t' i₃ = Simplex.points t i₃
h' :
  2 • ∡ (Simplex.points t' i₁) (Simplex.points t' i₂) (Simplex.points t' i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
⊢ p ∈ Simplex.circumsphere t
[PROOFSTEP]
rw [← circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ h₁' h₃' h', ← h₂']
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  2 • ∡ (Simplex.points t i₁) p (Simplex.points t i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = Simplex.points t i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = Simplex.points t i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, Independent := ha }
h₁' : Simplex.points t' i₁ = Simplex.points t i₁
h₂' : Simplex.points t' i₂ = p
h₃' : Simplex.points t' i₃ = Simplex.points t i₃
h' :
  2 • ∡ (Simplex.points t' i₁) (Simplex.points t' i₂) (Simplex.points t' i₃) =
    2 • ∡ (Simplex.points t i₁) (Simplex.points t i₂) (Simplex.points t i₃)
⊢ Simplex.points t' i₂ ∈ Simplex.circumsphere t'
[PROOFSTEP]
exact Simplex.mem_circumsphere _ _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄}
[PROOFSTEP]
have hn' : ¬Collinear ℝ ({ p₁, p₃, p₄ } : Set P) := by rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ ¬Collinear ℝ {p₁, p₃, p₄}
[PROOFSTEP]
rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄}
[PROOFSTEP]
let t₁ : Affine.Triangle ℝ P := ⟨![p₁, p₂, p₄], affineIndependent_iff_not_collinear_set.2 hn⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
⊢ Cospherical {p₁, p₂, p₃, p₄}
[PROOFSTEP]
let t₂ : Affine.Triangle ℝ P := ⟨![p₁, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hn'⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ Cospherical {p₁, p₂, p₃, p₄}
[PROOFSTEP]
rw [cospherical_iff_exists_sphere]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ ∃ s, {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
[PROOFSTEP]
refine' ⟨t₂.circumsphere, _⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
[PROOFSTEP]
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ p₁ ∈
      Metric.sphere
        (Affine.Simplex.circumsphere
            { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).center
        (Affine.Simplex.circumsphere
            { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).radius ∧
    p₂ ∈
        Metric.sphere
          (Affine.Simplex.circumsphere
              { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).center
          (Affine.Simplex.circumsphere
              { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).radius ∧
      p₃ ∈
          Metric.sphere
            (Affine.Simplex.circumsphere
                { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).center
            (Affine.Simplex.circumsphere
                { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).radius ∧
        p₄ ∈
          Metric.sphere
            (Affine.Simplex.circumsphere
                { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).center
            (Affine.Simplex.circumsphere
                { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).radius
[PROOFSTEP]
refine' ⟨t₂.mem_circumsphere 0, _, t₂.mem_circumsphere 1, t₂.mem_circumsphere 2⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ p₂ ∈
    Metric.sphere
      (Affine.Simplex.circumsphere
          { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).center
      (Affine.Simplex.circumsphere
          { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }).radius
[PROOFSTEP]
rw [Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq (by decide : (0 : Fin 3) ≠ 1)
    (by decide : (0 : Fin 3) ≠ 2) (by decide) (show t₂.points 0 = t₁.points 0 from rfl) rfl h.symm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ 0 ≠ 1
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ 0 ≠ 2
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ 1 ≠ 2
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₂, p₄]) }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₁, p₃, p₄]) }
⊢ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₁).center (Affine.Simplex.circumsphere t₁).radius
[PROOFSTEP]
exact t₁.mem_circumsphere 1
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
by_cases hc : Collinear ℝ ({ p₁, p₂, p₄ } : Set P)
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
by_cases he : p₁ = p₄
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
rw [he, Set.insert_eq_self.2 (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))]
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}
[PROOFSTEP]
by_cases hl : Collinear ℝ ({ p₂, p₃, p₄ } : Set P)
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : Collinear ℝ {p₂, p₃, p₄}
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}
[PROOFSTEP]
exact Or.inr hl
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}
[PROOFSTEP]
rw [or_iff_left hl]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
⊢ Cospherical {p₂, p₃, p₄}
[PROOFSTEP]
let t : Affine.Triangle ℝ P := ⟨![p₂, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hl⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }
⊢ Cospherical {p₂, p₃, p₄}
[PROOFSTEP]
rw [cospherical_iff_exists_sphere]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }
⊢ ∃ s, {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
[PROOFSTEP]
refine' ⟨t.circumsphere, _⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }
⊢ {p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius
[PROOFSTEP]
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }
⊢ p₂ ∈
      Metric.sphere
        (Affine.Simplex.circumsphere
            { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }).center
        (Affine.Simplex.circumsphere
            { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }).radius ∧
    p₃ ∈
        Metric.sphere
          (Affine.Simplex.circumsphere
              { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }).center
          (Affine.Simplex.circumsphere
              { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }).radius ∧
      p₄ ∈
        Metric.sphere
          (Affine.Simplex.circumsphere
              { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }).center
          (Affine.Simplex.circumsphere
              { points := ![p₂, p₃, p₄], Independent := (_ : AffineIndependent ℝ ![p₂, p₃, p₄]) }).radius
[PROOFSTEP]
exact ⟨t.mem_circumsphere 0, t.mem_circumsphere 1, t.mem_circumsphere 2⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
have hc' : Collinear ℝ ({ p₁, p₃, p₄ } : Set P) := by rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
⊢ Collinear ℝ {p₁, p₃, p₄}
[PROOFSTEP]
rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
refine' Or.inr _
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
rw [Set.insert_comm p₁ p₂] at hc
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₂, p₁, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
rwa [Set.insert_comm p₁ p₂,
  hc'.collinear_insert_iff_of_ne (Set.mem_insert _ _)
    (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) he]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
exact Or.inl (cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hc)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
rcases cospherical_or_collinear_of_two_zsmul_oangle_eq h with (hc | hc)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Cospherical {p₁, p₂, p₃, p₄}
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
exact Or.inl ⟨hc, coplanar_of_fact_finrank_eq_two _⟩
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
exact Or.inr hc