Theorem: combiInterior_eq (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
hs : AffineIndependent 𝕜 Subtype.val
⊢ combiInterior 𝕜 s = {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' combiInterior_subset_positive_weighings.antisymm fun 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✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} → x ∈ combiInterior 𝕜 s

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
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} → x ∈ combiInterior 𝕜 s
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
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
    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}

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
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
    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}
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✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 < x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
            ∀ (x_4 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_4 y) → ∑ y ∈ s, x_4 y = 1 → ∀ x_7 ∈ s, x_4 x_7 = 0 → ¬s.centerMass x_4 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
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 < x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
            ∀ (x_4 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_4 y) → ∑ y ∈ s, x_4 y = 1 → ∀ x_7 ∈ s, x_4 x_7 = 0 → ¬s.centerMass x_4 id = x
Tactic:
intro w hw₀ 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✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
    ∀ (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

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
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
    ∀ (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
Tactic:
refine' ⟨⟨w, fun y hy => (hw₀ y hy).le, hw₁, hw₂⟩, fun v hv₀ hv₁ y hy hvy hv₂ => (hw₀ y hy).ne' _⟩
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
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0

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
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Tactic:
rw [← hv₂] at 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✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : s.centerMass w id = s.centerMass v id
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0

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
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : s.centerMass w id = s.centerMass v id
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Tactic:
rw [Finset.centerMass_eq_of_sum_1 _ _ hv₁, Finset.centerMass_eq_of_sum_1 _ _ hw₁] at 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✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0

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
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Tactic:
rw [← hvy]
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
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = v 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✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = v y
Tactic:
exact hs.eq_of_sum_eq_sum_subtype (hw₁.trans hv₁.symm) hw₂ _ hy
State after:
no goals