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

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 s ⊆ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
rw [combiInterior, Finset.convexHull_eq, combiFrontier_eq]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
      {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} ⊆
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
      {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} ⊆
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
rintro x
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} →
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} →
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
simp only [not_exists, and_imp, not_and, mem_setOf_eq, mem_diff, exists_imp]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∀ (x_2 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_2 y) → ∑ y ∈ s, x_2 y = 1 → ∀ x_5 ∈ s, x_2 x_5 = 0 → ¬s.centerMass x_2 id = x) →
            ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∀ (x_2 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_2 y) → ∑ y ∈ s, x_2 y = 1 → ∀ x_5 ∈ s, x_2 x_5 = 0 → ¬s.centerMass x_2 id = x) →
            ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
Tactic:
rintro w hw₁ hw₂ hw₃ q
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
⊢ ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
⊢ ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
Tactic:
refine' ⟨w, fun y hy => _, hw₂, hw₃⟩
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
y : E
hy : y ∈ s
⊢ 0 < w y

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
y : E
hy : y ∈ s
⊢ 0 < w y
Tactic:
exact lt_of_le_of_ne (hw₁ _ hy) (Ne.symm fun t => q w hw₁ hw₂ y hy t hw₃)
State after:
no goals