internlm/Lean-Github huggingface dataset:
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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'
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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⟩
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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⟩
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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⟩
Proof state after:
no goals
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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']
Proof 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)
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof state after:
no goals
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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 _, ?_⟩
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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 _
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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]
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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⟩
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof state after:
no goals
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof 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
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof state after:
no goals
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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
Proof state after:
no goals
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
Proof 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⟩
Proof state after:
no goals
Theorem: forall_const_and_distrib
Proof 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 : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Tactic:
have d := @forall_and A (fun _ ↦ p) q
Proof 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 : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ (A → p) ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Theorem: forall_const_and_distrib
Proof 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 : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ (A → p) ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Tactic:
simp only [forall_const] at d
Proof 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 : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Theorem: forall_const_and_distrib
Proof 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 : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Tactic:
exact d
Proof state after:
no goals