awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg₈ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₉ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 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
neg₈ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₉ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₁₀ : ∀ (hp : Eq (α := ℝ) (-2) 0 ∨ ⟪v, p -ᵥ s.center⟫ = 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
neg₈ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₉ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁₀ : ∀ (hp : Eq (α := ℝ) (-2) 0 ∨ ⟪v, p -ᵥ s.center⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0
have neg₁₁ : ∀ (hp : ⟪v, p -ᵥ s.center⟫ = 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 : ⟪v, p -ᵥ s.center⟫ = 0
⊢ s.secondInter p v = p
have refine_2 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
Tactic: rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
-- 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 : ⟪v, p -ᵥ s.center⟫ = 0
refine_2 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
⊢ s.secondInter p v = p
have refine_2₁ : (HMul.hMul (α := ℝ) (-2) 0 / ⟪v, v⟫) • v +ᵥ p = p
Tactic: rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
-- 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 : ⟪v, p -ᵥ s.center⟫ = 0
refine_2 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
refine_2₁ : (HMul.hMul (α := ℝ) (-2) 0 / ⟪v, v⟫) • v +ᵥ p = p
⊢ s.secondInter p v = p
have refine_2₂ : (0 / ⟪v, v⟫) • v +ᵥ p = p
Tactic: rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
-- 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 : ⟪v, p -ᵥ s.center⟫ = 0
refine_2 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
refine_2₁ : (HMul.hMul (α := ℝ) (-2) 0 / ⟪v, v⟫) • v +ᵥ p = p
refine_2₂ : (0 / ⟪v, v⟫) • v +ᵥ p = p
⊢ s.secondInter p v = p
have refine_2₃ : HSMul.hSMul (α := ℝ) 0 v +ᵥ p = p
Tactic: rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
-- 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 : ⟪v, p -ᵥ s.center⟫ = 0
refine_2 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
refine_2₁ : (HMul.hMul (α := ℝ) (-2) 0 / ⟪v, v⟫) • v +ᵥ p = p
refine_2₂ : (0 / ⟪v, v⟫) • v +ᵥ p = p
refine_2₃ : HSMul.hSMul (α := ℝ) 0 v +ᵥ p = p
⊢ s.secondInter p v = p
have refine_2₄ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) 0 p = p
Tactic: rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
-- 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 : ⟪v, p -ᵥ s.center⟫ = 0
refine_2 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
refine_2₁ : (HMul.hMul (α := ℝ) (-2) 0 / ⟪v, v⟫) • v +ᵥ p = p
refine_2₂ : (0 / ⟪v, v⟫) • v +ᵥ p = p
refine_2₃ : HSMul.hSMul (α := ℝ) 0 v +ᵥ p = p
refine_2₄ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) 0 p = p
⊢ s.secondInter p v = p
have refine_2₅ : p = p
Tactic: rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
-- 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
hp : p ∈ s
v : V
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) p'
⊢ p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s
have refine_1 : ∀ (h : p' = p ∨ p' = s.secondInter p v), p' ∈ s
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- 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
hp : p ∈ s
v : V
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) p'
refine_1 : ∀ (h : p' = p ∨ p' = s.secondInter p v), p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s
have refine_2 : ∀ (h : p' ∈ s), p' = p ∨ p' = s.secondInter p v
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- 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
hp : p ∈ s
v : V
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) p'
h : p' = p ∨ p' = s.secondInter p v
⊢ p' ∈ s
have refine_1 : ∀ (h : p' = p), p' ∈ s
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- 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
hp : p ∈ s
v : V
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) p'
h : p' = p ∨ p' = s.secondInter p v
refine_1 : ∀ (h : p' = p), p' ∈ s
⊢ p' ∈ s
have refine_1₁ : ∀ (h : p' = s.secondInter p v), p' ∈ s
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- 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
hp : p ∈ s
v : V
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) p'
h : p' = s.secondInter p v
⊢ p' ∈ s
have refine_1 : s.secondInter p v ∈ s
Tactic: rwa [h, Sphere.secondInter_mem]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (hypothesis)
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
hp : p ∈ s
v : V
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) p'
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v
have hp'₁ : ∃ (a : ℝ), a • v = p' -ᵥ p
Tactic: rw [AffineSubspace.mem_mk', Submodule.mem_span_singleton] at hp'
Cleared hypotheses: hp', h
-- 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
hp : p ∈ s
v : V
p' : P
hp' : ∃ (a : ℝ), a • v = p' -ᵥ p
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v
have refine_2 : ∀ (r : ℝ) (hr : r • v = p' -ᵥ p), p' = p ∨ p' = s.secondInter p v
Tactic: rcases hp' with ⟨r, hr⟩
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (hypothesis)
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
hp : p ∈ s
v : V
p' : P
h : p' ∈ s
r : ℝ
hr : r • v = p' -ᵥ p
⊢ p' = p ∨ p' = s.secondInter p v
have hr₁ : p' = r • v +ᵥ p
Tactic: rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr
Cleared hypotheses: hr
-- 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
hp : p ∈ s
v : V
p' : P
h : p' ∈ s
r : ℝ
hr : p' = r • v +ᵥ p
⊢ p' = p ∨ p' = s.secondInter p v
have refine_2 : ∀ (h : r • v +ᵥ p ∈ s), r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
Tactic: subst hr
Cleared hypotheses: p', h, hr
-- 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
hp : p ∈ s
v : V
r : ℝ
h : r • v +ᵥ p ∈ s
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
have pos : ∀ (hv : v = 0), r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
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
hp : p ∈ s
v : V
r : ℝ
h : r • v +ᵥ p ∈ s
pos : ∀ (hv : v = 0), r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
have neg : ∀ (hv : ¬v = 0), r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
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
hp : p ∈ s
v : V
r : ℝ
h : r • v +ᵥ p ∈ s
hv : ¬v = 0
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
have neg : r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
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
hp : p ∈ s
v : V
r : ℝ
h : r • v +ᵥ p ∈ s
hv : ¬v = 0
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have neg : ∀ (hp : dist p s.center = s.radius) {v : V} (r : ℝ) (h : dist (r • v +ᵥ p) s.center = s.radius) (hv : ¬v = 0),
  r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mem_sphere] at h hp
Cleared hypotheses: hp, v, r, h, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (hypothesis)
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
hp : dist p s.center = s.radius
v : V
r : ℝ
h : dist (r • v +ᵥ p) s.center = s.radius
hv : ¬v = 0
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have h₁ : r = 0 ∨ r = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫
Tactic: rw [← hp, dist_smul_vadd_eq_dist _ _ hv] at h
Cleared hypotheses: h, 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
hp : dist p s.center = s.radius
v : V
r : ℝ
h : r = 0 ∨ r = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫
hv : ¬v = 0
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have neg : ∀ (h : r = 0), r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- 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
hp : dist p s.center = s.radius
v : V
r : ℝ
h : r = 0 ∨ r = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫
hv : ¬v = 0
neg : ∀ (h : r = 0), r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have neg₁ : ∀ (h : r = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫), r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- 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 q : P
hp : p ∈ s
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p'
⊢ p' = p ∨ p' = s.secondInter p (q -ᵥ p) ↔ p' ∈ s
have convert_3 : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) p'
Tactic: convert! s.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem 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 q : P
hp : p ∈ s
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p'
⊢ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) p'
have h : Eq (α := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) (affineSpan ℝ {p, q})
Tactic: convert! 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 q : P
hp : p ∈ s
p' : P
hp' : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p'
⊢ Eq (α := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) (affineSpan ℝ {p, q})
have h : Eq (α := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))))
  (AffineSubspace.direction (P := P) (affineSpan ℝ {p, q}))
