Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
hU : (interior (⋃ k, f k)).Nonempty
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
set s := interior (⋃ k, f k)
State after:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
⊢ ∃ k, (interior (f k)).Nonempty

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
set f' : Option B → Set A := fun k ↦
  match k with
  | none => sᶜ
  | some k => f k
State after:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
⊢ ∃ k, (interior (f k)).Nonempty

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
have hc' : ∀ k, IsClosed (f' k) := by
  simp only [s, Option.forall, isClosed_compl_iff, isOpen_interior, true_and, f']
  exact fun k ↦ hc k
State after:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
⊢ ∃ k, (interior (f k)).Nonempty

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
have d := dense_iUnion_interior_of_closed hc' hU'
State after:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
⊢ ∃ k, (interior (f k)).Nonempty

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
rcases Dense.exists_mem_open d isOpen_interior hU with ⟨x, xi, xs⟩
State after:
case intro.intro
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
x : A
xi : x ∈ ⋃ i, interior (f' i)
xs : x ∈ interior (⋃ k, f k)
⊢ ∃ k, (interior (f k)).Nonempty

State before:
case intro.intro
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
x : A
xi : x ∈ ⋃ i, interior (f' i)
xs : x ∈ interior (⋃ k, f k)
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
rcases Set.mem_iUnion.mp xi with ⟨k, xk⟩
State after:
case intro.intro.intro
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
x : A
xi : x ∈ ⋃ i, interior (f' i)
xs : x ∈ interior (⋃ k, f k)
k : Option B
xk : x ∈ interior (f' k)
⊢ ∃ k, (interior (f k)).Nonempty

State before:
case intro.intro.intro
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
x : A
xi : x ∈ ⋃ i, interior (f' i)
xs : x ∈ interior (⋃ k, f k)
k : Option B
xk : x ∈ interior (f' k)
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
match k with
| none => simp only [s, interior_compl, Set.mem_compl_iff, subset_closure xs,
    not_true_eq_false, f'] at xk
| some k => exact ⟨k, Set.nonempty_of_mem xk⟩
State after:
no goals

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
⊢ ∀ (k : Option B), IsClosed (f' k)
Tactic:
simp only [s, Option.forall, isClosed_compl_iff, isOpen_interior, true_and, f']
State after:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
⊢ ∀ (x : B), IsClosed (f x)

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
⊢ ∀ (x : B), IsClosed (f x)
Tactic:
exact fun k ↦ hc k
State after:
no goals

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
⊢ ⋃ k, f' k = univ
Tactic:
apply Set.ext
State after:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
⊢ ∀ (x : A), x ∈ ⋃ k, f' k ↔ x ∈ univ

State before:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
⊢ ∀ (x : A), x ∈ ⋃ k, f' k ↔ x ∈ univ
Tactic:
intro x
State after:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
⊢ x ∈ ⋃ k, f' k ↔ x ∈ univ

State before:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
⊢ x ∈ ⋃ k, f' k ↔ x ∈ univ
Tactic:
refine ⟨fun _ ↦ Set.mem_univ _, ?_⟩
State after:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
⊢ x ∈ univ → x ∈ ⋃ k, f' k

State before:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
⊢ x ∈ univ → x ∈ ⋃ k, f' k
Tactic:
intro _
State after:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
⊢ x ∈ ⋃ k, f' k

State before:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
⊢ x ∈ ⋃ k, f' k
Tactic:
rw [Set.mem_iUnion]
State after:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
⊢ ∃ i, x ∈ f' i

State before:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
⊢ ∃ i, x ∈ f' i
Tactic:
by_cases m : x ∈ s
State after:
case pos
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∈ s
⊢ ∃ i, x ∈ f' i

case neg
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∉ s
⊢ ∃ i, x ∈ f' i

State before:
case pos
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∈ s
⊢ ∃ i, x ∈ f' i
Tactic:
rcases Set.mem_iUnion.mp (interior_subset m) with ⟨k, mk⟩
State after:
case pos.intro
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∈ s
k : B
mk : x ∈ f k
⊢ ∃ i, x ∈ f' i

State before:
case pos.intro
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∈ s
k : B
mk : x ∈ f k
⊢ ∃ i, x ∈ f' i
Tactic:
use some k
State after:
no goals

State before:
case neg
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∉ s
⊢ ∃ i, x ∈ f' i
Tactic:
use none
State after:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∉ s
⊢ x ∈ f' none

State before:
case h
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
x : A
a✝ : x ∈ univ
m : x ∉ s
⊢ x ∈ f' none
Tactic:
exact m
State after:
no goals

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
x : A
xi : x ∈ ⋃ i, interior (f' i)
xs : x ∈ interior (⋃ k, f k)
k : Option B
xk : x ∈ interior (f' none)
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
simp only [s, interior_compl, Set.mem_compl_iff, subset_closure xs,
not_true_eq_false, f'] at xk
State after:
no goals

State before:
E : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : CompleteSpace E
inst✝³ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
hc' : ∀ (k : Option B), IsClosed (f' k)
hU' : ⋃ k, f' k = univ
d : Dense (⋃ i, interior (f' i))
x : A
xi : x ∈ ⋃ i, interior (f' i)
xs : x ∈ interior (⋃ k, f k)
k✝ : Option B
k : B
xk : x ∈ interior (f' (some k))
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
exact ⟨k, Set.nonempty_of_mem xk⟩
State after:
no goals