awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
    LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
H : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R)
⊢ ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)

Tactic:
⟨i, hi, H⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
    LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
H : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R)
⊢ ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)

Tactic:
exact ⟨i, hi, H⟩
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
    LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
H : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
⊢ ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)

Tactic:
⟨i, hi, H⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
    LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
H : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
⊢ ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)

Tactic:
exact ⟨i, hi, H⟩
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Add R
inst_1 : Zero R
inst_2 : Preorder R
d : PseudoMetric X R
ε : R
⊢ ∀ (a b : X),
    Membership.mem (γ := SetRel X X) {xy : X × X | (d : (a : X) → X → R) xy.1 xy.2 < ε} (a, b) →
      Membership.mem (γ := SetRel X X) {xy : X × X | (d : (a : X) → X → R) xy.1 xy.2 < ε} (b, a)

Tactic:
simp [d.symm]

Premises used: PseudoMetric.symm
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Add R
inst_1 : Zero R
inst_2 : LE R
d : PseudoMetric X R
ε : R
⊢ ∀ (a b : X),
    Membership.mem (γ := SetRel X X) {xy : X × X | (d : (a : X) → X → R) xy.1 xy.2 ≤ ε} (a, b) →
      Membership.mem (γ := SetRel X X) {xy : X × X | (d : (a : X) → X → R) xy.1 xy.2 ≤ ε} (b, a)

Tactic:
simp [d.symm]

Premises used: PseudoMetric.symm
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
n : ℕ
⊢ Membership.mem (γ := Set α) (⋂ (n : ℕ), A (res (↑x : ℕ → β) n))
    (Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) ⋯)

Tactic:
have := x.property.some_mem
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
n : ℕ
this :
  Membership.mem (γ := Set α) (⋂ (n : ℕ), A (res (↑x : ℕ → β) n))
    (Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) ⋯)
⊢ ∀ (i : ℕ), Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) ⋯ ∈ A (res (↑x : ℕ → β) i)

Tactic:
rw [mem_iInter] at this

Premises used: Set.mem_iInter
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) ⋯ ∈ A (res (↑x : ℕ → β) i)
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A (res (↑x : ℕ → β) n)

Tactic:
this n

Premises used: Set.Mem, Classical.choose, Set.Nonempty.some
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) ⋯ ∈ A (res (↑x : ℕ → β) i)
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A (res (↑x : ℕ → β) n)

Tactic:
exact this n
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : TopologicalSpace α
hA : ClosureAntitone A
⊢ CantorScheme.Antitone A

Tactic:
fun l a => subset_closure.trans (hA l a)

Premises used: subset_closure, CantorScheme.Antitone, HasSubset.Subset.trans
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : TopologicalSpace α
hanti : CantorScheme.Antitone A
hclosed : ∀ (l : List β), IsClosed[inst] (A l)
⊢ ClosureAntitone A

Tactic:
fun _ _ =>
  (hclosed _).closure_eq.subset.trans (hanti _ _)

Premises used: CantorScheme.ClosureAntitone, IsClosed.closure_eq, HasSubset.Subset.trans, List.cons, Eq.subset
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
a : (↑x : ℕ → β) = (↑y : ℕ → β)
⊢ x = y

Tactic:
ext1
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
a : res (↑x : ℕ → β) = res (↑y : ℕ → β)
⊢ (↑x : ℕ → β) = (↑y : ℕ → β)

Tactic:
apply res_injective

Premises used: PiNat.res_injective
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
a : ∀ (n : ℕ), res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
⊢ res (↑x : ℕ → β) = res (↑y : ℕ → β)

Tactic:
ext n : 1
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
⊢ res (↑x : ℕ → β) 0 = res (↑y : ℕ → β) 0

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
a : (↑x : ℕ → β) n = (↑y : ℕ → β) n ∧ res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
⊢ res (↑x : ℕ → β) (n + 1) = res (↑y : ℕ → β) (n + 1)

Tactic:
simp only [res_succ, cons.injEq]

Premises used: List.cons.injEq, PiNat.res_succ
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
⊢ (↑x : ℕ → β) n = (↑y : ℕ → β) n ∧ res (↑x : ℕ → β) n = res (↑y : ℕ → β) n

Tactic:
⟨?_, ih⟩

Premises used: And.intro
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
a : (↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ (↑x : ℕ → β) n = (↑y : ℕ → β) n ∧ res (↑x : ℕ → β) n = res (↑y : ℕ → β) n

Tactic:
refine ⟨?_, ih⟩
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
a : ∀ (hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n), ¬CantorScheme.Disjoint A
⊢ (↑x : ℕ → β) n = (↑y : ℕ → β) n

Tactic:
contrapose hA
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
a : ∃ (x : List β) (x_1 : β) (x_2 : β), ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
⊢ ¬CantorScheme.Disjoint A

Tactic:
simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]

Premises used: Ne, exists_prop, Pairwise, CantorScheme.Disjoint, Classical.not_forall
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ ∃ (x : List β) (x_1 : β) (x_2 : β), ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))

