awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
⊢ p ∈ Simplex.circumsphere t
have h₁ : t'p i₁ = t.points i₁
Tactic: have h₁ : t'p i₁ = t.points i₁ := by simp [t'p, 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
⊢ p ∈ Simplex.circumsphere t
have h₂ : t'p i₂ = p
Tactic: have h₂ : t'p i₂ = p := by simp [t'p]
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
⊢ p ∈ Simplex.circumsphere t
have h₃ : t'p i₃ = t.points i₃
Tactic: have h₃ : t'p i₃ = t.points i₃ := by simp [t'p, h₂₃.symm]
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
⊢ AffineIndependent ℝ t'p
have rw : AffineIndependent ℝ t.points
Tactic: rw [affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃, h₁, h₂, h₃,
      collinear_iff_of_two_zsmul_oangle_eq h, ←
      affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
⊢ p ∈ Simplex.circumsphere t
have ha : AffineIndependent ℝ t'p
Tactic: have ha : AffineIndependent ℝ t'p := by
    rw [affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃, h₁, h₂, h₃,
      collinear_iff_of_two_zsmul_oangle_eq h, ←
      affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃]
    exact t.independent
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
⊢ p ∈ Simplex.circumsphere t
have h₁' : t'.points i₁ = t.points i₁
Tactic: have h₁' : t'.points i₁ = t.points i₁ := 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
⊢ p ∈ Simplex.circumsphere t
have h₂' : t'.points i₂ = p
Tactic: have h₂' : t'.points i₂ = p := 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
⊢ p ∈ Simplex.circumsphere t
have h₃' : t'.points i₃ = t.points i₃
Tactic: have h₃' : t'.points i₃ = t.points i₃ := h₃
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
h₃' : t'.points i₃ = t.points i₃
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
have rwa : HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t'.points i₂) (t'.points i₃)) =
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
Tactic: rwa [h₁', h₂', h₃']
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
h₃' : t'.points i₃ = t.points i₃
rwa :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t'.points i₂) (t'.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
have rwa₁ : HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t'.points i₃)) =
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
Tactic: rwa [h₁', h₂', 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
h₃' : t'.points i₃ = t.points i₃
⊢ p ∈ Simplex.circumsphere t
have h' : HSMul.hSMul (α := ℤ) 2 (∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)) =
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
Tactic: have h' : (2 : ℤ) • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) =
      (2 : ℤ) • ∡ (t.points i₁) (t.points i₂) (t.points i₃) := by rwa [h₁', h₂', h₃']
-- 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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
t'p : Fin 3 → P := Function.update (β := fun (a : Fin 3) ↦ P) t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
h₃' : t'.points i₃ = t.points i₃
h' :
  HSMul.hSMul (α := ℤ) 2 (∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
⊢ p ∈ Simplex.circumsphere t
have rw : t'.points i₂ ∈ Simplex.circumsphere t'
Tactic: rw [← circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ h₁' h₃' h', ←
    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
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 = Simplex.circumradius t
have hS : let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points);
S = affineSpan ℝ (Set.range t.points)
Tactic: set S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) with hS
-- 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
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 ⋯
⊢ finrank.{0, u_1} ℝ ↥S.direction = 2
have rw : Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) = HAdd.hAdd (α := ℕ) 2 1
Tactic: rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
-- 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
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 ⋯
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t
have hf2 : 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⟩
-- 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
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)
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t
have 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
Tactic: have : Module.Oriented ℝ S.direction (Fin 2) :=
    ⟨Basis.orientation (finBasisOfFinrankEq _ _ hf2.out)⟩
-- 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
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₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t
have h : Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = |(∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)).sin|
Tactic: convert! t'.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃ using 3
-- 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
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|
⊢ dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t
have h₁ : Simplex.circumradius t = Simplex.circumradius.{u_1, u_2} (P := ↥S) (n := 2) t'
Tactic: convert! t'.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃ using 3
-- 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
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₃)) = |(∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)).sin|
have h : Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = Real.sin (∠ (t'.points i₁) (t'.points i₂) (t'.points i₃))
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)]
-- 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
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 * Simplex.circumradius t
have 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)
Tactic: rw [← t.dist_div_sin_angle_div_two_eq_circumradius h₁₂ h₁₃ 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
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₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hn' : ¬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]
-- 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
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 := ⋯ }
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have rw : ∃ (s : Sphere P), {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
Tactic: rw [cospherical_iff_exists_sphere]
-- 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
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
have refine : {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
Tactic: refine ⟨t₂.circumsphere, ?_⟩
-- 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
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₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
have 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
Tactic: simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
-- 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
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
have refine : 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⟩
-- 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
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
have rw : 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]
-- 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
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₄)
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have pos : ∀ (hc : Collinear ℝ (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)