awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
⊢ Continuous[instTopologicalSpaceSubtype, inst]
      (comp (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) Sum.inl) ∧
    Continuous[instTopologicalSpaceSubtype, inst]
      (comp (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) Sum.inr)

Tactic:
⟨continuous_subtype_val, continuous_subtype_val⟩

Premises used: continuous_subtype_val, And.intro
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
⊢ Continuous[instTopologicalSpaceSubtype, inst]
      (comp (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) Sum.inl) ∧
    Continuous[instTopologicalSpaceSubtype, inst]
      (comp (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) Sum.inr)

Tactic:
exact ⟨continuous_subtype_val, continuous_subtype_val⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
⊢ coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst

Tactic:
have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
⊢ IsClopenable s

Tactic:
⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩

Premises used: PolishSpace.IsClopenable, IsClosed.mono, instTopologicalSpaceSum, TopologicalSpace.coinduced, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
refine_1 : PolishSpace α
refine_2 : IsOpen[coinduced (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) instTopologicalSpaceSum] s
⊢ IsClopenable s

Tactic:
refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
refine_1 : PolishSpace α
⊢ PolishSpace α

Tactic:
rw [← f.induced_symm]

Premises used: Equiv.induced_symm
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
⊢ PolishSpace α

Tactic:
f.symm.polishSpace_induced

Premises used: Equiv.polishSpace_induced, Equiv.symm
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
⊢ PolishSpace α

Tactic:
exact f.symm.polishSpace_induced

Premises used: Equiv.polishSpace_induced, Equiv.symm
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
⊢ IsOpen[instTopologicalSpaceSubtype]
      (preimage (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) Sum.inl
        ((⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) ⁻¹' s)) ∧
    IsOpen[instTopologicalSpaceSubtype]
      (preimage (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) Sum.inr
        ((⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) ⁻¹' s))

Tactic:
simp [preimage_preimage, f, t]

Premises used: Set.preimage_preimage
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
haveI haveI₁ haveI₂ haveI₃ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)), IsClopenable s
haveI₄ haveI₅ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)), IsClopenable s
haveI₆ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
      let f := Equiv.Set.sumCompl s;
      ∀
        (hle :
          coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
              instTopologicalSpaceSum ≤
            inst),
        IsClopenable s
refine_1 :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
      let f := Equiv.Set.sumCompl s;
      ∀
        (hle :
          coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
              instTopologicalSpaceSum ≤
            inst),
        PolishSpace α
refine_2 refine_2₁ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
      let f := Equiv.Set.sumCompl s;
      ∀
        (hle :
          coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
              instTopologicalSpaceSum ≤
            inst),
        IsOpen[coinduced (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) instTopologicalSpaceSum] s
⊢ IsClopenable s

Tactic:
classical
  haveI : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  haveI : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]

Premises used: isOpen_sum_iff, Set.preimage_preimage, isOpen_coinduced
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsClopenable s
rcases :
  ∀ (t : TopologicalSpace α) (t_le : t ≤ inst) (t_polish : PolishSpace α) (h : IsClosed s) (h' : IsOpen s),
    IsClopenable sᶜ
⊢ IsClopenable sᶜ

Tactic:
rcases hs with ⟨t, t_le, t_polish, h, h'⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst
t_polish : PolishSpace α
h : IsClosed[t] s
h' : IsOpen[t] s
⊢ IsClopenable sᶜ

Tactic:
⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩

Premises used: IsClosed.isOpen_compl, PolishSpace.IsClopenable, IsOpen.isClosed_compl, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst
t_polish : PolishSpace α
h : IsClosed[t] s
h' : IsOpen[t] s
⊢ IsClopenable sᶜ

Tactic:
exact ⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsOpen[inst] s
⊢ IsClopenable s

Tactic:
simpa using hs.isClosed_compl.isClopenable.compl

Premises used: PolishSpace.IsClopenable.compl, IsOpen.isClosed_compl, IsClosed.isClopenable
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), IsClopenable (s n)
choose :
  ∀ (m : (n : ℕ) → TopologicalSpace α) (mt : ∀ (n : ℕ), m n ≤ t) (m_polish : ∀ (n : ℕ), PolishSpace α),
    (∀ (n : ℕ), IsClosed[m n] (s n)) →
      ∀ (m_open : ∀ (n : ℕ), IsOpen[m n] (s n)), IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)

