awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ insert x t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ insert x t, U i
⊢ s ⊆ U x ∪ ⋃ x ∈ t, U x

Tactic:
simp only [Finset.set_biUnion_insert] at hsC

Premises used: Finset.set_biUnion_insert
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ insert x t, IsOpen[inst] (U i)
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
⊢ IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)

Tactic:
simp only [Finset.forall_mem_insert] at hU

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
⊢ ∀ i ∈ t, IsOpen[inst] (U i)

Tactic:
have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
insert :
  ∀ (K₁ K₂ : Set X) (h1K₁ : IsCompact K₁) (h1K₂ : IsCompact K₂) (h2K₁ : K₁ ⊆ U x) (h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i)
    (hK : s = K₁ ∪ K₂),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ Insert.insert x t, K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ Insert.insert x t, K i

Tactic:
rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩

Premises used: And.left, IsCompact.binary_compact_cover, isOpen_biUnion
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
insert :
  ∀ (K : ι → Set X) (h1K : ∀ (i : ι), IsCompact (K i)) (h2K : ∀ (i : ι), K i ⊆ U i) (h3K : K₂ = ⋃ i ∈ t, K i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ Insert.insert x t, K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ Insert.insert x t, K i

Tactic:
rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i

Tactic:
⟨update K x K₁, ?_, ?_, ?_⟩

Premises used: Function.update, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
insert :
  ∀ (hx : i ∉ t) (hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x) (hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x))
    (h2K₁ : K₁ ⊆ U i), IsCompact (update (β := fun (a : ι) ↦ Set X) K i K₁ i)
insert₁ : ∀ (hi : i ≠ x), IsCompact (update (β := fun (a : ι) ↦ Set X) K x K₁ i)
⊢ IsCompact (update (β := fun (a : ι) ↦ Set X) K x K₁ i)

Tactic:
rcases eq_or_ne i x with rfl | hi

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
t : Finset ι
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hx : i ∉ t
hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
h2K₁ : K₁ ⊆ U i
⊢ IsCompact (update (β := fun (a : ι) ↦ Set X) K i K₁ i)

Tactic:
simp only [update_self, h1K₁]

Premises used: Function.update_self
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ IsCompact (update (β := fun (a : ι) ↦ Set X) K x K₁ i)

Tactic:
simp only [update_of_ne hi, h1K]

Premises used: Function.update_of_ne
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
insert :
  ∀ (hx : i ∉ t) (hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x) (hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x))
    (h2K₁ : K₁ ⊆ U i), update (β := fun (a : ι) ↦ Set X) K i K₁ i ⊆ U i
insert₁ : ∀ (hi : i ≠ x), update (β := fun (a : ι) ↦ Set X) K x K₁ i ⊆ U i
⊢ update (β := fun (a : ι) ↦ Set X) K x K₁ i ⊆ U i

Tactic:
rcases eq_or_ne i x with rfl | hi

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
t : Finset ι
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hx : i ∉ t
hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
h2K₁ : K₁ ⊆ U i
⊢ update (β := fun (a : ι) ↦ Set X) K i K₁ i ⊆ U i

Tactic:
simp only [update_self, h2K₁]

Premises used: Function.update_self
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ update (β := fun (a : ι) ↦ Set X) K x K₁ i ⊆ U i

Tactic:
simp only [update_of_ne hi, h2K]

Premises used: Function.update_of_ne
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
⊢ s = ⋃ i ∈ insert x t, update (β := fun (a : ι) ↦ Set X) K x K₁ i

Tactic:
simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

