awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_2₅ refine_2₆ : p = p
⊢ s.secondInter p v = p

Tactic:
rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]

Premises used: zero_div, MulZeroClass.mul_zero, zero_vadd, zero_smul, EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_2 : ∀ (h : p' ∈ s), p' = p ∨ p' = s.secondInter p v
⊢ p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_1₁ : ∀ (h : p' = s.secondInter p v), p' ∈ s
⊢ p' ∈ s

Tactic:
rcases h with (h | h)
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_1 refine_1₁ refine_1₂ refine_1₃ : p ∈ s
⊢ p' ∈ s

Tactic:
rwa [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_1 : s.secondInter p v ∈ s
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : p ∈ s
⊢ p' ∈ s

Tactic:
rwa [h, Sphere.secondInter_mem]

Premises used: EuclideanGeometry.Sphere.secondInter_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
⊢ ∃ (a : ℝ), a • v = p' -ᵥ p

Tactic:
rw [AffineSubspace.mem_mk', Submodule.mem_span_singleton] at hp'

Premises used: Submodule.mem_span_singleton, AffineSubspace.mem_mk'
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hp'₁ : ∃ (a : ℝ), a • v = p' -ᵥ p
⊢ p' ∈ s

Tactic:
rw [AffineSubspace.mem_mk', Submodule.mem_span_singleton] at hp'

Premises used: Submodule.mem_span_singleton, AffineSubspace.mem_mk'
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_2 : ∀ (r : ℝ) (hr : r • v = p' -ᵥ p), p' = p ∨ p' = s.secondInter p v
⊢ p' = p ∨ p' = s.secondInter p v

Tactic:
rcases hp' with ⟨r, hr⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' = r • v +ᵥ p

Tactic:
rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr

Premises used: eq_comm, eq_vadd_iff_vsub_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
refine_2 : ∀ (h : r • v +ᵥ p ∈ s), r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v
⊢ p' = p ∨ p' = s.secondInter p v

Tactic:
subst hr
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
neg : ∀ (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

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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

Tactic:
simp [hv]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
neg : r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v

Tactic:
rw [Sphere.secondInter]

Premises used: EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
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
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p

Tactic:
rw [mem_sphere] at h hp

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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 = 0 ∨ r = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫

Tactic:
rw [← hp, dist_smul_vadd_eq_dist _ _ hv] at h

Premises used: EuclideanGeometry.dist_smul_vadd_eq_dist
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
h₁ : r = 0 ∨ r = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫
⊢ ¬v = 0

Tactic:
rw [← hp, dist_smul_vadd_eq_dist _ _ hv] at h

Premises used: EuclideanGeometry.dist_smul_vadd_eq_dist
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
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
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p

Tactic:
rcases h with (h | h)
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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 : ℝ
hv : ¬v = 0
h : r = 0
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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 : ℝ
hv : ¬v = 0
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:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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

Tactic:
s.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem hp ?_

Premises used: EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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'
convert_3 : Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) p'
⊢ p' = p ∨ p' = s.secondInter p (q -ᵥ p) ↔ p' ∈ s

Tactic:
convert! s.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem hp ?_

Premises used: EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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) (affineSpan ℝ {p, q}) p'

Tactic:
hp'
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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'
h : Eq (α := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) (affineSpan ℝ {p, q})
⊢ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) p'

Tactic:
convert! hp'
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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'
h :
  Eq (α := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p, q}))
⊢ Eq (α := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))) (affineSpan ℝ {p, q})

Tactic:
rw [AffineSubspace.eq_iff_direction_eq_of_mem (AffineSubspace.self_mem_mk' p _)
    (left_mem_affineSpan_pair _ _ _)]

Premises used: AffineSubspace.self_mem_mk', AffineSubspace.eq_iff_direction_eq_of_mem, left_mem_affineSpan_pair
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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 (α := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ (q -ᵥ p))))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p, q}))

Tactic:
simp [direction_affineSpan, vectorSpan_pair_rev]

