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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
neg : p ≠ s.secondInter p (p' -ᵥ p)
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
refine
    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
-- 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
he : p = s.secondInter p (p' -ᵥ p)
⊢ 0 = ⟪p -ᵥ p', p -ᵥ s.center⟫

Tactic:
rw [eq_comm, Sphere.secondInter_eq_self_iff, ← neg_neg (p' -ᵥ p), inner_neg_left,
    neg_vsub_eq_vsub_rev, neg_eq_zero, eq_comm] at he

Premises used: neg_eq_zero, neg_neg, eq_comm, VSub.vsub, neg_vsub_eq_vsub_rev, EuclideanGeometry.Sphere.secondInter_eq_self_iff, inner_neg_left
-- 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
he : 0 = ⟪p -ᵥ p', p -ᵥ s.center⟫
⊢ False

Tactic:
((inner_pos_or_eq_of_dist_le_radius hp hp').resolve_right (Ne.symm h)).ne he

Premises used: EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, Ne.symm, Or.resolve_right, LT.lt.ne
-- 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
he : 0 = ⟪p -ᵥ p', p -ᵥ s.center⟫
⊢ False

Tactic:
exact ((inner_pos_or_eq_of_dist_le_radius hp hp').resolve_right (Ne.symm h)).ne he

Premises used: EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, Ne.symm, Or.resolve_right, LT.lt.ne
-- 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
⊢ Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
⟨Sphere.wbtw_secondInter hp hp'.le, ?_, ?_⟩

Premises used: EuclideanGeometry.Sphere.wbtw_secondInter, LT.lt.le, And.intro, Sbtw
-- 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
refine_1 : p' ≠ p
refine_2 : p' ≠ s.secondInter p (p' -ᵥ p)
⊢ Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
refine ⟨Sphere.wbtw_secondInter hp hp'.le, ?_, ?_⟩
-- 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
hp : p' ∈ s
⊢ dist p' s.center = s.radius

Tactic:
rw [mem_sphere] at 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
hp : dist p' s.center = s.radius
⊢ False

Tactic:
simp [hp] at 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 p' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
h : p' = s.secondInter p (p' -ᵥ p)
⊢ s.radius < s.radius

Tactic:
rw [h, mem_sphere.1 ((Sphere.secondInter_mem _).2 hp)] at hp'

Premises used: Iff.mpr, EuclideanGeometry.Sphere.secondInter_mem, EuclideanGeometry.mem_sphere, Iff.mp
-- 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' = s.secondInter p (p' -ᵥ p)
hp'₁ : s.radius < s.radius
⊢ p' = s.secondInter p (p' -ᵥ p)

Tactic:
rw [h, mem_sphere.1 ((Sphere.secondInter_mem _).2 hp)] at hp'

Premises used: Iff.mpr, EuclideanGeometry.Sphere.secondInter_mem, EuclideanGeometry.mem_sphere, Iff.mp
-- 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' : s.radius < s.radius
h : p' = s.secondInter p (p' -ᵥ p)
⊢ False

Tactic:
lt_irrefl _ hp'

Premises used: lt_irrefl
-- 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' : s.radius < s.radius
h : p' = s.secondInter p (p' -ᵥ p)
⊢ False

Tactic:
exact lt_irrefl _ hp'

Premises used: lt_irrefl
-- 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
n : ℕ
inst_4 : NeZero n
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
p : P
hp : p ∈ (sx.faceOpposite i).interior
⊢ sx.points i ∉ affineSpan ℝ (Set.range (sx.faceOpposite i).points)

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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
p : P
hp : p ∈ sx.interior
obtain :
  ∀ (w : Fin (n + 1) → ℝ) (hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1)
    (hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)),
    AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
      (s.secondInter (sx.points i)
        ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i) (p -ᵥ sx.points i))

Tactic:
obtain ⟨w, hw, hw01, rfl⟩ := hp

Premises used: 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
⊢ 0 < r

Tactic:
simp [inv_pos, sub_pos, r, (hw01 i).2]

Premises used: sub_pos, inv_pos, And.right
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
⊢ 0 < r

Tactic:
have hrpos : 0 < r := by simp [inv_pos, sub_pos, r, (hw01 i).2]
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
⊢ p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)

Tactic:
simp [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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
⊢ p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)

