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
a b p q : P
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
r : ℝ
hr : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
have rw : ∃ (k : ℝ), m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = k • (m -ᵥ a)
Tactic: rw [hr]
-- 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
a b p q : P
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
r : ℝ
hr : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
⊢ ∃ (k : ℝ), m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = k • (m -ᵥ a)
have h₁ : m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = (1 - r * 2) • (m -ᵥ a)
Tactic: use 1 - r * 2
-- 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
a b p q : P
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
r : ℝ
hr : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
⊢ m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = (1 - r * 2) • (m -ᵥ a)
have match_scalars : 1 - r * HAdd.hAdd (α := ℝ) 1 1 = (1 - r * 2) * 1
Tactic: match_scalars
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
⊢ dist a p * dist b p = dist c p * dist d p
have obtain : ∀ (q : P) (r : ℝ) (h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r),
  dist a p * dist b p = dist c p * dist d p
Tactic: obtain ⟨q, r, h'⟩ := (cospherical_def {a, b, c, d}).mp 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
⊢ dist a p * dist b p = dist c p * dist d p
have ha : dist a q = r
Tactic: obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp)
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
⊢ dist a p * dist b p = dist c p * dist d p
have hb : dist b q = r
Tactic: obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp)
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
⊢ dist a p * dist b p = dist c p * dist d p
have hc : dist c q = r
Tactic: obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp)
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = r
⊢ dist a p * dist b p = dist c p * dist d p
have hd : dist d q = r
Tactic: obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp)
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = r
hd : dist d q = r
⊢ dist a p * dist b p = dist c p * dist d p
have hc₁ : dist c q = dist d q
Tactic: rw [← hd] at hc
Cleared hypotheses: hc, hd
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ dist a p * dist b p = dist c p * dist d p
have ha₁ : dist a q = dist b q
Tactic: rw [← hb] at ha
Cleared hypotheses: ha, hb, hc, hd
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ dist a p * dist b p = dist c p * dist d p
have rw : |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
Tactic: rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
rw : |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
⊢ dist a p * dist b p = dist c p * dist d p
have rw₁ : |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
Tactic: rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
rw : |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
rw₁ : |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
⊢ dist a p * dist b p = dist c p * dist d p
have rw₂ : |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| =
  |HPow.hPow (β := ℕ) (dist d q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
Tactic: rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
-- 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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
rw : |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
rw₁ : |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
rw₂ :
  |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| =
    |HPow.hPow (β := ℕ) (dist d q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
⊢ dist a p * dist b p = dist c p * dist d p
have rw₃ : |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| = |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2|
Tactic: rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
-- 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}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
⊢ dist a p * dist b p = dist c p * dist d p
have hapb₁ : Sbtw ℝ a p b
Tactic: rw [EuclideanGeometry.angle_eq_pi_iff_sbtw] at hapb hcpd
Cleared hypotheses: hapb, hcpd
-- 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}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
hapb₁ : Sbtw ℝ a p b
⊢ dist a p * dist b p = dist c p * dist d p
have hcpd₁ : Sbtw ℝ c p d
Tactic: rw [EuclideanGeometry.angle_eq_pi_iff_sbtw] at hapb hcpd
Cleared hypotheses: hapb, hcpd
-- 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₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}
have suffices : Cospherical (P := P) {p₁, p₂, p₄, p₃}
Tactic: suffices h_equiv : Cospherical ({p₁, p₂, p₄, p₃} : Set P) by grind [Set.pair_comm p₄ p₃]
-- 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₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}
have h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
Tactic: have h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂ := by
    grind [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hp₃p₄]
-- 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₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}
have hp₁p₃ : Sbtw ℝ p₁ p p₂
Tactic: rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄
Cleared hypotheses: hp₁p₂, hp₃p₄, hn, 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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hp₁p₃ : Sbtw ℝ p₁ p p₂
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}
have hp₃p₅ : Sbtw ℝ p₃ p p₄
Tactic: rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄
Cleared hypotheses: hp₁p₂, hp₃p₄, hn, 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
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₂}
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}
have hcol_p₃pp₄ : Collinear ℝ (P := P) {p₃, p, p₄}
Tactic: have hcol_p₃pp₄ := hp₃p₄.wbtw.collinear
-- 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₄}
⊢ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
have this : AffineIndependent ℝ ![p₁, p, p₃]
Tactic: have : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
-- 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₄}
this : AffineIndependent ℝ ![p₁, p, p₃]
⊢ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw : AffineIndependent ℝ ![p₁, p₂, p₃]
Tactic: rw [← affineIndependent_iff_not_collinear_set]
-- 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₄}
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}
have h_notcol_p₁p₂p₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: have h_notcol_p₁p₂p₃ : ¬ Collinear ℝ ({p₁, p₂, p₃} : Set P) := by
    have : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
    rw [← affineIndependent_iff_not_collinear_set]
    grind [hp₁p₂.left_ne_right, affineIndependent_of_affineIndependent_collinear_ne,
      AffineIndependent.comm_left, AffineIndependent.comm_right]
-- 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₃}
⊢ Cospherical (P := P) {p₁, p₂, p₄, p₃}
have apply : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₄ p₃)
Tactic: apply cospherical_of_two_zsmul_oangle_eq_of_not_collinear ?_ h_notcol_p₁p₂p₃
-- 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₃}
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₄ p₃)
have suffices : ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃
Tactic: suffices ∡ p₁ p₂ p₃ = ∡ p₁ p₄ 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₃}
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃
have suffices : ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃
Tactic: suffices ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃ by
    grind [oangle_eq_of_angle_eq_of_sign_eq, Sbtw.oangle_sign_eq_of_sbtw]
-- 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₃}
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃
have rw : ∠ p₃ p₂ p = ∠ p₁ p₄ p
Tactic: rw [angle_comm, ← angle_eq_angle_of_angle_eq_pi p₃ hp₁p₂.angle₃₂₁_eq_pi,
    ← angle_eq_angle_of_angle_eq_pi p₁ hp₃p₄.angle₃₂₁_eq_pi]
-- 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₃}
⊢ ∠ p₃ p₂ p = ∠ p₁ p₄ p
have suffices : Similar ![p₁, p, p₄] ![p₃, p, p₂]
Tactic: suffices h_sim : Similar ![p₁, p, p₄] ![p₃, p, p₂] by
    grind [angle_comm, h_sim.angle_eq_all.right.left]
-- 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₃}
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₃}
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₃}
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