internlm/Lean-Github huggingface dataset:
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : G' ≤ G
⊢ False
Tactic:
exact lt_irrefl _ (trans h hn)
Proof state after:
no goals
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.right.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G'
Tactic:
apply Set.diff_subset
Proof state after:
no goals
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.right.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
ext v w
Proof state after:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w
Tactic:
simp only [deleteEdges_adj, Set.mem_diff, mem_edgeSet, not_and, not_not]
Proof state after:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Tactic:
have : G.Adj v w → G'.Adj v w := fun e => h.le e
Proof state after:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
this : G.Adj v w → G'.Adj v w
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
this : G.Adj v w → G'.Adj v w
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Tactic:
constructor <;> simp (config := {contextual := true}) [this]
Proof state after:
no goals
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G < G'
Tactic:
rintro ⟨s, ⟨⟨v, w⟩, h⟩, hs, rfl⟩
Proof state after:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s < G'
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s < G'
Tactic:
rw [lt_iff_le_and_ne]
Proof state after:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G' ∧ deleteEdges G' s ≠ G'
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G' ∧ deleteEdges G' s ≠ G'
Tactic:
constructor
Proof state after:
case mpr.intro.intro.intro.mk.intro.left
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'

case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≠ G'
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro.left
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'
Tactic:
apply deleteEdges_le
Proof state after:
no goals
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≠ G'
Tactic:
intro hd
Proof state after:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : deleteEdges G' s = G'
⊢ False
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
⊢ False
Tactic:
have := hs h
Proof state after:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : (v, w) ∈ edgeSet G'
⊢ False
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : (v, w) ∈ edgeSet G'
⊢ False
Tactic:
rw [mem_edgeSet] at this
Proof state after:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : G'.Adj v w
⊢ False
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : G'.Adj v w
⊢ False
Tactic:
simp [this, h] at hd
Proof state after:
no goals
Theorem: tsub_tsub_eq_min
Proof state before:
α : Type u_1
inst✝³ : CanonicallyLinearOrderedAddCommMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a - (a - b) = min a b
Tactic:
rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.LocallyFiniteAt.mono
Proof 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 : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
⊢ K.LocallyFiniteAt t
Tactic:
apply hX.subset
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
⊢ {t_1 | t_1 ∈ K.faces ∧ t ⊆ t_1} ⊆ {t | t ∈ K.faces ∧ s ⊆ t}
Theorem: Geometry.SimplicialComplex.LocallyFiniteAt.mono
Proof 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 : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
⊢ {t_1 | t_1 ∈ K.faces ∧ t ⊆ t_1} ⊆ {t | t ∈ K.faces ∧ s ⊆ t}
Tactic:
rintro u ⟨_, _⟩
Proof state after:
case 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 : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
u : Finset E
left✝ : u ∈ K.faces
right✝ : t ⊆ u
⊢ u ∈ {t | t ∈ K.faces ∧ s ⊆ t}
Theorem: Geometry.SimplicialComplex.LocallyFiniteAt.mono
Proof state before:
case 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 : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
u : Finset E
left✝ : u ∈ K.faces
right✝ : t ⊆ u
⊢ u ∈ {t | t ∈ K.faces ∧ s ⊆ t}
Tactic:
exact ⟨‹u ∈ K.faces›, hXY.trans ‹t ⊆ u›⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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!
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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⟩
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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, _⟩⟩
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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⟩
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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⟩)
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof 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
Proof 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