awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
suffices : Cospherical (P := P) {p₁, p₂, p₄, p₃}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}

Tactic:
suffices h_equiv : Cospherical ({p₁, p₂, p₄, p₃} : Set P) by grind [Set.pair_comm p₄ p₃]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
⊢ ∠ p₁ p p₄ = ∠ p₃ p p₂

Tactic:
grind [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hp₃p₄]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
⊢ ∠ p₁ p p₄ = ∠ p₃ p p₂

Tactic:
have h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂ := by
    grind [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hp₃p₄]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
⊢ Sbtw ℝ p₁ p p₂

Tactic:
rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hp₁p₃ : Sbtw ℝ p₁ p p₂
⊢ Sbtw ℝ p₃ p p₄

Tactic:
rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hp₁p₃ : Sbtw ℝ p₁ p p₂
hp₃p₅ : Sbtw ℝ p₃ p p₄
⊢ ¬Collinear ℝ (P := P) {p₁, p, p₃}

Tactic:
rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hp₁p₃ : Sbtw ℝ p₁ p p₂
hp₃p₅ : Sbtw ℝ p₃ p p₄
hn₁ : ¬Collinear ℝ (P := P) {p₁, p, p₃}
⊢ ∠ p₁ p p₄ = ∠ p₃ p p₂

Tactic:
rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
⊢ Collinear ℝ (P := P) {p₃, p, p₄}

Tactic:
have hcol_p₃pp₄ := hp₃p₄.wbtw.collinear
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
⊢ AffineIndependent ℝ ![p₁, p, p₃]

Tactic:
have : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
this : AffineIndependent ℝ ![p₁, p, p₃]
rw : AffineIndependent ℝ ![p₁, p₂, p₃]
⊢ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rw [← affineIndependent_iff_not_collinear_set]

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
this : AffineIndependent ℝ ![p₁, p, p₃]
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
grind [hp₁p₂.left_ne_right, affineIndependent_of_affineIndependent_collinear_ne,
      AffineIndependent.comm_left, AffineIndependent.comm_right]

Premises used: affineIndependent_of_affineIndependent_collinear_ne, AffineIndependent.comm_left, Sbtw.left_ne_right, AffineIndependent.comm_right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
⊢ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
have h_notcol_p₁p₂p₃ : ¬ Collinear ℝ ({p₁, p₂, p₃} : Set P) := by
    have : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
    rw [← affineIndependent_iff_not_collinear_set]
    grind [hp₁p₂.left_ne_right, affineIndependent_of_affineIndependent_collinear_ne,
      AffineIndependent.comm_left, AffineIndependent.comm_right]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
apply : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₄ p₃)
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}

Tactic:
apply cospherical_of_two_zsmul_oangle_eq_of_not_collinear ?_ h_notcol_p₁p₂p₃

Premises used: EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
this : ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₄ p₃)

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
suffices : ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₄ p₃)

Tactic:
suffices ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃ by grind
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
this : ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃

Tactic:
grind [oangle_eq_of_angle_eq_of_sign_eq, Sbtw.oangle_sign_eq_of_sbtw]

Premises used: Sbtw.oangle_sign_eq_of_sbtw, EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
suffices : ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃

Tactic:
suffices ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃ by
    grind [oangle_eq_of_angle_eq_of_sign_eq, Sbtw.oangle_sign_eq_of_sbtw]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
rw : ∠ p₃ p₂ p = ∠ p₁ p₄ p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃

Tactic:
rw [angle_comm, ← angle_eq_angle_of_angle_eq_pi p₃ hp₁p₂.angle₃₂₁_eq_pi,
    ← angle_eq_angle_of_angle_eq_pi p₁ hp₃p₄.angle₃₂₁_eq_pi]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_pi, Sbtw.angle₃₂₁_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
h_sim : Similar ![p₁, p, p₄] ![p₃, p, p₂]
⊢ ∠ p₃ p₂ p = ∠ p₁ p₄ p

Tactic:
grind [angle_comm, h_sim.angle_eq_all.right.left]

Premises used: EuclideanGeometry.angle_comm, And.right, And.left, Similar.angle_eq_all
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
suffices : Similar ![p₁, p, p₄] ![p₃, p, p₂]
⊢ ∠ p₃ p₂ p = ∠ p₁ p₄ p

