Theorem: convex_combiInterior (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
⊢ Convex 𝕜 (combiInterior 𝕜 s)
Tactic:
simp_rw [convex_iff_forall_pos, combiInterior_eq hs]
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} →
      ∀ ⦃y : E⦄,
        y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
          ∀ ⦃a b : 𝕜⦄,
            0 < a →
              0 < b →
                a + b = 1 →
                  a • x + b • y ∈ {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
hs : AffineIndependent 𝕜 Subtype.val
⊢ ∀ ⦃x : E⦄,
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
      ∀ ⦃y : E⦄,
        y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
          ∀ ⦃a b : 𝕜⦄,
            0 < a →
              0 < b →
                a + b = 1 →
                  a • x + b • y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
rintro x ⟨v, hv₀, hv₁, rfl⟩ y ⟨w, hw₀, hw₁, rfl⟩ a b ha hb h
State after:
case intro.intro.intro.intro.intro.intro
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a • s.centerMass v id + b • s.centerMass w id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}

State before:
case intro.intro.intro.intro.intro.intro
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a • s.centerMass v id + b • s.centerMass w id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' ⟨fun x => a * v x + b * w x, fun x hx => _, _, _⟩
State after:
case intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
x : E
hx : x ∈ s
⊢ 0 < (fun x => a * v x + b * w x) x

case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ ∑ y ∈ s, (fun x => a * v x + b * w x) y = 1

case intro.intro.intro.intro.intro.intro.refine'_3
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ s.centerMass (fun x => a * v x + b * w x) id = a • s.centerMass v id + b • s.centerMass w id

State before:
case intro.intro.intro.intro.intro.intro.refine'_3
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ s.centerMass (fun x => a * v x + b * w x) id = a • s.centerMass v id + b • s.centerMass w id
Tactic:
rw [Finset.centerMass_segment _ _ _ _ hv₁ hw₁ _ _ h]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
x : E
hx : x ∈ s
⊢ 0 < (fun x => a * v x + b * w x) x
Tactic:
exact add_pos (mul_pos ha <| hv₀ x hx) (mul_pos hb <| hw₀ x hx)
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ ∑ y ∈ s, (fun x => a * v x + b * w x) y = 1
Tactic:
rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum, hv₁, hw₁]
State after:
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a * 1 + b * 1 = 1

State before:
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a * 1 + b * 1 = 1
Tactic:
simp [h]
State after:
no goals