Theorem: subset_closure_combiInterior (LeanCamCombi/SimplicialComplex/Simplex.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
⊢ ↑s ⊆ closure (combiInterior ℝ s)
Tactic:
rintro x (hx : x ∈ s)
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ closure (combiInterior ℝ s)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ closure (combiInterior ℝ s)
Tactic:
apply seqClosure_subset_closure
State after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ seqClosure (combiInterior ℝ s)

State before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ seqClosure (combiInterior ℝ s)
Tactic:
have hsnonempty : s.Nonempty := ⟨x, hx⟩
State after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
⊢ x ∈ seqClosure (combiInterior ℝ s)

State before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
⊢ x ∈ seqClosure (combiInterior ℝ s)
Tactic:
have centroid_weights : ∑ i : E in s, Finset.centroidWeights ℝ s i = 1 := by
  apply Finset.sum_centroidWeights_eq_one_of_nonempty ℝ _ hsnonempty
State after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ x ∈ seqClosure (combiInterior ℝ s)

State before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ x ∈ seqClosure (combiInterior ℝ s)
Tactic:
refine' ⟨fun n => _, fun n => _, _⟩
State after:
case a.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ E

case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => ?m.106180 n) n ∈ combiInterior ℝ s

case a.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun n => ?m.106180 n) Filter.atTop (nhds x)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
Tactic:
apply Finset.sum_centroidWeights_eq_one_of_nonempty ℝ _ hsnonempty
State after:
no goals

State before:
case a.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ E
Tactic:
apply ((n : ℝ) + 2)⁻¹ • s.centroid ℝ id + (1 - ((n : ℝ) + 2)⁻¹) • x
State after:
no goals

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x) n ∈ combiInterior ℝ s
Tactic:
rw [Finset.centroid_def]
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • (Finset.affineCombination ℝ s id) (Finset.centroidWeights ℝ s) + (1 - (↑n + 2)⁻¹) • x) n ∈
    combiInterior ℝ s

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • (Finset.affineCombination ℝ s id) (Finset.centroidWeights ℝ s) + (1 - (↑n + 2)⁻¹) • x) n ∈
    combiInterior ℝ s
Tactic:
rw [affineCombination_eq_centerMass _]
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id + (1 - (↑n + 2)⁻¹) • x) n ∈ combiInterior ℝ s

𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
Tactic:
apply Finset.sum_centroidWeights_eq_one_of_nonempty ℝ _ hsnonempty
State after:
no goals

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id + (1 - (↑n + 2)⁻¹) • x) n ∈ combiInterior ℝ s
Tactic:
rw [← id_def x]
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id + (1 - (↑n + 2)⁻¹) • id x) n ∈ combiInterior ℝ s

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id + (1 - (↑n + 2)⁻¹) • id x) n ∈ combiInterior ℝ s
Tactic:
rw [← Finset.centerMass_ite_eq (R := ℝ) _ _ id hx]
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n =>
        (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id +
          (1 - (↑n + 2)⁻¹) • s.centerMass (fun j => if x = j then 1 else 0) id)
      n ∈
    combiInterior ℝ s

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n =>
        (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id +
          (1 - (↑n + 2)⁻¹) • s.centerMass (fun j => if x = j then 1 else 0) id)
      n ∈
    combiInterior ℝ s
Tactic:
simp only
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id +
      (1 - (↑n + 2)⁻¹) • s.centerMass (fun j => if x = j then 1 else 0) id ∈
    combiInterior ℝ s

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id +
      (1 - (↑n + 2)⁻¹) • s.centerMass (fun j => if x = j then 1 else 0) id ∈
    combiInterior ℝ s
Tactic:
rw [Finset.centerMass_segment]
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ s.centerMass (fun i => (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s i + (1 - (↑n + 2)⁻¹) * if x = i then 1 else 0) id ∈
    combiInterior ℝ s

case a.refine'_2.hw₁
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1

case a.refine'_2.hw₂
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (∑ i ∈ s, if x = i then 1 else 0) = 1

case a.refine'_2.hab
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (↑n + 2)⁻¹ + (1 - (↑n + 2)⁻¹) = 1

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ s.centerMass (fun i => (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s i + (1 - (↑n + 2)⁻¹) * if x = i then 1 else 0) id ∈
    combiInterior ℝ s
Tactic:
rw [combiInterior_eq hs]
State after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ s.centerMass (fun i => (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s i + (1 - (↑n + 2)⁻¹) * if x = i then 1 else 0) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}

State before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ s.centerMass (fun i => (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s i + (1 - (↑n + 2)⁻¹) * if x = i then 1 else 0) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' ⟨_, _, _, rfl⟩
State after:
case a.refine'_2.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∀ y ∈ s, 0 < (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s y + (1 - (↑n + 2)⁻¹) * if x = y then 1 else 0

case a.refine'_2.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ y ∈ s, ((↑n + 2)⁻¹ * Finset.centroidWeights ℝ s y + (1 - (↑n + 2)⁻¹) * if x = y then 1 else 0) = 1

State before:
case a.refine'_2.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ y ∈ s, ((↑n + 2)⁻¹ * Finset.centroidWeights ℝ s y + (1 - (↑n + 2)⁻¹) * if x = y then 1 else 0) = 1
Tactic:
sorry
State after:
no goals

State before:
case a.refine'_2.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∀ y ∈ s, 0 < (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s y + (1 - (↑n + 2)⁻¹) * if x = y then 1 else 0
Tactic:
simp only [mul_boole, Finset.centroidWeights_apply]
State after:
case a.refine'_2.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∀ y ∈ s, 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹ + if x = y then 1 - (↑n + 2)⁻¹ else 0

State before:
case a.refine'_2.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∀ y ∈ s, 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹ + if x = y then 1 - (↑n + 2)⁻¹ else 0
Tactic:
intro y hy
State after:
case a.refine'_2.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹ + if x = y then 1 - (↑n + 2)⁻¹ else 0

State before:
case a.refine'_2.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹ + if x = y then 1 - (↑n + 2)⁻¹ else 0
Tactic:
apply add_pos_of_pos_of_nonneg
State after:
case a.refine'_2.refine'_1.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹

case a.refine'_2.refine'_1.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 ≤ if x = y then 1 - (↑n + 2)⁻¹ else 0

State before:
case a.refine'_2.refine'_1.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹
Tactic:
apply mul_pos
State after:
case a.refine'_2.refine'_1.ha.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑n + 2)⁻¹

case a.refine'_2.refine'_1.ha.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑s.card)⁻¹

State before:
case a.refine'_2.refine'_1.ha.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑n + 2)⁻¹
Tactic:
rw [inv_pos]
State after:
case a.refine'_2.refine'_1.ha.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < ↑n + 2