Tactic:
choose m mt m_polish _ m_open using hs

Premises used: mt
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
⊢ ∃ (t' : TopologicalSpace α), (∀ (n : ℕ), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α

Tactic:
exists_polishSpace_forall_le m mt m_polish

Premises used: PolishSpace.exists_polishSpace_forall_le
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
obtain :
  ∀ (t' : TopologicalSpace α) (t'm : ∀ (n : ℕ), t' ≤ m n) (t'_polish : PolishSpace α),
    IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)

Tactic:
obtain ⟨t', t'm, -, t'_polish⟩ :
      ∃ t' : TopologicalSpace α, (∀ n : ℕ, t' ≤ m n) ∧ t' ≤ t ∧ @PolishSpace α t' :=
    exists_polishSpace_forall_le m mt m_polish

Premises used: PolishSpace.exists_polishSpace_forall_le, TopologicalSpace
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h_1 : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
h : ∀ (i : ℕ), IsOpen[t'] (s i)
⊢ IsOpen[t'] (⋃ (n : ℕ), s n)

Tactic:
apply isOpen_iUnion

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h_1 : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
n : ℕ
h : IsOpen[m n] (s n)
⊢ IsOpen[t'] (s n)

Tactic:
apply t'm n
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
n : ℕ
⊢ IsOpen[m n] (s n)

Tactic:
m_open n
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
n : ℕ
⊢ IsOpen[m n] (s n)

Tactic:
exact m_open n
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
⊢ IsOpen[t'] (⋃ (n : ℕ), s n)

Tactic:
have A : IsOpen[t'] (⋃ n, s n) := by
    apply isOpen_iUnion
    intro n
    apply t'm n
    exact m_open n
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
A : IsOpen[t'] (⋃ (n : ℕ), s n)
⊢ ∃ t'' ≤ t', PolishSpace α ∧ IsClosed.{u_1} (X := α) (⋃ (n : ℕ), s n) ∧ IsOpen.{u_1} (X := α) (⋃ (n : ℕ), s n)

Tactic:
@IsOpen.isClopenable α t' t'_polish _ A

Premises used: IsOpen.isClopenable, PolishSpace.IsClopenable
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
A : IsOpen[t'] (⋃ (n : ℕ), s n)
obtain :
  ∀ (t'' : TopologicalSpace α) (t''_le : t'' ≤ t') (t''_polish : PolishSpace α)
    (h1 : IsClosed.{u_1} (X := α) (⋃ (n : ℕ), s n)) (h2 : IsOpen.{u_1} (X := α) (⋃ (n : ℕ), s n)),
    IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)

Tactic:
obtain ⟨t'', t''_le, t''_polish, h1, h2⟩ : ∃ t'' : TopologicalSpace α,
      t'' ≤ t' ∧ @PolishSpace α t'' ∧ IsClosed[t''] (⋃ n, s n) ∧ IsOpen[t''] (⋃ n, s n) :=
    @IsOpen.isClopenable α t' t'_polish _ A

Premises used: IsOpen.isClopenable, TopologicalSpace
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
A : IsOpen[t'] (⋃ (n : ℕ), s n)
t'' : TopologicalSpace α
t''_le : t'' ≤ t'
t''_polish : PolishSpace α
h1 : IsClosed[t''] (⋃ (n : ℕ), s n)
h2 : IsOpen[t''] (⋃ (n : ℕ), s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)

Tactic:
⟨t'', t''_le.trans ((t'm 0).trans (mt 0)), t''_polish, h1, h2⟩

Premises used: PolishSpace.IsClopenable, And.intro, Exists.intro, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
A : IsOpen[t'] (⋃ (n : ℕ), s n)
t'' : TopologicalSpace α
t''_le : t'' ≤ t'
t''_polish : PolishSpace α
h1 : IsClosed[t''] (⋃ (n : ℕ), s n)
h2 : IsOpen[t''] (⋃ (n : ℕ), s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)

Tactic:
exact ⟨t'', t''_le.trans ((t'm 0).trans (mt 0)), t''_polish, h1, h2⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
inl : ∀ (hs : IsClosed.{u_1} (X := α) ∅) (h : ∅ ⊆ ball x r), ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'
inr : ∀ (hne : s.Nonempty), ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
hr : 0 < r
hs : IsClosed.{u_1} (X := α) ∅
h : ∅ ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'

Tactic:
⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩

Premises used: half_lt_self, half_pos, HDiv.hDiv, And.intro, Set.empty_subset, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
hr : 0 < r
hs : IsClosed.{u_1} (X := α) ∅
h : ∅ ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'

Tactic:
exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
⊢ IsCompact s

Tactic:
have : IsCompact s :=
    (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall)
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
⊢ ContinuousOn (Y := ℝ) (fun (y : α) ↦ dist y x) s

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
inr : ∀ (y : α) (hys : y ∈ s) (hy : s ⊆ closedBall x (dist y x)), ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
    this.exists_isMaxOn (β := α) (α := ℝ) hne (by fun_prop)

Premises used: IsCompact.exists_isMaxOn
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ dist y x < r

Tactic:
have hyr : dist y x < r := h hys
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
inr : ∀ (r' : ℝ) (hyr' : dist y x < r') (hrr' : r' < r), ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
rcases exists_between hyr with ⟨r', hyr', hrr'⟩

Premises used: exists_between
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
r' : ℝ
hyr' : dist y x < r'
hrr' : r' < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩

Premises used: dist_nonneg, Metric.closedBall_subset_ball, HasSubset.Subset.trans, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
r' : ℝ
hyr' : dist y x < r'
hrr' : r' < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
inl : ∀ (hr : r ≤ 0), ∃ r' < r, s ⊆ ball x r'
inr : ∀ (hr : 0 < r), ∃ r' < r, s ⊆ ball x r'
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
rcases le_or_gt r 0 with hr | hr

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ s = ∅

Tactic:
rw [ball_eq_empty.2 hr, subset_empty_iff] at h

Premises used: Iff.mpr, Metric.ball_eq_empty, Set.subset_empty_iff
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
h₁ : s = ∅
⊢ r ≤ 0

Tactic:
rw [ball_eq_empty.2 hr, subset_empty_iff] at h

Premises used: Iff.mpr, Metric.ball_eq_empty, Set.subset_empty_iff
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
inl : ∀ (hs : IsClosed.{u_1} (X := α) ∅), ∃ r' < r, ∅ ⊆ ball x r'
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
subst s
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed.{u_1} (X := α) ∅
⊢ ∃ r' < r, ∅ ⊆ ball x r'

Tactic:
(exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩

Premises used: Metric.ball, Exists.imp, And.intro, Set.empty_subset, NoMinOrder.exists_lt
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed.{u_1} (X := α) ∅
⊢ ∃ r' < r, ∅ ⊆ ball x r'

Tactic:
exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩

Premises used: Exists.imp, NoMinOrder.exists_lt
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : 0 < r
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
(exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩

Premises used: exists_pos_lt_subset_ball, Exists.imp, And.intro
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : 0 < r
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩

Premises used: exists_pos_lt_subset_ball, Exists.imp
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inst_2 : TopologicalSpace β
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ sphere a r, f z < f z'
⊢ ∀ z' ∈ closedBall a r \ ball a r, f z < f z'

Tactic:
simp_rw [← closedBall_diff_ball] at hf1

Premises used: Metric.closedBall_diff_ball