Premises used: Finset.set_biUnion_insert_update
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
empty :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X)
    (hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i))
    (hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i),
    ∃ (K : ι → Set X),
      (∀ (i : ι), IsCompact (K i)) ∧
        (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
insert :
  ∀ (x : ι) (t : Finset ι) (hx : x ∉ t)
    (ih :
      ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
        ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i)
    {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ Insert.insert x t, IsOpen[inst] (U i))
    (hsC : s ⊆ ⋃ i ∈ Insert.insert x t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ Insert.insert x t, K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i

Tactic:
induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

Premises used: Finset.forall_mem_insert, Insert.insert, Finset.notMem_empty, Set.iUnion_false, Set.subset_empty_iff, Set.iUnion_empty, Function.update_self, Finset.set_biUnion_insert, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
empty :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X)
    (hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i))
    (hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i),
    ∃ (K : ι → Set X),
      (∀ (i : ι), IsCompact (K i)) ∧
        (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
insert :
  ∀ (x : ι) (t : Finset ι) (hx : x ∉ t)
    (ih :
      ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
        ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i)
    {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ Insert.insert x t, IsOpen[inst] (U i))
    (hsC : s ⊆ ⋃ i ∈ Insert.insert x t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ Insert.insert x t, K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i

Tactic:
classical
  induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

Premises used: Finset.forall_mem_insert, Insert.insert, Finset.notMem_empty, Set.iUnion_false, Set.subset_empty_iff, Set.iUnion_empty, Function.update_self, Finset.set_biUnion_insert, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : TopologicalSpace Y
f : Y → X
hf : IsInducing f
⊢ R1Space Y

Tactic:
.of_continuous_specializes_imp hf.continuous fun _ _ ↦ hf.specializes_iff.1

Premises used: Topology.IsInducing.specializes_iff, R1Space.of_continuous_specializes_imp, Iff.mp, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
f : Y → X
⊢ R1Space Y

Tactic:
@IsInducing.r1Space _ _ _ _ (.induced f _) f (.induced f)

Premises used: Topology.IsInducing.r1Space, Topology.IsInducing.induced
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
p : X → Prop
⊢ R1Space.{u_1} (Subtype p)

Tactic:
.induced _

Premises used: R1Space.induced
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x : TopologicalSpace X := sInf T
⊢ R1Space X

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: R1Space.mk
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x : TopologicalSpace X := sInf T
refine : ∀ (x y : X), x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
⊢ R1Space X

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
simp :
  LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)

Tactic:
simp only [Specializes, nhds_sInf]

Premises used: nhds_sInf, Specializes
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
pos :
  ∀ (hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)),
    LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
      Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
neg :
  ∀ (hTd : ∀ (t : TopologicalSpace X) (_ : t ∈ T), ¬Disjoint (𝓝 x) (𝓝 y)),
    LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
      Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
by_cases! hTd : ∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
pos :
  ∀ (t : TopologicalSpace X) (htT : t ∈ T) (htd : Disjoint (𝓝 x) (𝓝 y)),
    LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
      Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
rcases hTd with ⟨t, htT, htd⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
t : TopologicalSpace X
htT : t ∈ T
htd : Disjoint (𝓝 x) (𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
.inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)

Premises used: iInf₂_le, Disjoint.mono, Or.inr
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
t : TopologicalSpace X
htT : t ∈ T
htd : Disjoint (𝓝 x) (𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)

Premises used: iInf₂_le, Disjoint.mono
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
hTd : ∀ (t : TopologicalSpace X) (_ : t ∈ T), ¬Disjoint (𝓝 x) (𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
.inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

Premises used: R1Space.specializes_or_disjoint_nhds, iInf₂_mono, Or.inl, Or.resolve_right
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
hTd : ∀ (t : TopologicalSpace X) (_ : t ∈ T), ¬Disjoint (𝓝 x) (𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

Premises used: R1Space.specializes_or_disjoint_nhds, iInf₂_mono, Or.resolve_right
-- Module: Mathlib.Topology.Separation.Basic
Goal:
ι : Type u_3
X : Type u_4
t : ι → TopologicalSpace X
ht : ∀ (i : ι), R1Space X
⊢ R1Space X

Tactic:
.sInf <| forall_mem_range.2 ht

Premises used: Iff.mpr, iInf, Set.forall_mem_range, R1Space.sInf
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
rw : R1Space X
⊢ R1Space X

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
ht : ∀ (i : Bool), R1Space X
⊢ R1Space X

Tactic:
apply R1Space.iInf

Premises used: R1Space.iInf
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ ∀ (i : Bool), R1Space X

Tactic:
simp [*]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
inst_2 : TopologicalSpace Y
inst_3 : R1Space Y
⊢ R1Space (X × Y)

Tactic:
.inf (.induced _) (.induced _)

Premises used: R1Space.induced, R1Space.inf
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : R1Space X_1
x y : X_1
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), R1Space.{u_4} (X i)
⊢ R1Space ((i : ι) → X i)

Tactic:
.iInf fun _ ↦ .induced _

Premises used: R1Space.iInf, R1Space.induced
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ IsCompact (f '' K \ interior s)

Tactic:
have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
simp_rw : ∀ x_1 ∈ f '' K \ interior s, ¬Inseparable (f x) x_1
⊢ SeparatedNhds {f x} (f '' K \ interior s)

Tactic:
simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]

Premises used: separatedNhds_iff_disjoint, disjoint_nhds_nhds_iff_not_inseparable, IsCompact.disjoint_nhdsSet_right, nhdsSet_singleton