awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
h₁₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
h₁₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ h₁₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
h₁₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
h₁₃ h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
h₁₃ h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
h₁₂ h₁₃ h₂₃ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2

Tactic:
simp [*] at *
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
i : Fin 3
rw :
  (↑2 : ℝ) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
⊢ dist (t.points i) (Simplex.centroid t) = 2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
rw [Affine.Simplex.dist_point_centroid]

Premises used: Affine.Simplex.dist_point_centroid
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
i : Fin 3
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
⊢ (↑2 : ℝ) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
i : Fin 3
rw :
  HAdd.hAdd (α := ℝ) (↑2 : ℝ) 1 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
⊢ dist (t.points i) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
rw [Affine.Simplex.dist_point_faceOppositeCentroid]

Premises used: Affine.Simplex.dist_point_faceOppositeCentroid
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
t : Triangle ℝ P
i : Fin 3
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (↑(HAdd.hAdd (α := ℕ) 2 1) : ℝ) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
⊢ HAdd.hAdd (α := ℝ) (↑2 : ℝ) 1 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : MetricSpace P
inst_1 : Nonempty P
⊢ Nonempty.{u_2 + 1} (Sphere P)

Tactic:
⟨⟨Classical.arbitrary P, 0⟩⟩

Premises used: Nonempty.intro, EuclideanGeometry.Sphere.mk, Classical.arbitrary, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
c : P
r : ℝ
⊢ center { center := c, radius := r : Sphere P } = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
c : P
r : ℝ
⊢ radius { center := c, radius := r : Sphere P } = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
center : Sphere.center { center := s.center, radius := s.radius : Sphere P } = s.center
radius : Sphere.radius { center := s.center, radius := s.radius : Sphere P } = s.radius
⊢ { center := s.center, radius := s.radius } = s

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
⊢ center { center := s.center, radius := s.radius : Sphere P } = s.center

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
⊢ radius { center := s.center, radius := s.radius : Sphere P } = s.radius

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
c : P
r : ℝ
⊢ Metric.sphere (center { center := c, radius := r : Sphere P }) (radius { center := c, radius := r : Sphere P }) =
    Metric.sphere c r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
s : Sphere P
⊢ p ∈ Metric.sphere s.center s.radius ↔ p ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
s : Sphere P
⊢ dist p s.center = s.radius ↔ p ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
s : Sphere P
⊢ p ∈ s ↔ dist p s.center = s.radius

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
s : Sphere P
⊢ p ∈ s ↔ dist s.center p = s.radius

Tactic:
Metric.mem_sphere'

Premises used: Metric.mem_sphere'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
s : Sphere P
⊢ ps ⊆ Metric.sphere s.center s.radius ↔ ∀ p ∈ ps, p ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
ps : Set P
s : Sphere P
hp : p ∈ ps
hps : ps ⊆ Metric.sphere s.center s.radius
⊢ dist p s.center = s.radius

Tactic:
mem_sphere.1 (Sphere.mem_coe.1 (Set.mem_of_mem_of_subset hp hps))

Premises used: EuclideanGeometry.mem_sphere, EuclideanGeometry.Sphere.mem_coe, Set.mem_of_mem_of_subset, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p c : P
ps : Set P
r : ℝ
hp : p ∈ ps
hps : ps ⊆ Metric.sphere (Sphere.center { center := c, radius := r }) (Sphere.radius { center := c, radius := r })
⊢ dist p c = r

Tactic:
dist_of_mem_subset_sphere hp hps

Premises used: EuclideanGeometry.dist_of_mem_subset_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
rw : s₁ ≠ s₂ ↔ ¬(s₁.center = s₂.center ∧ s₁.radius = s₂.radius)
rw₁ rw₂ : s₁ ≠ s₂ ↔ ¬s₁ = s₂
⊢ s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius

Tactic:
rw [← not_and_or, ← Sphere.ext_iff]

Premises used: not_and_or, EuclideanGeometry.Sphere.ext_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
⊢ s₁.center = s₂.center ↔ s₁ = s₂

Tactic:
⟨fun h => Sphere.ext h ?_, fun h => h ▸ rfl⟩

Premises used: EuclideanGeometry.Sphere.ext, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
refine : ∀ (h : s₁.center = s₂.center), s₁.radius = s₂.radius
⊢ s₁.center = s₂.center ↔ s₁ = s₂

Tactic:
refine ⟨fun h => Sphere.ext h ?_, fun h => h ▸ rfl⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
⊢ dist p s₁.center = s₁.radius

Tactic:
rw [mem_sphere] at hs₁ hs₂

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
hs₃ : dist p s₁.center = s₁.radius
⊢ dist p s₂.center = s₂.radius

Tactic:
rw [mem_sphere] at hs₁ hs₂

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
hs₃ : dist p s₁.center = s₁.radius
hs₄ : dist p s₂.center = s₂.radius
⊢ s₁.center = s₂.center

