awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
⟨fun x => (inducedMap D).2 ⟨x, hdom⟩, ?_, ?_, ?_⟩

Premises used: Subtype.mk, CantorScheme.inducedMap, And.intro, Exists.intro, Sigma.snd
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
refine_1 :
  (range fun (x : ℕ → Bool) ↦
      (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
        (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α))
          x ⋯)) ⊆
    C
refine_2 :
  Continuous.{0, u_1} (Y := α) fun (x : ℕ → Bool) ↦
    (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
      (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x
        ⋯)
refine_3 :
  Injective.{1, u_1 + 1} (β := α) fun (x : ℕ → Bool) ↦
    (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
      (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x
        ⋯)
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
refine ⟨fun x => (inducedMap D).2 ⟨x, hdom⟩, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
x : ℕ → Bool
⊢ (fun (x : ℕ → Bool) ↦
        (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
          (Subtype.mk (p := fun (x : ℕ → Bool) ↦
            x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x ⋯))
      x ∈
    C

Tactic:
map_mem ⟨_, hdom⟩ 0

Premises used: Set.Mem, CantorScheme.map_mem, Subtype.mk, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
x : ℕ → Bool
⊢ (fun (x : ℕ → Bool) ↦
        (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
          (Subtype.mk (p := fun (x : ℕ → Bool) ↦
            x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x ⋯))
      x ∈
    C

Tactic:
exact map_mem ⟨_, hdom⟩ 0

Premises used: CantorScheme.map_mem, Subtype.mk, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
refine_2 :
  Continuous (Y := (↑((inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) : Type))
    fun (x : ℕ → Bool) ↦
    Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x ⋯
⊢ Continuous.{0, u_1} (Y := α) fun (x : ℕ → Bool) ↦
    (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
      (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x
        ⋯)

Tactic:
apply hdiam.map_continuous.comp

Premises used: Continuous.comp, CantorScheme.VanishingDiam.map_continuous
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
⊢ Continuous (Y := (↑((inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) : Type))
    fun (x : ℕ → Bool) ↦
    Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
x y : ℕ → Bool
hxy :
  Eq.{u_1 + 1} (α := α)
    ((fun (x : ℕ → Bool) ↦
        (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
          (Subtype.mk (p := fun (x : ℕ → Bool) ↦
            x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x ⋯))
      x)
    ((fun (x : ℕ → Bool) ↦
        (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
          (Subtype.mk (p := fun (x : ℕ → Bool) ↦
            x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x ⋯))
      y)
⊢ x = y

Tactic:
simpa only [← Subtype.val_inj] using hdisj'.map_injective hxy

Premises used: Subtype.val_inj, CantorScheme.Disjoint.map_injective
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
obtain :
  ∀ (D : Set α) (hD : Perfect D) (Dnonempty : D.Nonempty) (hDC : D ⊆ C),
    ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc

Premises used: exists_perfect_nonempty_of_isClosed_of_not_countable
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
obtain :
  ∀ (f : (ℕ → Bool) → α) (hfD : range f ⊆ D) (hf : Continuous f ∧ Injective f),
    ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty

Premises used: Perfect.exists_nat_bool_injection
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Injective f
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
⟨f, hfD.trans hDC, hf⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Injective f
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
exact ⟨f, hfD.trans hDC, hf⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
rw :
  Ne (α := E (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯)) (x (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))
    (y (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))
⊢ Ne (α := E (firstDiff (E := E) x y)) (x (firstDiff (E := E) x y)) (y (firstDiff (E := E) x y))

Tactic:
rw [firstDiff_def, dif_pos h]

Premises used: PiNat.firstDiff_def, dif_pos
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ Ne (α := E (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯)) (x (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))
    (y (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))

Tactic:
Nat.find_spec (ne_iff.1 h)

Premises used: Function.ne_iff, Iff.mp, Nat.find_spec
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ Ne (α := E (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯)) (x (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))
    (y (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))

Tactic:
exact Nat.find_spec (ne_iff.1 h)

Premises used: Function.ne_iff, Iff.mp, Nat.find_spec
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ Ne (α := E (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯)) (x (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))
    (y (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯))

Tactic:
classical
  exact Nat.find_spec (ne_iff.1 h)
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < firstDiff (E := E) x y
⊢ n < if h : x ≠ y then Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯ else 0

Tactic:
rw [firstDiff_def] at hn

Premises used: PiNat.firstDiff_def
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < if h : x ≠ y then Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) ⋯ else 0
⊢ x n = y n

Tactic:
aesop
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ firstDiff (E := E) x y = firstDiff (E := E) y x

Tactic:
simp only [firstDiff_def, ne_comm]

Premises used: PiNat.firstDiff_def, ne_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ firstDiff (E := E) x y = firstDiff (E := E) y x

Tactic:
classical
  simp only [firstDiff_def, ne_comm]

Premises used: PiNat.firstDiff_def, ne_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
by_contra! : ∀ (H : firstDiff (E := E) x z < min (firstDiff (E := E) x y) (firstDiff (E := E) y z)), False
⊢ min (firstDiff (E := E) x y) (firstDiff (E := E) y z) ≤ firstDiff (E := E) x z

Tactic:
by_contra! H
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff (E := E) x z < min (firstDiff (E := E) x y) (firstDiff (E := E) y z)
⊢ firstDiff (E := E) x z < firstDiff (E := E) x y ∧ firstDiff (E := E) x z < firstDiff (E := E) y z

Tactic:
rw [lt_min_iff] at H

Premises used: lt_min_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff (E := E) x z < firstDiff (E := E) x y ∧ firstDiff (E := E) x z < firstDiff (E := E) y z
⊢ False

Tactic:
apply_firstDiff_ne h ?_

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff (E := E) x z < firstDiff (E := E) x y ∧ firstDiff (E := E) x z < firstDiff (E := E) y z
refine : Eq (α := E (firstDiff (E := E) x z)) (x (firstDiff (E := E) x z)) (z (firstDiff (E := E) x z))
⊢ False

Tactic:
refine apply_firstDiff_ne h ?_

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff (E := E) x z < firstDiff (E := E) x y ∧ firstDiff (E := E) x z < firstDiff (E := E) y z
⊢ Eq (α := E (firstDiff (E := E) x z)) (x (firstDiff (E := E) x z)) (y (firstDiff (E := E) x z))

Tactic:
apply_eq_of_lt_firstDiff H.1

Premises used: And.left, PiNat.apply_eq_of_lt_firstDiff