Theorem: Geometry.SimplicialComplex.subdivides_iff_partition (LeanCamCombi/SimplicialComplex/Subdivision.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
⊢ K₁.Subdivides K₂ ↔
    (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
constructor
State after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
⊢ K₁.Subdivides K₂ →
    (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
⊢ ((K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁) →
    K₁.Subdivides K₂

State before:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
⊢ K₁.Subdivides K₂ →
    (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
rintro ⟨hspace, hsubdiv⟩
State after:
case mp.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
    K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁

State before:
case mp.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
    K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
refine' ⟨_, hspace.le, fun s hs => _⟩
State after:
case mp.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ K₁.faces.Nonempty → K₂.faces.Nonempty

case mp.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ ∃ F ⊆ K₁.faces, combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁

State before:
case mp.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ ∃ F ⊆ K₁.faces, combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
refine' ⟨{t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, fun t ht => ht.1, _⟩
State after:
case mp.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ combiInterior ℝ s = ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

State before:
case mp.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ combiInterior ℝ s = ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
ext x
State after:
case mp.intro.refine'_2.h
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ combiInterior ℝ s ↔ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

State before:
case mp.intro.refine'_2.h
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ combiInterior ℝ s ↔ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
refine' ⟨fun hxs => _, _⟩
State after:
case mp.intro.refine'_2.h.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

case mp.intro.refine'_2.h.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁ → x ∈ combiInterior ℝ s

State before:
case mp.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ K₁.faces.Nonempty → K₂.faces.Nonempty
Tactic:
rintro ⟨s₁, hs₁⟩
State after:
case mp.intro.refine'_1.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
⊢ K₂.faces.Nonempty

State before:
case mp.intro.refine'_1.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
⊢ K₂.faces.Nonempty
Tactic:
obtain ⟨s₂, hs₂, -⟩ := hsubdiv hs₁
State after:
case mp.intro.refine'_1.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
s₂ : Finset E
hs₂ : s₂ ∈ K₂
⊢ K₂.faces.Nonempty

State before:
case mp.intro.refine'_1.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
s₂ : Finset E
hs₂ : s₂ ∈ K₂
⊢ K₂.faces.Nonempty
Tactic:
exact ⟨s₂, hs₂⟩
State after:
no goals

State before:
case mp.intro.refine'_2.h.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
have hxspace := mem_space_iff.2 ⟨s, hs, hxs.1⟩
State after:
case mp.intro.refine'_2.h.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : x ∈ K₂.space
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

State before:
case mp.intro.refine'_2.h.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : x ∈ K₂.space
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
rw [← hspace, ← combiInteriors_cover, mem_iUnion₂] at hxspace
State after:
case mp.intro.refine'_2.h.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

State before:
case mp.intro.refine'_2.h.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
obtain ⟨t, ht, hxt⟩ := hxspace
State after:
case mp.intro.refine'_2.h.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

State before:
case mp.intro.refine'_2.h.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
refine' mem_iUnion₂_of_mem ⟨ht, fun y hyt => _⟩ hxt
State after:
case mp.intro.refine'_2.h.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
⊢ y ∈ combiInterior ℝ s

State before:
case mp.intro.refine'_2.h.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
⊢ y ∈ combiInterior ℝ s
Tactic:
obtain ⟨u, hu, htu⟩ := hsubdiv ht
State after:
case mp.intro.refine'_2.h.refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
⊢ y ∈ combiInterior ℝ s

State before:
case mp.intro.refine'_2.h.refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
⊢ y ∈ combiInterior ℝ s
Tactic:
obtain ⟨W, hWu, htW⟩ := simplex_combiInteriors_split_interiors (K₂.indep hu) htu
State after:
case mp.intro.refine'_2.h.refine'_1.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ s

State before:
case mp.intro.refine'_2.h.refine'_1.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ s
Tactic:
rw [disjoint_interiors hs (K₂.down_closed hu hWu _) hxs (htW hxt)]
State after:
case mp.intro.refine'_2.h.refine'_1.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ W

𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅

State before:
case mp.intro.refine'_2.h.refine'_1.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ W

𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅
Tactic:
exact htW hyt
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅
Tactic:
rintro rfl
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
⊢ False
Tactic:
have := htW hxt
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
this : x ∈ combiInterior ℝ ∅
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
this : x ∈ combiInterior ℝ ∅
⊢ False
Tactic:
simp at this
State after:
no goals

State before:
case mp.intro.refine'_2.h.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁ → x ∈ combiInterior ℝ s
Tactic:
rw [mem_iUnion₂]
State after:
case mp.intro.refine'_2.h.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ (∃ i, ∃ (_ : i ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}), x ∈ combiInterior ℝ i) → x ∈ combiInterior ℝ s

State before:
case mp.intro.refine'_2.h.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ (∃ i, ∃ (_ : i ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}), x ∈ combiInterior ℝ i) → x ∈ combiInterior ℝ s
Tactic:
rintro ⟨t, ⟨-, hts⟩, hxt⟩
State after:
case mp.intro.refine'_2.h.refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
t : Finset E
hxt : x ∈ combiInterior ℝ t
hts : combiInterior ℝ t ⊆ combiInterior ℝ s
⊢ x ∈ combiInterior ℝ s

State before:
case mp.intro.refine'_2.h.refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
t : Finset E
hxt : x ∈ combiInterior ℝ t
hts : combiInterior ℝ t ⊆ combiInterior ℝ s
⊢ x ∈ combiInterior ℝ s
Tactic:
exact hts hxt
State after:
no goals

State before:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
⊢ ((K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁) →
    K₁.Subdivides K₂
Tactic:
rintro ⟨hempty, hspace, hpartition⟩
State after:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ K₁.Subdivides K₂

State before:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ K₁.Subdivides K₂
Tactic:
have hspace : K₁.space = K₂.space := by
  refine' hspace.antisymm fun x hx => _
  rw [← combiInteriors_cover, mem_iUnion₂] at hx ⊢
  obtain ⟨s, hs, hxs⟩ := hx
  obtain ⟨F, hF, hsint⟩ := hpartition _ hs
  rw [hsint, mem_iUnion₂] at hxs
  obtain ⟨t, ht, hxt⟩ := hxs
  exact ⟨t, hF ht, hxt⟩
State after:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
⊢ K₁.Subdivides K₂

State before:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
⊢ K₁.Subdivides K₂
Tactic:
refine' ⟨hspace, fun s hs => _⟩
State after:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain rfl | hsnonempty := s.eq_empty_or_nonempty
State after:
case mpr.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂

case mpr.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨x, hx⟩ := hsnonempty.combiInterior (K₁.indep hs)
State after:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
have hxspace := mem_space_iff.2 ⟨s, hs, hx.1⟩
State after:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : x ∈ K₁.space
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : x ∈ K₁.space
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
rw [hspace, ← combiInteriors_cover, mem_iUnion₂] at hxspace
State after:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨t, ht, hxt⟩ := hxspace
State after:
case mpr.intro.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
use t, ht
State after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t

State before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
Tactic:
rw [← closure_combiInterior_eq_convexHull (K₁.indep hs)]
State after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t

State before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t
Tactic:
refine' closure_minimal (fun x' hx' => _) (isClosed_convexHull _)
State after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
⊢ x' ∈ (convexHull ℝ) ↑t

State before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
have hxspace := mem_space_iff.2 ⟨s, hs, hx'.1⟩
State after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : x' ∈ K₁.space
⊢ x' ∈ (convexHull ℝ) ↑t

State before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : x' ∈ K₁.space
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
rw [hspace, ← combiInteriors_cover, mem_iUnion₂] at hxspace
State after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x' ∈ combiInterior ℝ i
⊢ x' ∈ (convexHull ℝ) ↑t

State before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x' ∈ combiInterior ℝ i
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
obtain ⟨t', ht', hxt'⟩ := hxspace
State after:
case right.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ x' ∈ (convexHull ℝ) ↑t

State before:
case right.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
convert hxt'.1
State after:
case h.e'_5.h.e'_6.h.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ t = t'

State before:
case h.e'_5.h.e'_6.h.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ t = t'
Tactic:
obtain ⟨F, hF, hinterior⟩ := hpartition _ ht
State after:
case h.e'_5.h.e'_6.h.e'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ t = t'

State before:
case h.e'_5.h.e'_6.h.e'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ t = t'
Tactic:
obtain ⟨F', hF', hinterior'⟩ := hpartition _ ht'
State after:
case h.e'_5.h.e'_6.h.e'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ t = t'

State before:
case h.e'_5.h.e'_6.h.e'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ t = t'
Tactic:
apply disjoint_interiors ht ht' (_ : x ∈ _) _
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t

𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t'

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ K₁.space = K₂.space
Tactic:
refine' hspace.antisymm fun x hx => _
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : x ∈ K₂.space
⊢ x ∈ K₁.space

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : x ∈ K₂.space
⊢ x ∈ K₁.space
Tactic:
rw [← combiInteriors_cover, mem_iUnion₂] at hx ⊢
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨s, hs, hxs⟩ := hx
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨F, hF, hsint⟩ := hpartition _ hs
State after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i

State before:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
rw [hsint, mem_iUnion₂] at hxs
State after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hxs : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i

State before:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hxs : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨t, ht, hxt⟩ := hxs
State after:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
t : Finset E
ht : t ∈ F
hxt : x ∈ combiInterior ℝ t
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i

State before:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
t : Finset E
ht : t ∈ F
hxt : x ∈ combiInterior ℝ t
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
exact ⟨t, hF ht, hxt⟩
State after:
no goals

State before:
case mpr.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨t, ht⟩ := hempty ⟨_, hs⟩
State after:
case mpr.intro.intro.inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
t : Finset E
ht : t ∈ K₂.faces
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂

State before:
case mpr.intro.intro.inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
t : Finset E
ht : t ∈ K₂.faces
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂
Tactic:
exact ⟨t, ht, by simp⟩
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
t : Finset E
ht : t ∈ K₂.faces
⊢ (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑t
Tactic:
simp
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t
Tactic:
rw [hinterior, mem_iUnion₂] at hxt ⊢
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hxt : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hxt : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨u, hu, hxu⟩ := hxt
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F
hxu : x ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F
hxu : x ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
Tactic:
exact ⟨u, hu, hxu⟩
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t'
Tactic:
rw [hinterior', mem_iUnion₂] at hxt' ⊢
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hxt' : ∃ i, ∃ (_ : i ∈ F'), x' ∈ combiInterior ℝ i
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hxt' : ∃ i, ∃ (_ : i ∈ F'), x' ∈ combiInterior ℝ i
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨u, hu, hxu⟩ := hxt'
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i
Tactic:
refine' ⟨u, hu, _⟩
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ u

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ u
Tactic:
rw [← disjoint_interiors hs (hF' hu) hx' hxu]
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ s

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ s
Tactic:
exact hx
State after:
no goals