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

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s = ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
apply Subset.antisymm _ _
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ (convexHull 𝕜) ↑s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
refine s.strongInductionOn ?_
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∀ (s : Finset E),
    (∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1) →
      (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∀ (s : Finset E),
    (∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1) →
      (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
rintro s ih x hx
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
by_cases h : x ∈ combiFrontier 𝕜 s
State after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∈ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∉ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

State before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∈ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
rw [mem_combiFrontier_iff] at h
State after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

State before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
obtain ⟨t, st, ht⟩ := h
State after:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

State before:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
specialize ih _ st ht
State after:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : x ∈ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

State before:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : x ∈ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
simp only [exists_prop, Set.mem_iUnion] at ih ⊢
State after:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : ∃ i ⊆ t, x ∈ combiInterior 𝕜 i
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i

State before:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : ∃ i ⊆ t, x ∈ combiInterior 𝕜 i
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
Tactic:
obtain ⟨Z, Zt, hZ⟩ := ih
State after:
case pos.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
Z : Finset E
Zt : Z ⊆ t
hZ : x ∈ combiInterior 𝕜 Z
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i

State before:
case pos.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
Z : Finset E
Zt : Z ⊆ t
hZ : x ∈ combiInterior 𝕜 Z
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
Tactic:
exact ⟨_, Zt.trans st.1, hZ⟩
State after:
no goals

State before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∉ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
exact subset_iUnion₂ s Subset.rfl ⟨hx, h⟩
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ (convexHull 𝕜) ↑s
Tactic:
exact iUnion₂_subset fun t ht ↦ diff_subset.trans $ convexHull_mono ht
State after:
no goals