awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
y₁ :
  o.oangle x z - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
y₂ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x)) =
    HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x)
y₃ :
  HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x) = HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z))
y₄ : HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))

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

Premises used: Orientation.oangle, Real.pi, Real.Angle.coe, HSub.hSub, Orientation.oangle_sub_left, HSMul.hSMul, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
r : ℝ
hx : ‖x‖ = r
hy : ‖y‖ = r
hz : ‖z‖ = r
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))

Tactic:
o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq hxyne hxzne (hy.symm ▸ hx) (hz.symm ▸ hx)

Premises used: Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq, Eq.rec, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x₁ x₂ y z : V
hx₁yne : x₁ ≠ y
hx₁zne : x₁ ≠ z
hx₂yne : x₂ ≠ y
hx₂zne : x₂ ≠ z
r : ℝ
hx₁ : ‖x₁‖ = r
hx₂ : ‖x₂‖ = r
hy : ‖y‖ = r
hz : ‖z‖ = r
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x₁) (z - x₁)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x₂) (z - x₂))

Tactic:
o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real hx₁yne hx₁zne hx₁ hy hz ▸
    o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real hx₂yne hx₂zne hx₂ hy hz

Premises used: Eq.rec, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
rw : ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
⊢ ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s

Tactic:
rw [mem_sphere', EuclideanGeometry.angle,
    ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]

Premises used: EuclideanGeometry.mem_sphere', InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, EuclideanGeometry.angle
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
⊢ o = midpoint ℝ p₁ p₃

Tactic:
have h_center : o = midpoint ℝ p₁ p₃ := hd.midpoint_eq_center.symm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
rw :
  ⟪p₁ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪p₁ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius

Tactic:
rw [← vsub_add_vsub_cancel p₁ o p₂, ← vsub_add_vsub_cancel p₃ o p₂,
    inner_add_left, inner_add_right, inner_add_right]

Premises used: vsub_add_vsub_cancel, inner_add_left, inner_add_right
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
rw : p₁ -ᵥ midpoint ℝ p₁ p₃ = -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₁ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₂ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₃ -ᵥ p₁)
rw₃ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(p₃ -ᵥ p₁))
rw₄ rw₅ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃)
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)

Tactic:
rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]

Premises used: smul_neg, neg_vsub_eq_vsub_rev, right_vsub_midpoint, left_vsub_midpoint
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)

Tactic:
have h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o) := by
    rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
rw :
  -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + -⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius
⊢ ⟪p₁ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪p₁ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius

Tactic:
rw [h_opp, inner_neg_left, inner_neg_left, real_inner_comm (p₃ -ᵥ o) (o -ᵥ p₂)]

Premises used: VSub.vsub, real_inner_comm, inner_neg_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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
ring_nf : -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + -⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius

Tactic:
ring_nf
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
rw : s.radius = dist o p₂ ↔ dist s.center p₂ = s.radius
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius

Tactic:
rw [neg_add_eq_zero, real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub,
    real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub, sq_eq_sq₀ dist_nonneg dist_nonneg,
    mem_sphere.mp hd.right_mem]

Premises used: EuclideanGeometry.Sphere.IsDiameter.right_mem, dist_nonneg, real_inner_self_eq_norm_sq, EuclideanGeometry.mem_sphere, Iff.mp, dist_eq_norm_vsub, sq_eq_sq₀, neg_add_eq_zero
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ s.radius = dist o p₂ ↔ dist s.center p₂ = s.radius

Tactic:
eq_comm

Premises used: eq_comm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ s.radius = dist o p₂ ↔ dist s.center p₂ = s.radius

Tactic:
exact eq_comm

Premises used: eq_comm
-- 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
p₁ p₂ p₃ : P
⊢ ∠ p₁ p₂ p₃ = π / 2 ↔ Membership.mem (γ := Sphere P) (Sphere.ofDiameter p₁ p₃) p₂

Tactic:
angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter (Sphere.isDiameter_ofDiameter p₁ p₃)

Premises used: EuclideanGeometry.Sphere.isDiameter_ofDiameter, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
⊢ FiniteDimensional ℝ V

Tactic:
haveI : FiniteDimensional ℝ V := .of_finrank_eq_succ (Fact.out : finrank ℝ V = 2)
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
⊢ 0 = π / 2

Tactic:
rw [h, angle_self_of_ne hne₂₃.symm] at hangle

Premises used: EuclideanGeometry.angle_self_of_ne, Ne.symm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
hangle₁ : 0 = π / 2
⊢ FiniteDimensional ℝ V

Tactic:
rw [h, angle_self_of_ne hne₂₃.symm] at hangle

