awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q

Tactic:
simp [Sphere.mem_orthRadius_iff_inner_left, h_ortho]

Premises used: EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q

Tactic:
have hq : q ∈ s.orthRadius p := by
    simp [Sphere.mem_orthRadius_iff_inner_left, h_ortho]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
rw : {p, q} ⊆ (↑(s.orthRadius p) : Set P)
⊢ LE.le (α := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) (s.orthRadius p)

Tactic:
rw [affineSpan_le]

Premises used: affineSpan_le
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p

Tactic:
simp [Sphere.self_mem_orthRadius]

Premises used: EuclideanGeometry.Sphere.self_mem_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p

Tactic:
have hp : p ∈ s.orthRadius p := by
    simp [Sphere.self_mem_orthRadius]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp_1 : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p
simp_rw : p ∈ (↑(s.orthRadius p) : Set P) ∧ q ∈ (↑(s.orthRadius p) : Set P)
⊢ {p, q} ⊆ (↑(s.orthRadius p) : Set P)

Tactic:
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp_1 : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p
⊢ p ∈ (↑(s.orthRadius p) : Set P) ∧ q ∈ (↑(s.orthRadius p) : Set P)

Tactic:
⟨hp, hq⟩

Premises used: And.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 : ∠ q p s.center = π / 2
hp_1 : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p
⊢ p ∈ (↑(s.orthRadius p) : Set P) ∧ q ∈ (↑(s.orthRadius p) : Set P)

Tactic:
exact ⟨hp, hq⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hp : p ∈ s
⊢ s.IsTangentAt p (affineSpan ℝ {p, q}) ↔ ∠ q p s.center = π / 2

Tactic:
⟨fun h ↦ IsTangentAt.angle_eq_pi_div_two h (right_mem_affineSpan_pair ℝ p q),
    fun h ↦ IsTangentAt_of_angle_eq_pi_div_two h hp⟩

Premises used: Real, EuclideanGeometry.Sphere.IsTangentAt.angle_eq_pi_div_two, right_mem_affineSpan_pair, EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hp : p ∈ s
⊢ s.IsTangentAt p (affineSpan ℝ {p, q}) ↔ ∠ q p s.center = π / 2

Tactic:
exact ⟨fun h ↦ IsTangentAt.angle_eq_pi_div_two h (right_mem_affineSpan_pair ℝ p q),
    fun h ↦ IsTangentAt_of_angle_eq_pi_div_two h hp⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₁ -ᵥ s.center‖ = s.radius
⊢ ‖p₂ -ᵥ s.center‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₁ -ᵥ s.center‖ = s.radius
hp₅ : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ ‖p₃ -ᵥ s.center‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₁ -ᵥ s.center‖ = s.radius
hp₅ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₆ : ‖p₃ -ᵥ s.center‖ = s.radius
⊢ p₂ ≠ p₁

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₁ -ᵥ s.center‖ = s.radius
hp₅ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₆ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₂ : p₂ ≠ p₁
⊢ p₂ ≠ p₃

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₃
rw :
  HSMul.hSMul (α := ℤ) 2
      (Orientation.oangle «o» (p₁ -ᵥ s.center - (p₂ -ᵥ s.center)) (p₃ -ᵥ s.center - (p₂ -ᵥ s.center))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle «o» (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
rw₁ : p₂ -ᵥ s.center ≠ p₁ -ᵥ s.center
rw₂ : p₂ -ᵥ s.center ≠ p₃ -ᵥ s.center
⊢ ∡ p₁ s.center p₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)

Tactic:
rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃]

Premises used: EuclideanGeometry.oangle, EuclideanGeometry.o, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₃
⊢ HSMul.hSMul (α := ℤ) 2
      (Orientation.oangle «o» (p₁ -ᵥ s.center - (p₂ -ᵥ s.center)) (p₃ -ᵥ s.center - (p₂ -ᵥ s.center))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle «o» (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))

Tactic:
simp [hp₂p₁, hp₂p₃]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Tactic:
simp [hp₂p₁, hp₂p₃]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Tactic:
simp [hp₂p₁, hp₂p₃]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
⊢ ‖p₁ -ᵥ s.center‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
hp₅ : ‖p₁ -ᵥ s.center‖ = s.radius
⊢ ‖p₂ -ᵥ s.center‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
hp₅ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₆ : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ ‖p₃ -ᵥ s.center‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
hp₅ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₆ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₇ : ‖p₃ -ᵥ s.center‖ = s.radius
⊢ ‖p₄ -ᵥ s.center‖ = s.radius

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
hp₅ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₆ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₇ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₈ : ‖p₄ -ᵥ s.center‖ = s.radius
⊢ p₂ ≠ p₁

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
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₁
⊢ p₂ ≠ p₄

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
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₄
⊢ p₃ ≠ p₁

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
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₁
⊢ p₃ ≠ p₄

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

Premises used: EuclideanGeometry.mem_sphere, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
rw :
  HSMul.hSMul (α := ℤ) 2
      (Orientation.oangle «o» (p₁ -ᵥ s.center - (p₃ -ᵥ s.center)) (p₄ -ᵥ s.center - (p₃ -ᵥ s.center))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle «o» (p₁ -ᵥ p₃) (p₄ -ᵥ p₃))
rw₁ : p₂ -ᵥ s.center ≠ p₁ -ᵥ s.center
rw₂ : p₂ -ᵥ s.center ≠ p₄ -ᵥ s.center
rw₃ : p₃ -ᵥ s.center ≠ p₁ -ᵥ s.center
rw₄ : p₃ -ᵥ s.center ≠ p₄ -ᵥ s.center
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)

Tactic:
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₄]

Premises used: EuclideanGeometry.oangle, EuclideanGeometry.Sphere.center, vsub_sub_vsub_cancel_right, Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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₄
⊢ HSMul.hSMul (α := ℤ) 2
      (Orientation.oangle «o» (p₁ -ᵥ s.center - (p₃ -ᵥ s.center)) (p₄ -ᵥ s.center - (p₃ -ᵥ s.center))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle «o» (p₁ -ᵥ p₃) (p₄ -ᵥ p₃))

Tactic:
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Tactic:
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Tactic:
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Tactic:
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Tactic:
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical (P := P) {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
obtain :
  ∀ (s : Sphere P) (hs : {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius),
    HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)

Tactic:
obtain ⟨s, hs⟩ := cospherical_iff_exists_sphere.1 h

Premises used: Iff.mp, EuclideanGeometry.cospherical_iff_exists_sphere
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical (P := P) {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
⊢ p₁ ∈ s ∧ p₂ ∈ s ∧ p₃ ∈ s ∧ p₄ ∈ s

Tactic:
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff, Sphere.mem_coe] at hs

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff, EuclideanGeometry.Sphere.mem_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical (P := P) {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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)

Tactic:
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₄

Premises used: And.right, And.left, EuclideanGeometry.Sphere.two_zsmul_oangle_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical (P := P) {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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)

Tactic:
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₄

Premises used: And.right, And.left, EuclideanGeometry.Sphere.two_zsmul_oangle_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
rw rw₁ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁)
⊢ ∡ p₁ s.center p₂ = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁)

Tactic:
rw [oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq h.symm
      (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

Premises used: EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq, EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere', Ne.symm