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₂ : 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₂}
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₃}
h_notcol_p₁pp₄ : ¬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₄}
h_notcol_p₃pp₂ : ¬Collinear ℝ (P := P) {p₃, p, p₂}
apply : dist p₁ p * dist p p₂ = dist p p₄ * dist p₃ p
⊢ Similar ![p₁, p, p₄] ![p₃, p, p₂]

Tactic:
apply similar_of_side_angle_side h_notcol_p₁pp₄ h_notcol_p₃pp₂ h_angle_eq ?_

Premises used: EuclideanGeometry.similar_of_side_angle_side
-- 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₄}
h_notcol_p₃pp₂ : ¬Collinear ℝ (P := P) {p₃, p, p₂}
⊢ dist p₁ p * dist p p₂ = dist p p₄ * dist p₃ p

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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
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₃}
⊢ Sbtw ℝ p₁ p p₂

Tactic:
have hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂ := angle_eq_pi_iff_sbtw.mp 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
⊢ Sbtw ℝ p₃ p p₄

Tactic:
have hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄ := angle_eq_pi_iff_sbtw.mp 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
⊢ AffineIndependent ℝ ![p₁, p, p₃]

Tactic:
have hindep : 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
⊢ let t := { points := ![p₁, p, p₃], independent := hindep : Affine.Simplex ℝ P 2 };
  t = { points := ![p₁, p, p₃], independent := hindep }

Tactic:
set t : Affine.Triangle ℝ P := ⟨_, hindep⟩ with ht

Premises used: Real, Affine.Triangle
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
⊢ 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.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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hmem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p}) p₂
simp : Subset (α := Set P) {p₁, p} {p₃, p, p₁}
⊢ {p₁, p} ⊆ Set.range t.points

Tactic:
simp [ht]
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hmem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p}) p₂
⊢ Subset (α := Set P) {p₁, p} {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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hmem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p}) p₂
⊢ p₂ ∈ S

Tactic:
exact affineSpan_mono ℝ (by simp [ht]; grind) hmem

Premises used: Real, affineSpan_mono
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
suffices : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p}) p₂
⊢ p₂ ∈ S

Tactic:
suffices hmem : p₂ ∈ affineSpan ℝ {p₁, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p}) p₂

Tactic:
simp [hp₁p₂_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₁p₂_sbtw.left_ne]

Premises used: Wbtw.collinear, Collinear.mem_affineSpan_of_mem_of_ne, Sbtw.wbtw, Sbtw.left_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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
⊢ p₂ ∈ S

Tactic:
have hp₂ : p₂ ∈ S := by
    suffices hmem : p₂ ∈ affineSpan ℝ {p₁, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
    simp [hp₁p₂_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₁p₂_sbtw.left_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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hmem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₃, p}) p₄
simp : Subset (α := Set P) {p₃, p} {p₃, p, p₁}
⊢ {p₃, p} ⊆ Set.range t.points

Tactic:
simp [ht]
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hmem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₃, p}) p₄
⊢ Subset (α := Set P) {p₃, p} {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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hmem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₃, p}) p₄
⊢ p₄ ∈ S

Tactic:
exact affineSpan_mono ℝ (by simp [ht]; grind) hmem

Premises used: Real, affineSpan_mono
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
suffices : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₃, p}) p₄
⊢ p₄ ∈ S

Tactic:
suffices hmem : p₄ ∈ affineSpan ℝ {p₃, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₃, p}) p₄

Tactic:
simp [hp₃p₄_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₃p₄_sbtw.left_ne]

Premises used: Wbtw.collinear, Collinear.mem_affineSpan_of_mem_of_ne, Sbtw.wbtw, Sbtw.left_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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
⊢ p₄ ∈ S

Tactic:
have hp₄ : p₄ ∈ S := by
    suffices hmem : p₄ ∈ affineSpan ℝ {p₃, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
    simp [hp₃p₄_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₃p₄_sbtw.left_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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
⊢ p₁ ∈ Set.range t.points

Tactic:
aesop
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
⊢ p ∈ Set.range t.points

Tactic:
aesop
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
⊢ p₃ ∈ Set.range t.points

Tactic:
aesop
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
p₃' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₃ ⋯
p₂' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₂ hp₂
p₄' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₄ hp₄
⊢ dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'

Tactic:
simpa [dist_eq_norm_vsub, ← s_isom.dist_map] using h

Premises used: dist_eq_norm_vsub, AffineIsometry.dist_map
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
p₃' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₃ ⋯
p₂' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₂ hp₂
p₄' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₄ hp₄
⊢ dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'

Tactic:
have h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p' := by
    simpa [dist_eq_norm_vsub, ← s_isom.dist_map] using h
-- 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
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₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
p₃' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₃ ⋯
p₂' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₂ hp₂
p₄' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₄ hp₄
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
⊢ ∠ p₁' p' p₂' = π

Tactic:
simpa [AffineIsometry.angle_map s_isom]

Premises used: AffineIsometry.angle_map