awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g

Tactic:
continuous_iff_continuousAt.2 fun y => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
refine : ∀ (y : (↑s : Type)), ContinuousAt g y
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g

Tactic:
refine continuous_iff_continuousAt.2 fun y => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y : (↑s : Type)
⊢ ContinuousAt g y

Tactic:
continuousAt_of_locally_lipschitz zero_lt_one 4 fun x hxy => ?_

Premises used: continuousAt_of_locally_lipschitz, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y : (↑s : Type)
refine : ∀ (x : (↑s : Type)) (hxy : dist x y < 1), dist (g x) (g y) ≤ 4 * dist x y
⊢ ContinuousAt g y

Tactic:
refine continuousAt_of_locally_lipschitz zero_lt_one 4 fun x hxy => ?_

Premises used: continuousAt_of_locally_lipschitz, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
inl : ∀ (hxy : dist x x < 1), dist (g x) (g x) ≤ 4 * dist x x
inr : ∀ (hne : x ≠ y), dist (g x) (g y) ≤ 4 * dist x y
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
rcases eq_or_ne x y with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
x : (↑s : Type)
hxy : dist x x < 1
⊢ dist (g x) (g x) ≤ 4 * dist x x

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
⊢ (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)

Tactic:
have hne' : x.1 ≠ y.1 := Subtype.coe_injective.ne hne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
⊢ dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)

Tactic:
have dist' : dist x y = dist x.1 y.1 := rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
by_contra! : ∀ (h : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) ≤ 0), False
⊢ 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)

Tactic:
by_contra! h
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
h : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) ≤ 0
apply :
  (↑x : ℕ → ℕ) (firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)) =
    (↑y : ℕ → ℕ) (firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ))
⊢ False

Tactic:
apply apply_firstDiff_ne hne'

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
h : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) ≤ 0
rw : (↑x : ℕ → ℕ) 0 = (↑y : ℕ → ℕ) 0
⊢ (↑x : ℕ → ℕ) (firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)) =
    (↑y : ℕ → ℕ) (firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ))

Tactic:
rw [Nat.le_zero.1 h]

Premises used: Nat.le_zero, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
h : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) ≤ 0
apply : dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) < HPow.hPow (β := ℕ) (1 / 2) 0
⊢ (↑x : ℕ → ℕ) 0 = (↑y : ℕ → ℕ) 0

Tactic:
apply apply_eq_of_dist_lt _ le_rfl

Premises used: PiNat.apply_eq_of_dist_lt, le_rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
h : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) ≤ 0
⊢ dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) < 1

Tactic:
hxy
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
h : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) ≤ 0
⊢ dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) < 1

Tactic:
exact hxy
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
⊢ 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)

Tactic:
have diff_pos : 0 < firstDiff x.1 y.1 := by
      by_contra! h
      apply apply_firstDiff_ne hne'
      rw [Nat.le_zero.1 h]
      apply apply_eq_of_dist_lt _ le_rfl
      rw [pow_zero]
      exact hxy
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
⊢ firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1

Tactic:
have hn : firstDiff x.1 y.1 = n + 1 := (Nat.succ_pred_eq_of_pos diff_pos).symm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
inr : dist (g x) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
rw [dist', dist_eq_of_ne hne', hn]

Premises used: PiNat.dist_eq_of_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
⊢ (↑x : ℕ → ℕ) n = (↑y : ℕ → ℕ) n

Tactic:
have B : x.1 n = y.1 n := mem_cylinder_firstDiff x.1 y.1 n (Nat.pred_lt diff_pos.ne')
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
B : (↑x : ℕ → ℕ) n = (↑y : ℕ → ℕ) n
⊢ dist (g x) (g y) ≤ dist (g x) (u ((↑x : ℕ → ℕ) n)) + dist (g y) (u ((↑x : ℕ → ℕ) n))

Tactic:
dist_triangle_right _ _ _

Premises used: dist_triangle_right
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
B : (↑x : ℕ → ℕ) n = (↑y : ℕ → ℕ) n
rw rw₁ :
  dist (g x) (u ((↑x : ℕ → ℕ) n)) + dist (g y) (u ((↑x : ℕ → ℕ) n)) =
    dist (g x) (u ((↑x : ℕ → ℕ) n)) + dist (g y) (u ((↑x : ℕ → ℕ) n))
⊢ dist (g x) (u ((↑x : ℕ → ℕ) n)) + dist (g y) (u ((↑x : ℕ → ℕ) n)) =
    dist (g x) (u ((↑x : ℕ → ℕ) n)) + dist (g y) (u ((↑y : ℕ → ℕ) n))

Tactic:
rw [← B]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
B : (↑x : ℕ → ℕ) n = (↑y : ℕ → ℕ) n
⊢ dist (g x) (u ((↑x : ℕ → ℕ) n)) + dist (g y) (u ((↑y : ℕ → ℕ) n)) ≤ (1 / 2) ^ n + (1 / 2) ^ n

Tactic:
add_le_add (A x n) (A y n)

Premises used: add_le_add
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : dist x y = dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
B : (↑x : ℕ → ℕ) n = (↑y : ℕ → ℕ) n
⊢ (1 / 2) ^ n + (1 / 2) ^ n = 4 * (1 / 2) ^ (n + 1)

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), Dist.dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
y x : (↑s : Type)
hxy : Dist.dist x y < 1
hne : x ≠ y
hne' : (↑x : ℕ → ℕ) ≠ (↑y : ℕ → ℕ)
dist' : Dist.dist x y = Dist.dist (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
n : ℕ := firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) - 1
diff_pos : 0 < firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ)
hn : firstDiff (E := fun (n : ℕ) ↦ ℕ) (↑x : ℕ → ℕ) (↑y : ℕ → ℕ) = n + 1
B : (↑x : ℕ → ℕ) n = (↑y : ℕ → ℕ) n
dist :
  Dist.dist (g x) (u ((↑x : ℕ → ℕ) n)) + Dist.dist (g y) (u ((↑x : ℕ → ℕ) n)) =
    Dist.dist (g x) (u ((↑x : ℕ → ℕ) n)) + Dist.dist (g y) (u ((↑y : ℕ → ℕ) n))
dist₁ : (1 / 2) ^ n + (1 / 2) ^ n = 4 * (1 / 2) ^ (n + 1)
⊢ Dist.dist (g x) (g y) ≤ 4 * (1 / 2) ^ (n + 1)

Tactic:
calc
      dist (g x) (g y) ≤ dist (g x) (u (x.1 n)) + dist (g y) (u (x.1 n)) :=
        dist_triangle_right _ _ _
      _ = dist (g x) (u (x.1 n)) + dist (g y) (u (y.1 n)) := by rw [← B]
      _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := add_le_add (A x n) (A y n)
      _ = 4 * (1 / 2) ^ (n + 1) := by ring

Premises used: add_le_add, dist_triangle_right, HDiv.hDiv, HAdd.hAdd, Dist.dist, OfNat.ofNat, Subtype.val