Premises used: direction_affineSpan, vectorSpan_pair_rev
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
simp_rw : (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
⊢ s.secondInter p (r • v) = s.secondInter p v

Tactic:
simp_rw [Sphere.secondInter, real_inner_smul_left, inner_smul_right, smul_smul,
    div_mul_eq_div_div]

Premises used: smul_smul, inner_smul_right, EuclideanGeometry.Sphere.secondInter, real_inner_smul_left, div_mul_eq_div_div
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
rw₅ : (r * (⟪v, p -ᵥ s.center⟫ * -2) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₆ : (⟪v, p -ᵥ s.center⟫ * -2 / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
rw₇ rw₈ : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪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

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]

Premises used: mul_assoc, mul_div_assoc, mul_div_cancel_left₀, mul_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
⊢ Ne (α := ℝ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
rw : s.secondInter p (HSMul.hSMul (α := ℝ) (-1) v) = s.secondInter p v
rw₁ rw₂ : s.secondInter p v = s.secondInter p v
⊢ s.secondInter p (-v) = s.secondInter p v

Tactic:
rw [← neg_one_smul ℝ v, s.secondInter_smul p v (by simp : (-1 : ℝ) ≠ 0)]

Premises used: Real, neg_one_smul, EuclideanGeometry.Sphere.secondInter_smul
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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), s.secondInter (s.secondInter p v) v = p
neg : ∀ (hv : ¬v = 0), s.secondInter (s.secondInter p v) v = p
⊢ s.secondInter (s.secondInter p v) v = p

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
⊢ s.secondInter (s.secondInter p v) v = p

Tactic:
simp [hv]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
⊢ ⟪v, v⟫ ≠ 0

Tactic:
have hv' : ⟪v, v⟫ ≠ 0 := inner_self_ne_zero.2 hv
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
neg :
  ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v + (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) +ᵥ p = p
⊢ s.secondInter (s.secondInter p v) v = p

Tactic:
simp only [Sphere.secondInter, vadd_vsub_assoc, vadd_vadd, inner_add_right, inner_smul_right,
    div_mul_cancel₀ _ hv']

Premises used: div_mul_cancel₀, vadd_vsub_assoc, vadd_vadd, inner_add_right, inner_smul_right, EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
neg : ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v = 0
⊢ ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v + (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) +ᵥ p = p

Tactic:
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, ← add_smul, ← add_div]

Premises used: vsub_eq_zero_iff_eq, add_smul, vadd_vsub, add_div
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
⊢ HSMul.hSMul (α := ℝ) 0 v = 0

Tactic:
zero_smul ℝ _

Premises used: Real, zero_smul
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
h : (-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫ = 0
⊢ ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v = 0

Tactic:
convert! zero_smul ℝ _

Premises used: Real, zero_smul
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
⊢ 0 / ⟪v, v⟫ = 0

Tactic:
zero_div (G₀ := ℝ) _

Premises used: zero_div
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
h : -2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫ = 0
⊢ (-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫ = 0

Tactic:
convert! zero_div (G₀ := ℝ) _

Premises used: zero_div
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
hv' : ⟪v, v⟫ ≠ 0
⊢ -2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
⊢ s.secondInter p (p' -ᵥ p) =
    (AffineMap.lineMap p p' : (a : ℝ) → P) (-2 * ⟪p' -ᵥ p, p -ᵥ s.center⟫ / ⟪p' -ᵥ p, p' -ᵥ p⟫)

Tactic:
rfl

Premises used: EuclideanGeometry.Sphere.secondInter, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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₂ : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) (s.secondInter p₁ (p₂ -ᵥ p₁))

Tactic:
smul_vsub_vadd_mem_affineSpan_pair _ _ _

Premises used: Set.Mem, smul_vsub_vadd_mem_affineSpan_pair, EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
rw : Collinear ℝ (P := P) {s.secondInter p (p' -ᵥ p), p, p'}
⊢ Collinear ℝ (P := P) {p, p', s.secondInter p (p' -ᵥ p)}

Tactic:
rw [Set.pair_comm, Set.insert_comm]

Premises used: Set.insert_comm, Set.pair_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
⊢ Collinear ℝ (P := P) {s.secondInter p (p' -ᵥ p), p, p'}

Tactic:
(collinear_insert_iff_of_mem_affineSpan (s.secondInter_vsub_mem_affineSpan _ _)).2
      (collinear_pair ℝ _ _)

Premises used: Iff.mpr, Real, collinear_pair, EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan, collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
⊢ Collinear ℝ (P := P) {s.secondInter p (p' -ᵥ p), p, p'}

Tactic:
exact
    (collinear_insert_iff_of_mem_affineSpan (s.secondInter_vsub_mem_affineSpan _ _)).2
      (collinear_pair ℝ _ _)

Premises used: Iff.mpr, Real, collinear_pair, EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan, collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
pos : ∀ (h : p' = p), Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
neg : ∀ (h : ¬p' = p), Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
by_cases h : p' = p
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : p' = p
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
wbtw_of_collinear_of_dist_center_le_radius (s.secondInter_collinear p p') hp hp'
      ((Sphere.secondInter_mem _).2 hp) ?_

Premises used: Iff.mpr, EuclideanGeometry.Sphere.secondInter_mem, EuclideanGeometry.Sphere.secondInter_collinear, EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius