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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
⊢ Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) = HAdd.hAdd (α := ℕ) 2 1

Tactic:
simp
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
⊢ Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)

Tactic:
have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by
    rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
    simp⟩
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
have :
  ∀ (this : Oriented ℝ (↥S.direction) (Fin 2)),
    dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 =
      Simplex.circumradius t
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t

Tactic:
have : Module.Oriented ℝ S.direction (Fin 2) :=
    ⟨Basis.orientation (finBasisOfFinrankEq _ _ hf2.out)⟩
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2)
⊢ dist (t'.points i₁) (t'.points i₃) / |(∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)).sin| / 2 =
    Simplex.circumradius.{u_1, u_2} (P := ↥S) (n := 2) t'

Tactic:
t'.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃

Premises used: Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2)
h : Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = |(∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)).sin|
h₁ : Simplex.circumradius t = Simplex.circumradius.{u_1, u_2} (P := ↥S) (n := 2) t'
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t

Tactic:
convert! t'.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃ using 3

Premises used: Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2)
h : Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = Real.sin (∠ (t'.points i₁) (t'.points i₂) (t'.points i₃))
⊢ Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = |(∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)).sin|

Tactic:
rw [← Real.Angle.sin_toReal,
      Real.abs_sin_eq_sin_abs_of_abs_le_pi (Real.Angle.abs_toReal_le_pi _),
      ← angle_eq_abs_oangle_toReal (t'.independent.injective.ne h₁₂)
        (t'.independent.injective.ne h₂₃.symm)]

Premises used: Real.abs_sin_eq_sin_abs_of_abs_le_pi, Real.Angle.abs_toReal_le_pi, Function.Injective.ne, AffineIndependent.injective, Ne.symm, EuclideanGeometry.angle_eq_abs_oangle_toReal, Affine.Simplex.independent, Real.Angle.sin_toReal
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2)
⊢ Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = Real.sin (∠ (t'.points i₁) (t'.points i₂) (t'.points i₃))

Tactic:
congr
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2)
⊢ Simplex.circumradius t = Simplex.circumradius.{u_1, u_2} (P := ↥S) (n := 2) t'

Tactic:
simp [t']
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
rw :
  dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) =
    2 * (dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2)
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = 2 * Simplex.circumradius t

Tactic:
rw [← t.dist_div_sin_angle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃]

Premises used: Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) =
    2 * (dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2)

Tactic:
ring
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn rwa rwa₁ rwa₂ rwa₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
⊢ ¬Collinear ℝ (P := P) {p₁, p₃, p₄}

Tactic:
rwa [← collinear_iff_of_two_zsmul_oangle_eq h]

Premises used: EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
⊢ ¬Collinear ℝ (P := P) {p₁, p₃, p₄}

Tactic:
have hn' : ¬Collinear ℝ ({p₁, p₃, p₄} : Set P) := by
    rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
rw : ∃ (s : Sphere P), {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}

Tactic:
rw [cospherical_iff_exists_sphere]

Premises used: EuclideanGeometry.cospherical_iff_exists_sphere
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ ∃ (s : Sphere P), {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius

Tactic:
⟨t₂.circumsphere, ?_⟩

Premises used: Affine.Simplex.circumsphere, Exists.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
refine :
  {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
⊢ ∃ (s : Sphere P), {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius

Tactic:
refine ⟨t₂.circumsphere, ?_⟩
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
simp_rw :
  p₁ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
    p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
      p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
        p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
⊢ {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius

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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ p₁ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
    p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
      p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
        p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius

Tactic:
⟨t₂.mem_circumsphere 0, ?_, t₂.mem_circumsphere 1, t₂.mem_circumsphere 2⟩

Premises used: Affine.Simplex.mem_circumsphere, And.intro, OfNat.ofNat
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
refine : p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
⊢ p₁ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
    p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
      p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧
        p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius

Tactic:
refine ⟨t₂.mem_circumsphere 0, ?_, t₂.mem_circumsphere 1, t₂.mem_circumsphere 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ Ne (α := Fin 3) 0 1

Tactic:
decide
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ Ne (α := Fin 3) 0 2

Tactic:
decide
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ Ne (α := Fin 3) 1 2

Tactic:
decide
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
rw : p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₁).center (Affine.Simplex.circumsphere t₁).radius
⊢ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius

Tactic:
rw [Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq
    (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide)
    (show t₂.points 0 = t₁.points 0 from rfl) rfl h.symm]

Premises used: Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq, Eq.symm, rfl
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₁).center (Affine.Simplex.circumsphere t₁).radius

Tactic:
t₁.mem_circumsphere 1

Premises used: Eq.mpr, Affine.Simplex.mem_circumsphere, Set.Mem, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, OfNat.ofNat, Matrix.vecCons
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
hn' : ¬Collinear ℝ (P := P) {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₁).center (Affine.Simplex.circumsphere t₁).radius

Tactic:
exact t₁.mem_circumsphere 1

Premises used: Affine.Simplex.mem_circumsphere, OfNat.ofNat
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hn : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄}

Tactic:
⟨cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hn, coplanar_of_fact_finrank_eq_two _⟩

Premises used: coplanar_of_fact_finrank_eq_two, EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear, EuclideanGeometry.Concyclic.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
pos :
  ∀ (hc : Collinear ℝ (P := P) {p₁, p₂, p₄}),
    Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
neg :
  ∀ (hc : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}),
    Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
by_cases hc : Collinear ℝ ({p₁, p₂, p₄} : Set P)

Premises used: Real, Collinear, Insert.insert, Singleton.singleton
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
pos : ∀ (he : p₁ = p₄), Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
neg : ∀ (he : ¬p₁ = p₄), Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
by_cases he : 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
pos : Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
rw [he, Set.insert_eq_self.2
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))]

Premises used: Iff.mpr, Set.mem_singleton, Set.mem_insert_of_mem, Set.insert_eq_self
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
pos : ∀ (hl : Collinear ℝ (P := P) {p₂, p₃, p₄}), Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
neg : ∀ (hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}), Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}

Tactic:
by_cases hl : Collinear ℝ ({p₂, p₃, p₄} : Set P)

Premises used: Real, Collinear, Insert.insert, Singleton.singleton
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : Collinear ℝ (P := P) {p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}

Tactic:
Or.inr hl

Premises used: Or.inr
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : Collinear ℝ (P := P) {p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}

Tactic:
exact Or.inr hl

Premises used: Or.inr