awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
h : |(∡ p₁ p₂ p₃).sin| = (∡ p₃ p₁ s.center).cos
⊢ dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| / 2 = s.radius

Tactic:
convert! dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₃ hp₁p₃

Premises used: EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
rw : |(∡ p₃ p₁ s.center).toReal| ≤ π / 2
⊢ |(∡ p₁ p₂ p₃).sin| = (∡ p₃ p₁ s.center).cos

Tactic:
rw [← Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi
    (two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃),
    abs_of_nonneg (Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two.2 _)]

Premises used: Iff.mpr, Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi, Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two, Ne.symm, EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, abs_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₃ p₁ s.center).toReal| ≤ π / 2

Tactic:
(abs_oangle_center_right_toReal_lt_pi_div_two hp₁ hp₃).le

Premises used: LT.lt.le, EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₃ p₁ s.center).toReal| ≤ π / 2

Tactic:
exact (abs_oangle_center_right_toReal_lt_pi_div_two hp₁ hp₃).le

Premises used: LT.lt.le, EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
rw : dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * (dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| / 2)
rw₁ rw₂ : dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin|
⊢ dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * s.radius

Tactic:
rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃,
    mul_div_cancel₀ _ (two_ne_zero' ℝ)]

Premises used: Real, EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius, mul_div_cancel₀, two_ne_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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ HSMul.hSMul (β := V) ((∡ (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t.points i₃ -ᵥ t.points i₁) : V) +ᵥ
      midpoint ℝ (t.points i₁) (t.points i₃) =
    Simplex.circumcenter t

Tactic:
Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center (t.mem_circumsphere _)
    (t.mem_circumsphere _) (t.mem_circumsphere _) (t.independent.injective.ne h₁₂)
    (t.independent.injective.ne h₁₃) (t.independent.injective.ne h₂₃)

Premises used: Affine.Simplex.mem_circumsphere, Function.Injective.ne, Affine.Simplex.circumcenter, AffineIndependent.injective, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, Affine.Simplex.independent
-- 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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ dist (t.points i₁) (t.points i₃) / |(∡ (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 = Simplex.circumradius t

Tactic:
Sphere.dist_div_sin_oangle_div_two_eq_radius (t.mem_circumsphere _) (t.mem_circumsphere _)
    (t.mem_circumsphere _) (t.independent.injective.ne h₁₂) (t.independent.injective.ne h₁₃)
    (t.independent.injective.ne h₂₃)

Premises used: Affine.Simplex.mem_circumsphere, EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius, Function.Injective.ne, AffineIndependent.injective, Affine.Simplex.independent, Affine.Simplex.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ dist (t.points i₁) (t.points i₃) / |(∡ (t.points i₁) (t.points i₂) (t.points i₃)).sin| = 2 * Simplex.circumradius t

Tactic:
Sphere.dist_div_sin_oangle_eq_two_mul_radius (t.mem_circumsphere _) (t.mem_circumsphere _)
    (t.mem_circumsphere _) (t.independent.injective.ne h₁₂) (t.independent.injective.ne h₁₃)
    (t.independent.injective.ne h₂₃)

Premises used: Affine.Simplex.mem_circumsphere, Function.Injective.ne, EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius, AffineIndependent.injective, Affine.Simplex.independent, Affine.Simplex.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.circumsphere t =
    {
      center :=
        HSMul.hSMul (β := V) ((∡ (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2)
            ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t.points i₃ -ᵥ t.points i₁) : V) +ᵥ
          midpoint ℝ (t.points i₁) (t.points i₃),
      radius := dist (t.points i₁) (t.points i₃) / |(∡ (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 }

Tactic:
t.circumsphere.ext
    (t.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter h₁₂ h₁₃ h₂₃).symm
    (t.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃).symm

Premises used: EuclideanGeometry.Sphere.ext, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, Eq.symm, 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
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
⊢ t'p i₁ = t.points i₁

Tactic:
simp [t'p, 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)
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
⊢ t'p i₁ = t.points i₁

Tactic:
have h₁ : t'p i₁ = t.points i₁ := by simp [t'p, 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)
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₁
⊢ t'p i₂ = p

Tactic:
simp [t'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)
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₁
⊢ t'p i₂ = p

Tactic:
have h₂ : t'p i₂ = p := by simp [t'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)
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
⊢ t'p i₃ = t.points i₃

Tactic:
simp [t'p, h₂₃.symm]

Premises used: 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
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
⊢ t'p i₃ = t.points i₃

Tactic:
have h₃ : t'p i₃ = t.points i₃ := by simp [t'p, h₂₃.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
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₃
rw : AffineIndependent ℝ t.points
⊢ AffineIndependent ℝ t'p

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₂₃]

Premises used: EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq, affineIndependent_iff_not_collinear_of_ne
-- 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)
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.points

Tactic:
t.independent

Premises used: Affine.Simplex.independent
-- 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)
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.points

Tactic:
exact t.independent

Premises used: Affine.Simplex.independent
-- 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)
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

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
-- 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)
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 }
⊢ t'.points i₁ = t.points i₁

Tactic:
have h₁' : t'.points i₁ = t.points i₁ := 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)
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₁
⊢ t'.points i₂ = p

Tactic:
have h₂' : t'.points i₂ = p := 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)
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
⊢ t'.points i₃ = t.points i₃

Tactic:
have h₃' : t'.points i₃ = t.points i₃ := 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)
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₃))
rwa₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (t'.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) (t.points i₂) (t.points i₃))
rwa₂ rwa₃ rwa₄ rwa₅ :
  HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₁) p (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₃))

Tactic:
rwa [h₁', h₂', 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)
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₃))

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₃']
-- 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)
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₃))
rw : t'.points i₂ ∈ Simplex.circumsphere t'
⊢ p ∈ Simplex.circumsphere t

Tactic:
rw [← circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ h₁' h₃' h', ←
    h₂']

Premises used: Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_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)
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₃))
⊢ t'.points i₂ ∈ Simplex.circumsphere t'

Tactic:
Simplex.mem_circumsphere _ _

Premises used: Affine.Simplex.mem_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)
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₃))
⊢ t'.points i₂ ∈ Simplex.circumsphere t'

Tactic:
exact Simplex.mem_circumsphere _ _

Premises used: Affine.Simplex.mem_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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ 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

Premises used: Affine.Simplex.points, Real, affineSpan, Set.range, AffineSubspace
-- 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 ⋯
rw : Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) = HAdd.hAdd (α := ℕ) 2 1
⊢ finrank.{0, u_1} ℝ ↥S.direction = 2

Tactic:
rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]

Premises used: direction_affineSpan, AffineIndependent.finrank_vectorSpan, Affine.Simplex.independent