awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have hbp : dist b p ≠ 0
Tactic: have hbp := left_dist_ne_zero_of_angle_eq_pi hbpd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist c d = dist c p / dist b p * dist a b
have h₁ : ∠ c p d = ∠ b p a
Tactic: rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : ∠ c p d = ∠ b p a
⊢ dist c d = dist c p / dist b p * dist a b
have hab : dist c p = dist c p / dist b p * dist b p
Tactic: rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : ∠ c p d = ∠ b p a
hab : dist c p = dist c p / dist b p * dist b p
⊢ dist c d = dist c p / dist b p * dist a b
have hcb : dist d p = dist c p / dist b p * dist a p
Tactic: rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ ∠ c p d = ∠ b p a
have h₁ : ∠ c p d = ∠ d p c
Tactic: rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : ∠ c p d = ∠ d p c
⊢ ∠ c p d = ∠ b p a
have h₂ : ∠ d p c = ∠ d p c
Tactic: rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have h₁ : dist c d = dist c p / dist b p * dist a b
Tactic: have h₁ : dist c d = dist c p / dist b p * dist a b := by
    rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]
    · rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm]
    all_goals simp [field, mul_comm, hmul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist d a = dist a p / dist b p * dist b c
have h₂ : ∠ d p a = ∠ c p b
Tactic: rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : ∠ d p a = ∠ c p b
⊢ dist d a = dist a p / dist b p * dist b c
have hab : dist d p = dist a p / dist b p * dist c p
Tactic: rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : ∠ d p a = ∠ c p b
hab : dist d p = dist a p / dist b p * dist c p
⊢ dist d a = dist a p / dist b p * dist b c
have hcb : dist a p = dist a p / dist b p * dist b p
Tactic: rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ ∠ d p a = ∠ c p b
have h₂ : ∠ d p b = π
Tactic: rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have h₂ : dist d a = dist a p / dist b p * dist b c
Tactic: have h₂ : dist d a = dist a p / dist b p * dist b c := by
    rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]
    · rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]; rwa [angle_comm]
    all_goals simp [field, mul_comm, hmul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have h₃ : dist d p = dist a p * dist c p / dist b p
Tactic: have h₃ : dist d p = dist a p * dist c p / dist b p := by simp [field, hmul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
x y : ℝ
⊢ x * (y * x) = x * x * y
have rw : y * (x * x) = x * x * y
Tactic: rw [mul_left_comm, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
x y : ℝ
rw : y * (x * x) = x * x * y
⊢ x * (y * x) = x * x * y
have rw₁ : x * x * y = x * x * y
Tactic: rw [mul_left_comm, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have h₄ : ∀ (x y : ℝ), x * (y * x) = x * x * y
Tactic: have h₄ : ∀ x y : ℝ, x * (y * x) = x * x * y := fun x y => by rw [mul_left_comm, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ dist (s.secondInter p v) s.center = dist p s.center
have rw : dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
Tactic: rw [Sphere.secondInter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
have pos : ∀ (hv : v = 0), dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
pos : ∀ (hv : v = 0), dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
⊢ dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
have neg : ∀ (hv : ¬v = 0), dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
have neg : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫
Tactic: rw [dist_smul_vadd_eq_dist _ _ hv]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫ = 0
have refine_1 : ∀ (hp : s.secondInter p v = p), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: refine ⟨fun hp => ?_, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
refine_1 : ∀ (hp : s.secondInter p v = p), ⟪v, p -ᵥ s.center⟫ = 0
⊢ s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫ = 0
have refine_2 : ∀ (hp : ⟪v, p -ᵥ s.center⟫ = 0), s.secondInter p v = p
Tactic: refine ⟨fun hp => ?_, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have pos : ∀ (hv : v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
pos : ∀ (hv : v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg : ∀ (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₄ : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₄ : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₅ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₄ : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₅ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₆ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₄ : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₅ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₆ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₇ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₄ : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₅ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₆ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₇ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₈ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
Tactic: rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
Cleared hypotheses: hp, hv