Tactic:
⟨res x n, _, _, hA, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, PiNat.res
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
a : ¬_root_.Disjoint (A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n)) (A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n))
⊢ ∃ (x : List β) (x_1 : β) (x_2 : β), ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))

Tactic:
refine ⟨res x n, _, _, hA, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
a : ∃ x_1 ∈ A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n), x_1 ∈ A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n)
⊢ ¬_root_.Disjoint (A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n)) (A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n))

Tactic:
rw [not_disjoint_iff]

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ ∃ x_1 ∈ A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n), x_1 ∈ A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n)

Tactic:
⟨(inducedMap A).2 x, ?_, ?_⟩

Premises used: CantorScheme.inducedMap, And.intro, Exists.intro, Sigma.snd
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
a : (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n)
a₁ : (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n)
⊢ ∃ x_1 ∈ A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n), x_1 ∈ A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n)

Tactic:
refine ⟨(inducedMap A).2 x, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
a : (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A (res (↑x : ℕ → β) n.succ)
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n)

Tactic:
rw [← res_succ]

Premises used: PiNat.res_succ
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A (res (↑x : ℕ → β) n.succ)

Tactic:
apply map_mem

Premises used: CantorScheme.map_mem
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
a : (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y ∈ A (res (↑y : ℕ → β) n.succ)
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n)

Tactic:
rw [hxy, ih, ← res_succ]

Premises used: PiNat.res_succ
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y ∈ A (res (↑y : ℕ → β) n.succ)

Tactic:
apply map_mem

Premises used: CantorScheme.map_mem
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
a : res (↑x : ℕ → β) 0 = res (↑y : ℕ → β) 0
a₁ : ∀ (n : ℕ) (ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n), res (↑x : ℕ → β) (n + 1) = res (↑y : ℕ → β) (n + 1)
⊢ res (↑x : ℕ → β) n = res (↑y : ℕ → β) n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp only [res_succ, cons.injEq]
    refine ⟨?_, ih⟩
    contrapose hA
    simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]
    refine ⟨res x n, _, _, hA, ?_⟩
    rw [not_disjoint_iff]
    refine ⟨(inducedMap A).2 x, ?_, ?_⟩
    · rw [← res_succ]
      apply map_mem
    rw [hxy, ih, ← res_succ]
    apply map_mem

Premises used: Ne, CantorScheme.map_mem, exists_prop, Set.not_disjoint_iff, List.cons.injEq, Pairwise, CantorScheme.Disjoint, PiNat.res_succ, Classical.not_forall
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
hA : VanishingDiam A
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
⊢ Tendsto (β := ENNReal) (fun (n : ℕ) ↦ Metric.ediam (A (res x n))) atTop (𝓝 0)

Tactic:
specialize hA x
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : Tendsto (β := ENNReal) (fun (n : ℕ) ↦ Metric.ediam (A (res x n))) atTop (𝓝 0)
⊢ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hA

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
simp : 0 < ε / 2
⊢ ENNReal.ofReal (ε / 2) > 0

Tactic:
simp only [gt_iff_lt, ENNReal.ofReal_pos]

Premises used: ENNReal.ofReal_pos, gt_iff_lt
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
linarith : ε / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε / 2 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 < ε / 2

Tactic:
linarith
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
obtain :
  ∀ (n : ℕ) (hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)),
    ∃ (n : ℕ), ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∃ (n : ℕ), ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε

Tactic:
obtain ⟨n, hn⟩ := hA (ENNReal.ofReal (ε / 2)) (by
    simp only [gt_iff_lt, ENNReal.ofReal_pos]; linarith)

Premises used: ENNReal.ofReal, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
h : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∃ (n : ℕ), ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε

Tactic:
use n
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
h : edist y z < ENNReal.ofReal ε
⊢ dist y z < ε

Tactic:
rw [← ENNReal.ofReal_lt_ofReal_iff ε_pos, ← edist_dist]

Premises used: edist_dist, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
h : Metric.ediam (A (res x n)) < ENNReal.ofReal ε
⊢ edist y z < ENNReal.ofReal ε

Tactic:
apply lt_of_le_of_lt (Metric.edist_le_ediam_of_mem hy hz)

Premises used: lt_of_le_of_lt, Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
h : ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε
⊢ Metric.ediam (A (res x n)) < ENNReal.ofReal ε

Tactic:
apply lt_of_le_of_lt (hn _ (le_refl _))

Premises used: lt_of_le_of_lt, le_refl
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
h : ε / 2 < ε
⊢ ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε

Tactic:
rw [ENNReal.ofReal_lt_ofReal_iff ε_pos]

Premises used: ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
linarith : ε ≤ ε / 2 → 2 / 2 = 1
linarith₁ : ε ≤ ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε ≤ ε / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : ε ≤ ε / 2 → 0 - ε + (2 * ε - 1 * ε) = 0
⊢ ε / 2 < ε

Tactic:
linarith