Theorem: Geometry.SimplicialComplex.combiInteriors_cover (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = K.space
Tactic:
unfold space
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s
Tactic:
refine' (Set.iUnion₂_mono fun _ _ => _).antisymm (Set.iUnion₂_subset fun s hs => _)
State after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
x✝¹ : Finset E
x✝ : x✝¹ ∈ K
⊢ combiInterior 𝕜 x✝¹ ⊆ (convexHull 𝕜) ↑x✝¹

case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ i ∈ K, combiInterior 𝕜 i

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
Tactic:
rw [simplex_combiInteriors_cover]
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ ⋃ i ∈ K, combiInterior 𝕜 i

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
Tactic:
refine' Set.iUnion₂_mono' fun t hts => _
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
State after:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 i'

case refine'_2.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
ht : t.Nonempty
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'

State before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
x✝¹ : Finset E
x✝ : x✝¹ ∈ K
⊢ combiInterior 𝕜 x✝¹ ⊆ (convexHull 𝕜) ↑x✝¹
Tactic:
exact combiInterior_subset_convexHull
State after:
no goals

State before:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 i'
Tactic:
refine' ⟨s, hs, _⟩
State after:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 s

State before:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 s
Tactic:
rw [combiInterior_empty]
State after:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∅ ⊆ combiInterior 𝕜 s

State before:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∅ ⊆ combiInterior 𝕜 s
Tactic:
exact Set.empty_subset _
State after:
no goals

State before:
case refine'_2.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
ht : t.Nonempty
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'
Tactic:
exact ⟨t, K.down_closed' hs hts ht, Set.Subset.rfl⟩
State after:
no goals