State before:
case a.refine'_2.refine'_1.ha.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < ↑n + 2
Tactic:
norm_cast
State after:
case a.refine'_2.refine'_1.ha.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < n + 2

State before:
case a.refine'_2.refine'_1.ha.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < n + 2
Tactic:
simp
State after:
no goals

State before:
case a.refine'_2.refine'_1.ha.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < (↑s.card)⁻¹
Tactic:
rw [inv_pos]
State after:
case a.refine'_2.refine'_1.ha.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < ↑s.card

State before:
case a.refine'_2.refine'_1.ha.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < ↑s.card
Tactic:
norm_cast
State after:
case a.refine'_2.refine'_1.ha.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < s.card

State before:
case a.refine'_2.refine'_1.ha.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 < s.card
Tactic:
rwa [Finset.card_pos]
State after:
no goals

State before:
case a.refine'_2.refine'_1.hb
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
⊢ 0 ≤ if x = y then 1 - (↑n + 2)⁻¹ else 0
Tactic:
split_ifs
State after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ 0 ≤ 1 - (↑n + 2)⁻¹

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : ¬x = y
⊢ 0 ≤ 0

State before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ 0 ≤ 1 - (↑n + 2)⁻¹
Tactic:
rw [sub_nonneg]
State after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ (↑n + 2)⁻¹ ≤ 1

State before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ (↑n + 2)⁻¹ ≤ 1
Tactic:
apply inv_le_one
State after:
case pos.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ 1 ≤ ↑n + 2

State before:
case pos.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ 1 ≤ ↑n + 2
Tactic:
norm_cast
State after:
case pos.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ 1 ≤ n + 2

State before:
case pos.ha
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : x = y
⊢ 1 ≤ n + 2
Tactic:
apply Nat.succ_pos
State after:
no goals

State before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
y : E
hy : y ∈ s
h✝ : ¬x = y
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals

State before:
case a.refine'_2.hw₁
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
Tactic:
apply centroid_weights
State after:
no goals

State before:
case a.refine'_2.hw₂
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (∑ i ∈ s, if x = i then 1 else 0) = 1
Tactic:
simp [Finset.sum_boole, Finset.filter_eq, hx]
State after:
no goals

State before:
case a.refine'_2.hab
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (↑n + 2)⁻¹ + (1 - (↑n + 2)⁻¹) = 1
Tactic:
simp only [add_sub_cancel]
State after:
no goals

State before:
case a.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun n => (↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x) Filter.atTop (nhds x)
Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]
State after:
case a.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) Filter.atTop (nhds 0)

State before:
case a.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) Filter.atTop (nhds 0)
Tactic:
convert_to Filter.Tendsto (fun e : ℕ => ((e : ℝ) + 2)⁻¹ * ‖s.centroid ℝ id - x‖) Filter.atTop _
State after:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) = fun e =>
    (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖

case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖) Filter.atTop (nhds 0)

State before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖) Filter.atTop (nhds 0)
Tactic:
suffices Filter.Tendsto (fun e : ℕ => (↑(e + 2) : ℝ)⁻¹) Filter.atTop (nhds 0) by
  simpa using this.mul_const _
State after:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑(e + 2))⁻¹) Filter.atTop (nhds 0)

State before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑(e + 2))⁻¹) Filter.atTop (nhds 0)
Tactic:
refine' tendsto_inv_atTop_zero.comp _
State after:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ↑(e + 2)) Filter.atTop Filter.atTop

State before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ↑(e + 2)) Filter.atTop Filter.atTop
Tactic:
rw [tendsto_natCast_atTop_iff]
State after:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => e + 2) Filter.atTop Filter.atTop

State before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => e + 2) Filter.atTop Filter.atTop
Tactic:
apply Filter.tendsto_add_atTop_nat
State after:
no goals

State before:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) = fun e =>
    (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖
Tactic:
ext n
State after:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ‖(↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x - x‖ = (↑n + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖

State before:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ‖(↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x - x‖ = (↑n + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖
Tactic:
rw [add_sub_assoc, sub_smul, sub_right_comm, one_smul, sub_self, zero_sub, ← smul_neg, ←
  smul_add, norm_smul_of_nonneg, ← sub_eq_add_neg]
State after:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ (↑n + 2)⁻¹

State before:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ (↑n + 2)⁻¹
Tactic:
rw [inv_nonneg]
State after:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ ↑n + 2

State before:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ ↑n + 2
Tactic:
norm_cast
State after:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ n + 2

State before:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ n + 2
Tactic:
apply Nat.zero_le
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
this : Filter.Tendsto (fun e => (↑(e + 2))⁻¹) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun e => (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖) Filter.atTop (nhds 0)
Tactic:
simpa using this.mul_const _
State after:
no goals