Tactic:
suffices h_sim : Similar ![p₁, p, p₄] ![p₃, p, p₂] by
    grind [angle_comm, h_sim.angle_eq_all.right.left]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
hcol_1 : Collinear ℝ (P := P) {p₁, p, p₄}
hcol : Collinear ℝ (P := P) {p₁, p, p₃}
⊢ False

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
hcol : Collinear ℝ (P := P) {p₁, p, p₄}
suffices : Collinear ℝ (P := P) {p₁, p, p₃}
⊢ False

Tactic:
suffices hcol : Collinear ℝ ({p₁, p, p₃} : Set P) by grind
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
hcol_1 : Collinear ℝ (P := P) {p₁, p, p₄}
hcol : Collinear ℝ (P := P) {p₁, p₃, p, p₄}
⊢ Collinear ℝ (P := P) {p₁, p, p₃}

Tactic:
grind [Collinear.subset _ hcol]

Premises used: Collinear.subset
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
hcol : Collinear ℝ (P := P) {p₁, p, p₄}
suffices : Collinear ℝ (P := P) {p₁, p₃, p, p₄}
⊢ Collinear ℝ (P := P) {p₁, p, p₃}

Tactic:
suffices hcol : Collinear ℝ ({p₁, p₃, p, p₄} : Set P) by grind [Collinear.subset _ hcol]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
hcol : Collinear ℝ (P := P) {p₁, p, p₄}
⊢ p ≠ p₄

Tactic:
have hne_pp₄ := hp₃p₄.ne_right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
hcol : Collinear ℝ (P := P) {p₁, p, p₄}
hne_pp₄ : p ≠ p₄
⊢ Collinear ℝ (P := P) {p₁, p₃, p, p₄}

Tactic:
grind [collinear_insert_insert_of_mem_affineSpan_pair, Collinear.mem_affineSpan_of_mem_of_ne]

Premises used: Collinear.mem_affineSpan_of_mem_of_ne, collinear_insert_insert_of_mem_affineSpan_pair
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ ¬Collinear ℝ (P := P) {p₁, p, p₄}

Tactic:
have h_notcol_p₁pp₄ : ¬ Collinear ℝ ({p₁, p, p₄} : Set P) := by
    intro hcol
    suffices hcol : Collinear ℝ ({p₁, p, p₃} : Set P) by grind
    suffices hcol : Collinear ℝ ({p₁, p₃, p, p₄} : Set P) by grind [Collinear.subset _ hcol]
    have hne_pp₄ := hp₃p₄.ne_right
    grind [collinear_insert_insert_of_mem_affineSpan_pair, Collinear.mem_affineSpan_of_mem_of_ne]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ (P := P) {p₁, p, p₄}
hcol_1 : Collinear ℝ (P := P) {p₃, p, p₂}
hcol : Collinear ℝ (P := P) {p₁, p, p₃}
⊢ False

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ (P := P) {p₁, p, p₄}
hcol : Collinear ℝ (P := P) {p₃, p, p₂}
suffices : Collinear ℝ (P := P) {p₁, p, p₃}
⊢ False

Tactic:
suffices hcol : Collinear ℝ ({p₁, p, p₃} : Set P) by grind
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ (P := P) {p₁, p, p₄}
hcol_1 : Collinear ℝ (P := P) {p₃, p, p₂}
hcol : Collinear ℝ (P := P) {p₃, p₁, p, p₂}
⊢ Collinear ℝ (P := P) {p₁, p, p₃}

Tactic:
grind [Collinear.subset _ hcol]

Premises used: Collinear.subset
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ (P := P) {p₁, p, p₄}
hcol : Collinear ℝ (P := P) {p₃, p, p₂}
suffices : Collinear ℝ (P := P) {p₃, p₁, p, p₂}
⊢ Collinear ℝ (P := P) {p₁, p, p₃}

Tactic:
suffices hcol : Collinear ℝ ({p₃, p₁, p, p₂} : Set P) by grind [Collinear.subset _ hcol]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ (P := P) {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ (P := P) {p₁, p, p₄}
hcol : Collinear ℝ (P := P) {p₃, p, p₂}
⊢ p ≠ p₂

Tactic:
have hne_pp₂ := hp₁p₂.ne_right