Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors (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₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
Tactic:
refine' ⟨fun h => ⟨h.1.superset, fun s hs => _⟩, fun h =>
  ⟨h.1.antisymm' fun x hx => _, fun s₁ hs₁ => _⟩⟩
State after:
case 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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂

case 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx : x ∈ K₁.space
⊢ x ∈ K₂.space

case refine'_3
𝕜 : 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂

State before:
case 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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Tactic:
obtain ⟨t, ht, hst⟩ := h.2 hs
State after:
case 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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂

State before:
case 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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Tactic:
obtain ⟨u, hut, hu, hsu⟩ :=
  simplex_combiInteriors_split_interiors_nonempty (K₁.nonempty hs) (K₂.indep ht) hst
State after:
case refine'_1.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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
u : Finset E
hut : u ⊆ t
hu : u.Nonempty
hsu : combiInterior ℝ s ⊆ combiInterior ℝ u
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂

State before:
case refine'_1.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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
u : Finset E
hut : u ⊆ t
hu : u.Nonempty
hsu : combiInterior ℝ s ⊆ combiInterior ℝ u
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Tactic:
exact ⟨u, K₂.down_closed' ht hut hu, hsu⟩
State after:
no goals

State before:
case 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx : x ∈ K₁.space
⊢ x ∈ K₂.space
Tactic:
obtain ⟨s₁, hs₁, hx⟩ := mem_space_iff.1 hx
State after:
case refine'_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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
⊢ x ∈ K₂.space

State before:
case refine'_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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
⊢ x ∈ K₂.space
Tactic:
obtain ⟨s₂, hs₂, hs₁s₂⟩ := h.2 _ hs₁
State after:
case refine'_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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ x ∈ K₂.space

State before:
case refine'_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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ x ∈ K₂.space
Tactic:
rw [mem_space_iff]
State after:
case refine'_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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s ∈ K₂.faces, x ∈ (convexHull ℝ) ↑s

State before:
case refine'_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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s ∈ K₂.faces, x ∈ (convexHull ℝ) ↑s
Tactic:
exact ⟨s₂, hs₂, convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
  (K₁.indep hs₁) (K₂.indep hs₂) hs₁s₂ hx⟩
State after:
no goals

State before:
case refine'_3
𝕜 : 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨s₂, hs₂, hs₁s₂⟩ := h.2 _ hs₁
State after:
case refine'_3.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂

State before:
case refine'_3.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
Tactic:
exact ⟨_, hs₂, convexHull_subset_convexHull_of_combiInterior_subset_combiInterior (K₁.indep hs₁)
  (K₂.indep hs₂) hs₁s₂⟩
State after:
no goals