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
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:
have hp₁'p₂' : ∠ p₁' p' p₂' = π := by simpa [AffineIsometry.angle_map s_isom]
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
⊢ ∠ p₃' p' p₄' = π

Tactic:
simpa [AffineIsometry.angle_map s_isom]

Premises used: AffineIsometry.angle_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₄
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
⊢ ∠ p₃' p' p₄' = π

Tactic:
have hp₃'p₄' : ∠ p₃' p' p₄' = π := by simpa [AffineIsometry.angle_map s_isom]
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
h_cospherical' : Cospherical (P := ↥S) {p₁', p₂', p₃', p₄'}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}

Tactic:
simpa [Set.image_insert_eq, Set.image_singleton] using Cospherical.subtype_val h_cospherical'

Premises used: Set.image_singleton, Set.image_insert_eq, EuclideanGeometry.Cospherical.subtype_val
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
suffices : Cospherical (P := ↥S) {p₁', p₂', p₃', p₄'}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}

Tactic:
suffices h_cospherical' : Cospherical {p₁', p₂', p₃', p₄'} by
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was:
    `grind [Set.image_insert_eq, Set.image_singleton]` -/
    simpa [Set.image_insert_eq, Set.image_singleton] using Cospherical.subtype_val h_cospherical'
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
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
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
⊢ Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) = HAdd.hAdd (α := ℕ) 2 1

Tactic:
simp
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
⊢ Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)

Tactic:
have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by
    rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
    simp⟩
-- Module: Mathlib.Geometry.Euclidean.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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
rw : AffineIndependent ℝ (P := P) ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'])
⊢ ¬Collinear ℝ (P := ↥S) {p₁', p', p₃'}

Tactic:
rw [← affineIndependent_iff_not_collinear_set,
      ← s_isom.toAffineMap.affineIndependent_iff s_isom.injective]

Premises used: affineIndependent_iff_not_collinear_set, AffineIsometry.toAffineMap, AffineIsometry.injective, AffineMap.affineIndependent_iff
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ AffineIndependent ℝ ![p₁, p, p₃]

Tactic:
hindep
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
h₁ : (⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'] = ![p₁, p, p₃]
⊢ AffineIndependent ℝ (P := P) ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'])

Tactic:
convert! hindep
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
h₁ : ∀ (i : Fin (Nat.succ 0).succ.succ), ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i
⊢ (⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'] = ![p₁, p, p₃]

Tactic:
ext i
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩) =
    ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))
h₂ :
  ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩) =
    ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ))
h₃ :
  ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩) =
    ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ))
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i

Tactic:
fin_cases i
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩) =
    ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))

Tactic:
rfl
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩) =
    ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ))

Tactic:
rfl
-- 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'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩) =
    ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ))

Tactic:
rfl