Tactic:
have hp' : (p' -ᵥ (sx.points i)) =
      r • (Finset.univ.affineCombination ℝ sx.points w -ᵥ (sx.points i)) := by simp [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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
this :
  AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i) (p' -ᵥ sx.points i))
rwa :
  ∀
    (this :
      AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
        (s.secondInter (sx.points i)
          (r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)))),
    AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
      (s.secondInter (sx.points i)
        ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
        (s.secondInter (sx.points i)
          ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))),
    AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
      (s.secondInter (sx.points i)
        ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i)
      ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))

Tactic:
rwa [hp', s.secondInter_smul _ _ hrpos.ne'] at this

Premises used: EuclideanGeometry.Sphere.secondInter_smul, LT.lt.ne'
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
suffices :
  AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i) (p' -ᵥ sx.points i))
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i)
      ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))

Tactic:
suffices (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
      (s.secondInter (sx.points i) (p' -ᵥ (sx.points i))) by
    rwa [hp', s.secondInter_smul _ _ hrpos.ne'] at this
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i) (p' -ᵥ sx.points i))

Tactic:
s.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite hi hsx ?_

Premises used: EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
refine : p' ∈ (sx.faceOpposite i).interior
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i) (p' -ᵥ sx.points i))

Tactic:
refine s.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite hi hsx ?_

Premises used: EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
simp_rw :
  Membership.mem (α := P) (sx.face ⋯).interior
    ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P)
        (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) + Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) :
      P)
⊢ p' ∈ (sx.faceOpposite i).interior

Tactic:
simp_rw [p', ← Finset.univ.affineCombination_piSingle ℝ (sx.points)
    (Finset.mem_univ i), AffineMap.lineMap_apply, Finset.affineCombination_vsub,
    ← LinearMap.map_smul, Finset.weightedVSub_vadd_affineCombination,
    Affine.Simplex.faceOpposite]

Premises used: Finset.affineCombination_vsub, Finset.mem_univ, Affine.Simplex.points, Real, Finset.univ, AffineMap.lineMap_apply, LinearMap.map_smul, Finset.weightedVSub_vadd_affineCombination, Affine.Simplex.faceOpposite, Finset.affineCombination_piSingle
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
rw :
  (∀ (i_1 : Fin (n + 1)),
      Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 →
        0 <
          HAdd.hAdd (β := Fin (n + 1) → ℝ) (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i_1) ∧
    ∀ i_1 ∉ {i}ᶜ,
      HAdd.hAdd (β := Fin (n + 1) → ℝ) (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
          (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i_1 =
        0
hw₁ :
  Eq (α := ℝ)
    (∑ i_1 : Fin (n + 1),
      HAdd.hAdd (β := Fin (n + 1) → ℝ) (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
        (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i_1)
    1
⊢ Membership.mem (α := P) (sx.face ⋯).interior
    ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P)
        (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) + Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) :
      P)

Tactic:
rw [Affine.Simplex.affineCombination_mem_interior_face_iff_pos]

Premises used: Affine.Simplex.affineCombination_mem_interior_face_iff_pos
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
simp :
  (∀ (i_1 : Fin (n + 1)),
      ¬i_1 = i →
        0 <
          HAdd.hAdd (β := ℝ) (r * HSub.hSub (β := ℝ) (w i_1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ))
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ)) ∧
    r * (w i - 1) + 1 = 0
⊢ (∀ (i_1 : Fin (n + 1)),
      Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 →
        0 <
          HAdd.hAdd (β := Fin (n + 1) → ℝ) (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i_1) ∧
    ∀ i_1 ∉ {i}ᶜ,
      HAdd.hAdd (β := Fin (n + 1) → ℝ) (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
          (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i_1 =
        0

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton, Pi.add_apply, Pi.smul_apply, Pi.sub_apply,
      smul_eq_mul, Decidable.not_not, forall_eq, Pi.single_eq_same]

Premises used: Finset.mem_singleton, forall_eq, Finset.mem_compl, Pi.add_apply, Decidable.not_not, smul_eq_mul, Pi.single_eq_same, Pi.sub_apply, Pi.smul_apply
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
⊢ r * (w i - 1) + 1 = 0

Tactic:
grind
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
refine :
  ∀ (j : Fin (n + 1)) (hj : ¬j = i),
    0 <
      HAdd.hAdd (β := ℝ) (r * HSub.hSub (β := ℝ) (w j) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j : ℝ))
        (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j : ℝ)
⊢ (∀ (i_1 : Fin (n + 1)),
      ¬i_1 = i →
        0 <
          HAdd.hAdd (β := ℝ) (r * HSub.hSub (β := ℝ) (w i_1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ))
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ)) ∧
    r * (w i - 1) + 1 = 0

Tactic:
refine ⟨fun j hj ↦ ?_, by grind⟩