Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces (LeanCamCombi/SimplicialComplex/Finite.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 t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ K.LocallyFinite ↔ ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
Tactic:
constructor
State after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ K.LocallyFinite → ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite

case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite) → K.LocallyFinite

State before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ K.LocallyFinite → ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
Tactic:
unfold LocallyFinite
State after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∀ ⦃s : Finset E⦄, s ∈ K.faces → s.Nonempty → K.LocallyFiniteAt s) →
    ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite

State before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∀ ⦃s : Finset E⦄, s ∈ K.faces → s.Nonempty → K.LocallyFiniteAt s) →
    ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
Tactic:
contrapose!
State after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∃ x, ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite) → ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

State before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∃ x, ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite) → ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
Tactic:
rintro ⟨x, hx⟩
State after:
case mp.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

State before:
case mp.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
Tactic:
by_cases hxspace : x ∈ K.space
State after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

State before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
Tactic:
obtain ⟨s, ⟨hX, hXhull, hXbound⟩, hXunique⟩ := combiInteriors_partition hxspace
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
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hXunique : ∀ (y : Finset E), (fun s => s ∈ K ∧ x ∈ combiInterior 𝕜 s) y → y = s
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

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
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hXunique : ∀ (y : Finset E), (fun s => s ∈ K ∧ x ∈ combiInterior 𝕜 s) y → y = s
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
Tactic:
simp at hXunique
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
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

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
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
Tactic:
refine'
  ⟨s, hX, Finset.nonempty_of_ne_empty _, fun hXlocallyfinite =>
    hx <| hXlocallyfinite.subset fun t hY => ⟨hY.1, _⟩⟩
State after:
case pos.intro.intro.intro.intro.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✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
⊢ s ≠ ∅

case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
⊢ s ⊆ t

State before:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
⊢ s ⊆ t
Tactic:
have hXYhull := K.inter_subset_convexHull hX hY.1 ⟨hXhull, hY.2⟩
State after:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) (↑s ∩ ↑t)
⊢ s ⊆ t

State before:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) (↑s ∩ ↑t)
⊢ s ⊆ t
Tactic:
rw [← Finset.coe_inter] at hXYhull
State after:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) ↑(s ∩ t)
⊢ s ⊆ t

State before:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) ↑(s ∩ t)
⊢ s ⊆ t
Tactic:
by_contra hXY
State after:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) ↑(s ∩ t)
hXY : ¬s ⊆ t
⊢ False

State before:
case pos.intro.intro.intro.intro.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✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) ↑(s ∩ t)
hXY : ¬s ⊆ t
⊢ False
Tactic:
exact hXbound (mem_combiFrontier_iff.2 ⟨s ∩ t, ⟨Finset.inter_subset_left,
  fun hXXY => hXY (Finset.subset_inter_iff.1 hXXY).2⟩, hXYhull⟩)
State after:
no goals

State before:
case pos.intro.intro.intro.intro.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✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
⊢ s ≠ ∅
Tactic:
rintro rfl
State after:
case pos.intro.intro.intro.intro.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✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
hX : ∅ ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑∅
hXbound : x ∉ combiFrontier 𝕜 ∅
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = ∅
⊢ False

State before:
case pos.intro.intro.intro.intro.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✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
hX : ∅ ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑∅
hXbound : x ∉ combiFrontier 𝕜 ∅
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = ∅
⊢ False
Tactic:
simp at hXhull
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
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
Tactic:
refine (hx ?_).elim
State after:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite

State before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
Tactic:
convert finite_empty
State after:
case h.e'_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✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s} = ∅

State before:
case h.e'_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✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s} = ∅
Tactic:
exact eq_empty_of_forall_not_mem fun s hX => hxspace <| mem_biUnion hX.1 hX.2
State after:
no goals

State before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite) → K.LocallyFinite
Tactic:
rintro hS s - ⟨x, hx⟩
State after:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
hS : ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
s : Finset E
x : E
hx : x ∈ s
⊢ K.LocallyFiniteAt s

State before:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
hS : ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
s : Finset E
x : E
hx : x ∈ s
⊢ K.LocallyFiniteAt s
Tactic:
exact (hS x).subset fun t => And.imp_right fun ht => subset_convexHull _ _ <| ht hx
State after:
no goals