Premises used: EuclideanGeometry.angle_self_of_ne, Ne.symm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
hangle₁ : 0 = π / 2
this₁ : FiniteDimensional ℝ V
⊢ p₁ = p₃

Tactic:
rw [h, angle_self_of_ne hne₂₃.symm] at hangle

Premises used: EuclideanGeometry.angle_self_of_ne, Ne.symm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : 0 = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : -(HMul.hMul (α := ℝ) 2 0 - 1 * π) + (0 - π) = 0
⊢ False

Tactic:
linarith [Real.pi_pos]

Premises used: Real.pi_pos
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
⊢ p₁ ≠ p₃

Tactic:
have hne₁₃ : p₁ ≠ p₃ := fun h ↦ by
    rw [h, angle_self_of_ne hne₂₃.symm] at hangle; linarith [Real.pi_pos]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
⊢ IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃

Tactic:
have hd := Sphere.isDiameter_ofDiameter p₁ p₃
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
by_contra : ∀ (hne : ¬s = Sphere.ofDiameter p₁ p₃), False
⊢ s = Sphere.ofDiameter p₁ p₃

Tactic:
by_contra hne
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
⊢ p₂ = p₁ ∨ p₂ = p₃

Tactic:
have := eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
      (Fact.out : finrank ℝ V = 2) hne hne₁₃ hp₁ hp₃ hp₂
      hd.left_mem hd.right_mem (angle_eq_pi_div_two_iff_mem_sphere_ofDiameter.mp hangle)
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this_1 : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
this : p₂ = p₁ ∨ p₂ = p₃
⊢ False

Tactic:
this.elim hne₁₂.symm hne₂₃

Premises used: Ne.symm, Or.elim
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this_1 : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
this : p₂ = p₁ ∨ p₂ = p₃
⊢ False

Tactic:
exact this.elim hne₁₂.symm hne₂₃

Premises used: Ne.symm, Or.elim
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
⊢ s = Sphere.ofDiameter p₁ p₃

Tactic:
have h_eq : s = Sphere.ofDiameter p₁ p₃ := by
    by_contra hne
    have := eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
      (Fact.out : finrank ℝ V = 2) hne hne₁₃ hp₁ hp₃ hp₂
      hd.left_mem hd.right_mem (angle_eq_pi_div_two_iff_mem_sphere_ofDiameter.mp hangle)
    exact this.elim hne₁₂.symm hne₂₃
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
h_eq : s = Sphere.ofDiameter p₁ p₃
⊢ s.IsDiameter p₁ p₃

Tactic:
h_eq ▸ hd

Premises used: Eq.rec, Eq.symm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
h_eq : s = Sphere.ofDiameter p₁ p₃
⊢ s.IsDiameter p₁ p₃

Tactic:
exact h_eq ▸ hd
-- 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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq_mem : q ∈ as
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0

Tactic:
have h1 := IsTangentAt.inner_left_eq_zero_of_mem h hq_mem
-- 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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq_mem : q ∈ as
h1 : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2

Tactic:
rw [inner_eq_zero_iff_angle_eq_pi_div_two] at h1

Premises used: InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two
-- 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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
rw : π - π / 2 = π / 2
⊢ ∠ q p s.center = π / 2

Tactic:
rw [angle, ← neg_vsub_eq_vsub_rev _ s.center, angle_neg_right, h1]

Premises used: InnerProductGeometry.angle_neg_right, EuclideanGeometry.Sphere.center, neg_vsub_eq_vsub_rev, EuclideanGeometry.angle
-- 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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₆ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
linarith₉ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₀ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₂ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
linarith₁₄ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₅ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₆ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
linarith₁₇ : π / 2 < π - π / 2 → 1 * π - (2 * π - 1 * π) = 0
⊢ π - π / 2 = π / 2

Tactic:
linarith
-- 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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p

Tactic:
have hp_mem := left_mem_affineSpan_pair ℝ p q
-- 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
⊢ s.IsTangentAt p (affineSpan ℝ {p, q})

Tactic:
⟨hp, hp_mem, ?_⟩

Premises used: EuclideanGeometry.Sphere.IsTangentAt.mk
-- 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
refine : LE.le (α := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) (s.orthRadius p)
⊢ s.IsTangentAt p (affineSpan ℝ {p, q})

Tactic:
refine ⟨hp, hp_mem, ?_⟩
-- 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
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
rwa₄ rwa₅ rwa₆ 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

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

Premises used: inner_neg_right, neg_eq_zero, EuclideanGeometry.Sphere.center, neg_vsub_eq_vsub_rev, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, EuclideanGeometry.angle
-- 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
⊢ ⟪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