Tactic:
rw [mem_sphere] at hs₁ hs₂

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : dist p s₁.center = s₁.radius
hs₂ : dist p s₂.center = s₂.radius
h : s₁.center = s₂.center
rw : dist p s₁.center = s₂.radius
rw₁ : dist p s₁.center = dist p s₂.center
rw₂ rw₃ : dist p s₂.center = dist p s₂.center
⊢ s₁.radius = s₂.radius

Tactic:
rw [← hs₁, ← hs₂, h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
⊢ s₁.center ≠ s₂.center ↔ s₁ ≠ s₂

Tactic:
(Sphere.center_eq_iff_eq_of_mem hs₁ hs₂).not

Premises used: Iff.not, EuclideanGeometry.Sphere.center_eq_iff_eq_of_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
rw : s.radius = dist p₂ s.center
rw₁ rw₂ : s.radius = s.radius
⊢ dist p₁ s.center = dist p₂ s.center

Tactic:
rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
rw : s.radius = dist s.center p₂
rw₁ rw₂ : s.radius = s.radius
⊢ dist s.center p₁ = dist s.center p₂

Tactic:
rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]

Premises used: EuclideanGeometry.mem_sphere', Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
h : p ∈ s
⊢ 0 ≤ s.radius

Tactic:
Metric.nonneg_of_mem_sphere h

Premises used: Metric.nonneg_of_mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
⊢ s.center ∈ s ↔ s.radius = 0

Tactic:
simp [mem_sphere, eq_comm]

Premises used: eq_comm, EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
⊢ Cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius

Tactic:
Iff.rfl

Premises used: EuclideanGeometry.Cospherical, Iff.rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
⊢ Cospherical ps ↔ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
refine_1 : ∀ (h : Cospherical ps), ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
refine_2 : ∀ (h : ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius), Cospherical ps
⊢ Cospherical ps ↔ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
h : Cospherical ps
refine_1 : ∀ (c : P) (r : ℝ) (h : ∀ p ∈ ps, dist p c = r), ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
⊢ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius

Tactic:
rcases h with ⟨c, r, h⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ p ∈ ps, dist p c = r
⊢ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius

Tactic:
⟨⟨c, r⟩, h⟩

Premises used: EuclideanGeometry.Sphere.mk, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ p ∈ ps, dist p c = r
⊢ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius

Tactic:
exact ⟨⟨c, r⟩, h⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
h : ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
refine_2 : ∀ (s : Sphere P) (h : ps ⊆ Metric.sphere s.center s.radius), Cospherical ps
⊢ Cospherical ps

Tactic:
rcases h with ⟨s, h⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps

Tactic:
⟨s.center, s.radius, h⟩

Premises used: EuclideanGeometry.Cospherical, EuclideanGeometry.Sphere.center, Exists.intro, EuclideanGeometry.Sphere.radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps

Tactic:
exact ⟨s.center, s.radius, h⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
⊢ Cospherical (Metric.sphere s.center s.radius)

Tactic:
cospherical_iff_exists_sphere.2 ⟨s, Set.Subset.rfl⟩

Premises used: Iff.mpr, Set.Subset.rfl, Exists.intro, EuclideanGeometry.cospherical_iff_exists_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
hc : Cospherical ps₂
rcases : ∀ (c : P) (r : ℝ) (hcr : ∀ p ∈ ps₂, dist p c = r), Cospherical ps₁
⊢ Cospherical ps₁

Tactic:
rcases hc with ⟨c, r, hcr⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
c : P
r : ℝ
hcr : ∀ p ∈ ps₂, dist p c = r
⊢ Cospherical ps₁

Tactic:
⟨c, r, fun p hp => hcr p (hs hp)⟩

Premises used: EuclideanGeometry.Cospherical, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
c : P
r : ℝ
hcr : ∀ p ∈ ps₂, dist p c = r
⊢ Cospherical ps₁

Tactic:
exact ⟨c, r, fun p hp => hcr p (hs hp)⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
inst_1 : Nonempty P
⊢ Cospherical.{u_2} (P := P) ∅

Tactic:
let ⟨p⟩ := ‹Nonempty P›
  ⟨p, 0, fun _ => False.elim⟩

Premises used: EuclideanGeometry.Cospherical, False.elim, _private.0.EuclideanGeometry.cospherical_empty.match_1, Exists.intro, EmptyCollection.emptyCollection, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
h : ∃ (radius : ℝ), ∀ (p_1 : P), Membership.mem (γ := Set P) {p} p_1 → dist p_1 p = radius
⊢ Cospherical (P := P) {p}

Tactic:
use p
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
P : Type u_2
inst : MetricSpace P
p : P
⊢ ∃ (radius : ℝ), ∀ (p_1 : P), Membership.mem (γ := Set P) {p} p_1 → dist p_1 p = radius

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
hps : Cospherical ps
rcases : ∀ (c : E) (r : ℝ) (hc : ∀ p ∈ ps, dist p c = r), Cospherical (f '' ps)
⊢ Cospherical (f '' ps)

Tactic:
rcases hps with ⟨c, r, hc⟩