internlm/Lean-Github huggingface dataset:
Theorem: subset_closure_combiInterior
Proof 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 _]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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}
Theorem: subset_closure_combiInterior
Proof 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⟩
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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)⁻¹
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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]
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof 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
Theorem: subset_closure_combiInterior
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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]
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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]
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof 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]
Proof 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)