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
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
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
have rw₆ : (⟪v, p -ᵥ s.center⟫ * -2 / ⟪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
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
⊢ (-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 * ⟪v, p -ᵥ s.center⟫ / ⟪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
⊢ s.secondInter p (-v) = s.secondInter p v
have rw : s.secondInter p (HSMul.hSMul (α := ℝ) (-1) v) = s.secondInter p v
Tactic: rw [← neg_one_smul ℝ v, s.secondInter_smul p v (by simp : (-1 : ℝ) ≠ 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
rw : s.secondInter p (HSMul.hSMul (α := ℝ) (-1) v) = s.secondInter p v
⊢ s.secondInter p (-v) = s.secondInter p v
have rw₁ : s.secondInter p v = s.secondInter p v
Tactic: rw [← neg_one_smul ℝ v, s.secondInter_smul p v (by simp : (-1 : ℝ) ≠ 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
⊢ s.secondInter (s.secondInter p v) v = p
have pos : ∀ (hv : v = 0), s.secondInter (s.secondInter p v) v = p
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), s.secondInter (s.secondInter p v) v = p
⊢ s.secondInter (s.secondInter p v) v = p
have neg : ∀ (hv : ¬v = 0), s.secondInter (s.secondInter p v) v = p
Tactic: by_cases hv : v = 0
-- 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
v : V
hv : ¬v = 0
⊢ s.secondInter (s.secondInter p v) v = p
have hv' : ⟪v, v⟫ ≠ 0
Tactic: have hv' : ⟪v, v⟫ ≠ 0 := inner_self_ne_zero.2 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
hv : ¬v = 0
hv' : ⟪v, v⟫ ≠ 0
⊢ s.secondInter (s.secondInter p v) v = p
have neg : ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v + (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) +ᵥ p = p
Tactic: simp only [Sphere.secondInter, vadd_vsub_assoc, vadd_vadd, inner_add_right, inner_smul_right,
    div_mul_cancel₀ _ 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
hv : ¬v = 0
hv' : ⟪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
have neg : ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v = 0
Tactic: rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, ← add_smul, ← add_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
hv : ¬v = 0
hv' : ⟪v, v⟫ ≠ 0
⊢ ((-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫) • v = 0
have h : (-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫ = 0
Tactic: convert! zero_smul ℝ _
-- 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
hv' : ⟪v, v⟫ ≠ 0
⊢ (-2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫) / ⟪v, v⟫ = 0
have h : -2 * (-2 * ⟪v, p -ᵥ s.center⟫ + ⟪v, p -ᵥ s.center⟫) + -2 * ⟪v, p -ᵥ s.center⟫ = 0
Tactic: convert! zero_div (G₀ := ℝ) _
-- 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' : P
⊢ Collinear ℝ (P := P) {p, p', s.secondInter p (p' -ᵥ p)}
have rw : Collinear ℝ (P := P) {s.secondInter p (p' -ᵥ p), p, p'}
Tactic: rw [Set.pair_comm, Set.insert_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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
have pos : ∀ (h : p' = p), Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
Tactic: by_cases h : p' = p
-- 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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
pos : ∀ (h : p' = p), Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
have neg : ∀ (h : ¬p' = p), Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
Tactic: by_cases h : p' = p
-- 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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
have neg : 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) ?_
-- 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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : p = s.secondInter p (p' -ᵥ p)
⊢ False
have he₁ : 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
Cleared hypotheses: he
-- 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' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
⊢ Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
have refine_1 : p' ≠ p
Tactic: refine ⟨Sphere.wbtw_secondInter hp hp'.le, ?_, ?_⟩
-- 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' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
refine_1 : p' ≠ p
⊢ Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
have refine_2 : p' ≠ s.secondInter p (p' -ᵥ p)
Tactic: refine ⟨Sphere.wbtw_secondInter hp hp'.le, ?_, ?_⟩
-- 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
hp : p' ∈ s
⊢ False
have hp₁ : dist p' s.center = s.radius
Tactic: rw [mem_sphere] at hp
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' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
h : p' = s.secondInter p (p' -ᵥ p)
⊢ False
have hp'₁ : s.radius < s.radius
Tactic: rw [h, mem_sphere.1 ((Sphere.secondInter_mem _).2 hp)] 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
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
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
    (s.secondInter (sx.points i) (p -ᵥ sx.points i))
have 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))
Tactic: obtain ⟨w, hw, hw01, rfl⟩ := hp
Cleared hypotheses: p, 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
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)⁻¹
⊢ 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))
have hrpos : 0 < r
Tactic: have hrpos : 0 < r := by simp [inv_pos, sub_pos, r, (hw01 i).2]
-- 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
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
⊢ 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))
have hp' : 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']
-- 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
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))
⊢ 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))
have 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))
Tactic: rwa [hp', s.secondInter_smul _ _ hrpos.ne'] at this
Cleared hypotheses: this
-- 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
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))
⊢ 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))
have 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))
Tactic: rwa [hp', s.secondInter_smul _ _ hrpos.ne'] at this
Cleared hypotheses: this
-- 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
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)
      ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i))
have suffices : AffineSubspace.SOppSide (affineSpan ℝ (Set.range (sx.faceOpposite i).points)) (sx.points i)
  (s.secondInter (sx.points i) (p' -ᵥ 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
-- 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
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))
have refine : p' ∈ (sx.faceOpposite i).interior
Tactic: refine s.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite hi hsx ?_
-- 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
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)
⊢ p' ∈ (sx.faceOpposite i).interior
have simp_rw : Membership.mem (α := P) (sx.face sorry).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: 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]
-- 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
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)
⊢ 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)
have 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
Tactic: rw [Affine.Simplex.affineCombination_mem_interior_face_iff_pos]