awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
rwa :
  ∀ (h : InnerProductGeometry.angle (q -ᵥ p) (s.center -ᵥ p) = π / 2) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
rwa₁ :
  ∀ (h : ⟪q -ᵥ p, s.center -ᵥ p⟫_ℝ = 0) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
rwa₂ :
  ∀ (h : ⟪q -ᵥ p, -(p -ᵥ s.center)⟫_ℝ = 0) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
rwa₃ :
  ∀ (h : -⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
have rwa₄ : ∀ (h : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0) (hp : p ∈ s)
  (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center,
      inner_neg_right, neg_eq_zero] at h
Cleared hypotheses: h, hp, hp_mem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
⊢ LE.le (α := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) (s.orthRadius p)
have h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: have h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0 := by
    rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center,
      inner_neg_right, neg_eq_zero] at h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ 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
⊢ LE.le (α := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) (s.orthRadius p)
have hq : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ 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
⊢ LE.le (α := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) (s.orthRadius p)
have rw : {p, q} ⊆ (↑(s.orthRadius p) : Set P)
Tactic: rw [affineSpan_le]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ 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
⊢ {p, q} ⊆ (↑(s.orthRadius p) : Set P)
have hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p
Tactic: have hp : p ∈ s.orthRadius p := by
    simp [Sphere.self_mem_orthRadius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ 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, q} ⊆ (↑(s.orthRadius p) : Set P)
have simp_rw : p ∈ (↑(s.orthRadius p) : Set P) ∧ q ∈ (↑(s.orthRadius p) : Set P)
Tactic: simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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 p₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have hp₄ : ‖p₁ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃
Cleared hypotheses: hp₁, hp₂, hp₃, hp₂p₁, hp₂p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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 p₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have hp₅ : ‖p₂ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃
Cleared hypotheses: hp₁, hp₂, hp₃, hp₂p₁, hp₂p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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 p₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have hp₆ : ‖p₃ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃
Cleared hypotheses: hp₁, hp₂, hp₃, hp₂p₁, hp₂p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have 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₂))
Tactic: rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂))
⊢ ∡ p₁ s.center p₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have rw₁ : p₂ -ᵥ s.center ≠ p₁ -ᵥ s.center
Tactic: rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ ∡ p₁ s.center p₃ = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have rw₂ : p₂ -ᵥ s.center ≠ p₃ -ᵥ s.center
Tactic: rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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₄
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have hp₅ : ‖p₁ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄
Cleared hypotheses: hp₁, hp₂, hp₃, hp₄, hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have hp₆ : ‖p₂ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄
Cleared hypotheses: hp₁, hp₂, hp₃, hp₄, hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have hp₇ : ‖p₃ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄
Cleared hypotheses: hp₁, hp₂, hp₃, hp₄, hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have hp₈ : ‖p₄ -ᵥ s.center‖ = s.radius
Tactic: rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄
Cleared hypotheses: hp₁, hp₂, hp₃, hp₄, hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have 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₃))
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₄]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₃))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have rw₁ : p₂ -ᵥ s.center ≠ p₁ -ᵥ s.center
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₄]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have rw₂ : p₂ -ᵥ s.center ≠ p₄ -ᵥ s.center
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₄]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have rw₃ : p₃ -ᵥ s.center ≠ p₁ -ᵥ s.center
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₄]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have rw₄ : p₃ -ᵥ s.center ≠ p₄ -ᵥ s.center
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₄]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₄
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have 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₄)
Tactic: obtain ⟨s, hs⟩ := cospherical_iff_exists_sphere.1 h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
have hs₁ : p₁ ∈ s ∧ p₂ ∈ s ∧ p₃ ∈ s ∧ p₄ ∈ s
Tactic: simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff, Sphere.mem_coe] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂
⊢ ∡ p₁ s.center p₂ = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁)
have rw : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ 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₁)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂
⊢ ∡ p₁ s.center p₂ = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
have rw : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁) =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
Tactic: 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₁)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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 :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
⊢ ∡ p₁ s.center p₂ = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
have rw₁ : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center) =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
Tactic: 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₁)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₃ : p₁ ≠ p₃
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = (↑π : Real.Angle)
have rw : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ∡ p₁ s.center p₃ = (↑π : Real.Angle)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₃ : p₁ ≠ p₃
rw : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ∡ p₁ s.center p₃ = (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = (↑π : Real.Angle)
have rw₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center)) =
  (↑π : Real.Angle)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₃ : p₁ ≠ p₃
rw : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ∡ p₁ s.center p₃ = (↑π : Real.Angle)
rw₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center)) =
    (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = (↑π : Real.Angle)
have rw₂ : (↑π : Real.Angle) = (↑π : Real.Angle)
Tactic: 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]