Tactic: rw [AffineSubspace.eq_iff_direction_eq_of_mem (AffineSubspace.self_mem_mk' p _)
    (left_mem_affineSpan_pair _ _ _)]
-- 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
r : ℝ
hr : r ≠ 0
⊢ s.secondInter p (r • v) = s.secondInter p v
have simp_rw : (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: simp_rw [Sphere.secondInter, real_inner_smul_left, inner_smul_right, smul_smul,
    div_mul_eq_div_div]
-- 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
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫)) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, 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
r : ℝ
hr : r ≠ 0
rw : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫)) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw₁ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r) / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, 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
r : ℝ
hr : r ≠ 0
rw : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫)) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₁ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r) / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw₂ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, 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
r : ℝ
hr : r ≠ 0
rw : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫)) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₁ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r) / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₂ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw₃ : (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, 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
r : ℝ
hr : r ≠ 0
rw : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫)) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₁ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r) / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₂ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₃ : (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw₄ : (r * ⟪v, p -ᵥ s.center⟫ * -2 / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, 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
r : ℝ
hr : r ≠ 0
rw : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫)) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₁ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r) / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₂ : (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₃ : (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₄ : (r * ⟪v, p -ᵥ s.center⟫ * -2 / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw₅ : (r * (⟪v, p -ᵥ s.center⟫ * -2) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Tactic: rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, mul_comm]