Theorem: interior_zero_iff_open_cover (Sard/ObsoleteHelpers.lean)

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ interior s = ∅ ↔ ∀ (α : I), interior (s ∩ U α) = ∅
Tactic:
constructor
State after:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ interior s = ∅ → ∀ (α : I), interior (s ∩ U α) = ∅

case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ (∀ (α : I), interior (s ∩ U α) = ∅) → interior s = ∅

State before:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ interior s = ∅ → ∀ (α : I), interior (s ∩ U α) = ∅
Tactic:
intro hs α
State after:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ interior (s ∩ U α) = ∅

State before:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ interior (s ∩ U α) = ∅
Tactic:
have aux: interior (s ∩ U α) ⊆ interior s := by
  apply interior_mono
  apply Set.inter_subset_left
State after:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
aux : interior (s ∩ U α) ⊆ interior s
⊢ interior (s ∩ U α) = ∅

State before:
case mp
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
aux : interior (s ∩ U α) ⊆ interior s
⊢ interior (s ∩ U α) = ∅
Tactic:
exact Set.subset_eq_empty aux hs
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ interior (s ∩ U α) ⊆ interior s
Tactic:
apply interior_mono
State after:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ s ∩ U α ⊆ s

State before:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
hs : interior s = ∅
α : I
⊢ s ∩ U α ⊆ s
Tactic:
apply Set.inter_subset_left
State after:
no goals

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
⊢ (∀ (α : I), interior (s ∩ U α) = ∅) → interior s = ∅
Tactic:
intro h
State after:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ interior s = ∅

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ interior s = ∅
Tactic:
suffices ∀ V : Set X, (hV : V ⊆ s ∧ IsOpen V) → V = ∅ by sorry
State after:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ ∀ (V : Set X), V ⊆ s ∧ IsOpen V → V = ∅

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
⊢ ∀ (V : Set X), V ⊆ s ∧ IsOpen V → V = ∅
Tactic:
rintro V ⟨hVS, hV⟩
State after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
⊢ V = ∅

State before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
⊢ V = ∅
Tactic:
have h' : ∀ α : I, V ∩ U α = ∅ := by
  intro α
  have h₁ : IsOpen (V ∩ U α) := by exact IsOpen.inter hV (hU α)
  have h₂ : V ∩ U α ⊆ s ∩ U α := by exact Set.inter_subset_inter_left (U α) hVS
  have h₃ : V ∩ U α ⊆ interior (s ∩ U α) := by exact interior_maximal h₂ h₁
  exact Set.subset_eq_empty h₃ (h α)
State after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
⊢ V = ∅

State before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
⊢ V = ∅
Tactic:
have h'' : V = ⋃ (α : I), (V ∩ U α) := by
  ext i
  rw [Set.mem_iUnion]
  sorry
State after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ V = ∅

State before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ V = ∅
Tactic:
rw [h'']
State after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ⋃ α, V ∩ U α = ∅

State before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ⋃ α, V ∩ U α = ∅
Tactic:
simp only [Set.iUnion_eq_empty]
State after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ∀ (i : I), V ∩ U i = ∅

State before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ∀ (i : I), V ∩ U i = ∅
Tactic:
tauto
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
this : ∀ (V : Set X), V ⊆ s ∧ IsOpen V → V = ∅
⊢ interior s = ∅
Tactic:
sorry
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
⊢ ∀ (α : I), V ∩ U α = ∅
Tactic:
intro α
State after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
⊢ V ∩ U α = ∅

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
⊢ V ∩ U α = ∅
Tactic:
have h₁ : IsOpen (V ∩ U α) := by exact IsOpen.inter hV (hU α)
State after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
⊢ V ∩ U α = ∅

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
⊢ V ∩ U α = ∅
Tactic:
have h₂ : V ∩ U α ⊆ s ∩ U α := by exact Set.inter_subset_inter_left (U α) hVS
State after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
⊢ V ∩ U α = ∅

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
⊢ V ∩ U α = ∅
Tactic:
have h₃ : V ∩ U α ⊆ interior (s ∩ U α) := by exact interior_maximal h₂ h₁
State after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
h₃ : V ∩ U α ⊆ interior (s ∩ U α)
⊢ V ∩ U α = ∅

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
h₃ : V ∩ U α ⊆ interior (s ∩ U α)
⊢ V ∩ U α = ∅
Tactic:
exact Set.subset_eq_empty h₃ (h α)
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
⊢ IsOpen (V ∩ U α)
Tactic:
exact IsOpen.inter hV (hU α)
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
⊢ V ∩ U α ⊆ s ∩ U α
Tactic:
exact Set.inter_subset_inter_left (U α) hVS
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
⊢ V ∩ U α ⊆ interior (s ∩ U α)
Tactic:
exact interior_maximal h₂ h₁
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
⊢ V = ⋃ α, V ∩ U α
Tactic:
ext i
State after:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ i ∈ ⋃ α, V ∩ U α

State before:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ i ∈ ⋃ α, V ∩ U α
Tactic:
rw [Set.mem_iUnion]
State after:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ ∃ i_1, i ∈ V ∩ U i_1

State before:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ ∃ i_1, i ∈ V ∩ U i_1
Tactic:
sorry
State after:
no goals