awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ ¬Collinear ℝ (P := ↥S) {p₁', p', p₃'}
have rw : AffineIndependent ℝ (P := P) ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'])
Tactic: rw [← affineIndependent_iff_not_collinear_set,
      ← s_isom.toAffineMap.affineIndependent_iff s_isom.injective]
-- 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₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ AffineIndependent ℝ (P := P) ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'])
have h₁ : (⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃'] = ![p₁, p, p₃]
Tactic: convert! hindep
-- 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₄' = π
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₃'] = ![p₁, p, p₃]
have h₁ : ∀ (i : Fin (Nat.succ 0).succ.succ), ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i
Tactic: ext i
-- 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₄' = π
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
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i
have h₁ : ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩) =
  ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ))
Tactic: fin_cases i
Cleared hypotheses: i
-- 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₄' = π
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))
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i
have h₂ : ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩) =
  ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ))
Tactic: fin_cases i
Cleared hypotheses: i
-- 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₄' = π
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))
⊢ ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i
have h₃ : ((⇑s_isom.toAffineMap : (a : ↥S) → P) ∘ ![p₁', p', p₃']) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩) =
  ![p₁, p, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ))
Tactic: fin_cases i
Cleared hypotheses: i
-- 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₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ Cospherical (P := ↥S) {p₁', p₂', p₃', p₄'}
have hncol : ¬Collinear ℝ (P := ↥S) {p₁', p', p₃'}
Tactic: have hncol : ¬ Collinear ℝ {p₁', p', p₃'} := by
    rw [← affineIndependent_iff_not_collinear_set,
      ← s_isom.toAffineMap.affineIndependent_iff s_isom.injective]
    convert! hindep
    ext i; fin_cases i <;> rfl
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
⊢ dist a p * dist b p = dist c p * dist d p
have hapb₁ : Collinear ℝ (P := P) {a, p, b}
Tactic: apply collinear_of_angle_eq_zero at hapb
Cleared hypotheses: hapb
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hcpd : ∠ c p d = 0
hapb : Collinear ℝ (P := P) {a, p, b}
⊢ dist a p * dist b p = dist c p * dist d p
have hcpd₁ : Collinear ℝ (P := P) {c, p, d}
Tactic: apply collinear_of_angle_eq_zero at hcpd
Cleared hypotheses: hcpd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.power p = 0 ↔ p ∈ s
have rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ p ∈ s
Tactic: rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ p ∈ s
⊢ s.power p = 0 ↔ p ∈ s
have rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ dist p s.center = s.radius
Tactic: rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ p ∈ s
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ dist p s.center = s.radius
⊢ s.power p = 0 ↔ p ∈ s
have rw₂ : HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center = s.radius
Tactic: rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ p ∈ s
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ dist p s.center = s.radius
rw₂ : HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center = s.radius
⊢ s.power p = 0 ↔ p ∈ s
have rw₃ : dist p s.center = s.radius ↔ dist p s.center = s.radius
Tactic: rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ 0 < s.power p ↔ s.radius < dist p s.center
have rw : 0 < HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius < dist p s.center
Tactic: rw [power, sub_pos, pow_lt_pow_iff_left₀ hr dist_nonneg two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : 0 < HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius < dist p s.center
⊢ 0 < s.power p ↔ s.radius < dist p s.center
have rw₁ : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist p s.center) 2 ↔ s.radius < dist p s.center
Tactic: rw [power, sub_pos, pow_lt_pow_iff_left₀ hr dist_nonneg two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : 0 < HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius < dist p s.center
rw₁ : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist p s.center) 2 ↔ s.radius < dist p s.center
⊢ 0 < s.power p ↔ s.radius < dist p s.center
have rw₂ : s.radius < dist p s.center ↔ s.radius < dist p s.center
Tactic: rw [power, sub_pos, pow_lt_pow_iff_left₀ hr dist_nonneg two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.power p < 0 ↔ dist p s.center < s.radius
have rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 < 0 ↔ dist p s.center < s.radius
Tactic: rw [power, sub_neg, pow_lt_pow_iff_left₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 < 0 ↔ dist p s.center < s.radius
⊢ s.power p < 0 ↔ dist p s.center < s.radius
have rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 < HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center < s.radius
Tactic: rw [power, sub_neg, pow_lt_pow_iff_left₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 < 0 ↔ dist p s.center < s.radius
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 < HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center < s.radius
⊢ s.power p < 0 ↔ dist p s.center < s.radius
have rw₂ : dist p s.center < s.radius ↔ dist p s.center < s.radius
Tactic: rw [power, sub_neg, pow_lt_pow_iff_left₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ 0 ≤ s.power p ↔ s.radius ≤ dist p s.center
have rw : 0 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius ≤ dist p s.center
Tactic: rw [power, sub_nonneg, pow_le_pow_iff_left₀ hr dist_nonneg two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : 0 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius ≤ dist p s.center
⊢ 0 ≤ s.power p ↔ s.radius ≤ dist p s.center
have rw₁ : HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 ↔ s.radius ≤ dist p s.center
Tactic: rw [power, sub_nonneg, pow_le_pow_iff_left₀ hr dist_nonneg two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : 0 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius ≤ dist p s.center
rw₁ : HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 ↔ s.radius ≤ dist p s.center
⊢ 0 ≤ s.power p ↔ s.radius ≤ dist p s.center
have rw₂ : s.radius ≤ dist p s.center ↔ s.radius ≤ dist p s.center
Tactic: rw [power, sub_nonneg, pow_le_pow_iff_left₀ hr dist_nonneg two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.power p ≤ 0 ↔ dist p s.center ≤ s.radius
have rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ≤ 0 ↔ dist p s.center ≤ s.radius
Tactic: rw [power, sub_nonpos, pow_le_pow_iff_left₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ≤ 0 ↔ dist p s.center ≤ s.radius
⊢ s.power p ≤ 0 ↔ dist p s.center ≤ s.radius
have rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 ≤ HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center ≤ s.radius
Tactic: rw [power, sub_nonpos, pow_le_pow_iff_left₀ dist_nonneg hr two_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ≤ 0 ↔ dist p s.center ≤ s.radius
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 ≤ HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center ≤ s.radius
⊢ s.power p ≤ 0 ↔ dist p s.center ≤ s.radius
have rw₂ : dist p s.center ≤ s.radius ↔ dist p s.center ≤ s.radius
Tactic: rw [power, sub_nonpos, pow_le_pow_iff_left₀ dist_nonneg hr two_ne_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
⊢ dist a s.center = dist b s.center
have rw : s.radius = dist b s.center
Tactic: rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
rw : s.radius = dist b s.center
⊢ dist a s.center = dist b s.center
have rw₁ : s.radius = s.radius
Tactic: rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
⊢ dist p a * dist p b = |s.power p|
have hq : dist a s.center = dist b s.center
Tactic: have hq : dist a s.center = dist b s.center := by
    rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hq : dist a s.center = dist b s.center
⊢ dist p a * dist p b = |s.power p|
have rw : dist a p * dist p b = |s.power p|
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
    mem_sphere.mp hb, power, abs_sub_comm]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = |s.power p|
⊢ dist p a * dist p b = |s.power p|
have rw₁ : dist a p * dist b p = |s.power p|
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
    mem_sphere.mp hb, power, abs_sub_comm]