awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₃}
⊢ Similar ![p₁, p, p₄] ![p₃, p, p₂]
have h_notcol_p₁pp₄ : ¬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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₂}
⊢ False
have suffices : Collinear ℝ (P := P) {p₁, p, p₃}
Tactic: suffices hcol : Collinear ℝ ({p₁, p, p₃} : Set P) by grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₂}
⊢ Collinear ℝ (P := P) {p₁, p, p₃}
have suffices : Collinear ℝ (P := P) {p₃, p₁, p, p₂}
Tactic: suffices hcol : Collinear ℝ ({p₃, p₁, p, p₂} : Set P) by grind [Collinear.subset _ hcol]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₂}
⊢ Collinear ℝ (P := P) {p₃, p₁, p, p₂}
have hne_pp₂ : p ≠ p₂
Tactic: have hne_pp₂ := hp₁p₂.ne_right
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₄}
⊢ Similar ![p₁, p, p₄] ![p₃, p, p₂]
have h_notcol_p₃pp₂ : ¬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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₂}
⊢ Similar ![p₁, p, p₄] ![p₃, p, p₂]
have apply : dist p₁ p * dist p p₂ = dist p p₄ * dist p₃ p
Tactic: apply similar_of_side_angle_side h_notcol_p₁pp₄ h_notcol_p₃pp₂ h_angle_eq ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₃}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
Tactic: have hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂ := angle_eq_pi_iff_sbtw.mp hp₁p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₂
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
Tactic: have hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄ := angle_eq_pi_iff_sbtw.mp hp₃p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₄
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hindep : AffineIndependent ℝ ![p₁, p, p₃]
Tactic: have hindep : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₃]
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have ht : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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 }
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hS : let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points);
S = affineSpan ℝ (Set.range t.points)
Tactic: set S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) with hS
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₁, p} ⊆ Set.range t.points
have simp : Subset (α := Set P) {p₁, p} {p₃, p, p₁}
Tactic: simp [ht]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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
have suffices : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p}) p₂
Tactic: suffices hmem : p₂ ∈ affineSpan ℝ {p₁, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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)
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hp₂ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₃, p} ⊆ Set.range t.points
have simp : Subset (α := Set P) {p₃, p} {p₃, p, p₁}
Tactic: simp [ht]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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
have suffices : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₃, p}) p₄
Tactic: suffices hmem : p₄ ∈ affineSpan ℝ {p₃, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hp₄ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₄
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have h_dist' : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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'
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hp₁'p₂' : ∠ p₁' p' p₂' = π
Tactic: have hp₁'p₂' : ∠ p₁' p' p₂' = π := by simpa [AffineIsometry.angle_map s_isom]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₂' = π
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have hp₃'p₄' : ∠ p₃' p' p₄' = π
Tactic: have hp₃'p₄' : ∠ p₃' p' p₄' = π := by simpa [AffineIsometry.angle_map s_isom]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₄' = π
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have suffices : Cospherical (P := ↥S) {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'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
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₄' = π
⊢ finrank.{0, u_1} ℝ ↥S.direction = 2
have rw : Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) = HAdd.hAdd (α := ℕ) 2 1
Tactic: rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
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₄' = π
⊢ Cospherical (P := ↥S) {p₁', p₂', p₃', p₄'}
have hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
Tactic: have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by
    rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
    simp⟩