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

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
⊢ s = t
Tactic:
classical
by_contra h
have hst : s ∩ t ⊂ s := by
  use inter_subset_left
  intro H
  exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right,
    fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1
refine' hxs.2 (Set.mem_biUnion hst _)
push_cast
exact K.inter_subset_convexHull hs ht ⟨hxs.1, hxt.1⟩
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
⊢ s = t
Tactic:
by_contra h
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ False
Tactic:
have hst : s ∩ t ⊂ s := by
  use inter_subset_left
  intro H
  exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right,
    fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ False
Tactic:
refine' hxs.2 (Set.mem_biUnion hst _)
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) ↑(s ∩ t)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) ↑(s ∩ t)
Tactic:
push_cast
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) (↑s ∩ ↑t)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) (↑s ∩ ↑t)
Tactic:
exact K.inter_subset_convexHull hs ht ⟨hxs.1, hxt.1⟩
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ s ∩ t ⊂ s
Tactic:
use inter_subset_left
State after:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ ¬s ⊆ s ∩ t

State before:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ ¬s ⊆ s ∩ t
Tactic:
intro H
State after:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
H : s ⊆ s ∩ t
⊢ False

State before:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
H : s ⊆ s ∩ t
⊢ False
Tactic:
exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right,
  fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1
State after:
no goals