awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j : ι // j ∉ K }), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι)) < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * (↑K.card : ℝ≥0∞) < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), EDist.edist (x x_1) (y x_1) < δ
edist :
  HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (EDist.edist (x i) (y i)))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)),
        min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) (EDist.edist (α := F (↑i : ι)) (x (↑i : ι)) (y (↑i : ι)))) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, EDist.edist (x i) (y i))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι)))
edist₁ :
  HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, EDist.edist (x i) (y i))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) <
    ∑ _i ∈ K, δ + ε / 2
edist₂ : ∑ _i ∈ K, δ + ε / 2 ≤ ε / 2 + ε / 2
⊢ Membership.mem (γ := Set (((i : ι) → F i) × ((i : ι) → F i)))
    {p : ((i : ι) → F i) × ((i : ι) → F i) | EDist.edist p.1 p.2 < ε} (x, y)

Tactic:
calc
          edist x y = ∑' i : ι, min (2⁻¹ ^ encode i) (edist (x i) (y i)) := rfl
          _ = ∑ i ∈ K, min (2⁻¹ ^ encode i) (edist (x i) (y i)) +
                ∑' i : ↑(K : Set ι)ᶜ, min (2⁻¹ ^ encode (i : ι)) (edist (x i) (y i)) :=
            (ENNReal.sum_add_tsum_compl ..).symm
          _ ≤ ∑ i ∈ K, edist (x i) (y i) + ∑' i : ↑(K : Set ι)ᶜ, 2⁻¹ ^ encode (i : ι) := by
            gcongr
            · apply min_le_right
            · apply min_le_left
          _ < ∑ _i ∈ K, δ + ε / 2 := by
            refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le
          _ ≤ ε / 2 + ε / 2 := by gcongr; simpa [mul_comm] using hδ.le
          _ = ε := ENNReal.add_halves _

Premises used: SetLike.coe, ENNReal.sum_add_tsum_compl, ENNReal.add_halves, EDist.edist, Eq.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
⊢ 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)

Tactic:
have : (0 : ℝ≥0∞) < 2⁻¹ ^ encode i := ENNReal.pow_pos (by norm_num) _
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
⊢ 0 < min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) ε

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
right :
  Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (𝓟 {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) ε})
    {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < ε}
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : 0 < ε), 𝓟 {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε})
    {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < ε}

Tactic:
refine mem_iInf_of_mem (min (2⁻¹ ^ encode i) ε) <| mem_iInf_of_mem (by positivity) ?_

Premises used: Filter.mem_iInf_of_mem, Inv.inv, HPow.hPow, Encodable.encode, OfNat.ofNat, Min.min
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
right :
  ∀ (a b : (i : ι) → F i), edist a b < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i) → edist a b < ε → edist (a i) (b i) < ε
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (𝓟 {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) ε})
    {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < ε}

Tactic:
simp only [and_imp, Prod.forall, setOf_subset_setOf, lt_min_iff, mem_principal]

Premises used: and_imp, Filter.mem_principal, Set.setOf_subset_setOf, Prod.forall, lt_min_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
x y : (i : ι) → F i
hn : edist x y < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
⊢ edist x y < ε → edist (x i) (y i) < ε

Tactic:
(edist_le_edist_pi_of_edist_lt hn).trans_lt

Premises used: PiCountable.edist_le_edist_pi_of_edist_lt, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
x y : (i : ι) → F i
hn : edist x y < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
⊢ edist x y < ε → edist (x i) (y i) < ε

Tactic:
exact (edist_le_edist_pi_of_edist_lt hn).trans_lt

Premises used: PiCountable.edist_le_edist_pi_of_edist_lt, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EMetricSpace (F i)
⊢ ∀ {x y : (i : ι) → F i}, edist x y = 0 → x = y

Tactic:
simp [edist_eq_tsum, funext_iff]

Premises used: PiCountable.edist_eq_tsum, funext_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
⊢ dist x y = ∑' (i : ι), min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (x i) (y i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
⊢ Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) 2⁻¹ (encode i)

Tactic:
simpa [one_div] using summable_geometric_two_encode

Premises used: one_div, summable_geometric_two_encode
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
refine : ∀ (i : ι), 0 ≤ min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (x i) (y i))
⊢ Summable (α := ℝ) fun (i : ι) ↦ min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (x i) (y i))

Tactic:
refine .of_nonneg_of_le (fun i => ?_) (fun i => min_le_left _ _) <| by
    simpa [one_div] using summable_geometric_two_encode
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ HPow.hPow (α := ℝ) 2⁻¹ (encode i)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (x i) (y i))

Tactic:
exact le_min (by positivity) dist_nonneg

Premises used: dist_nonneg, le_min
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i j : ι
h : j ≠ i
⊢ 0 ≤ HPow.hPow (α := ℝ) 2⁻¹ (encode j)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i : ι
h : dist x y < HPow.hPow (α := ℝ) 2⁻¹ (encode i)
⊢ dist (x i) (y i) ≤ dist x y

Tactic:
simpa only [not_le.2 h, false_or] using min_le_iff.1 (min_dist_le_dist_pi x y i)

Premises used: not_le, Iff.mpr, PiCountable.min_dist_le_dist_pi, min_le_iff, false_or, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
simp : LE.le (α := ℝ) 0 (∑' (i : ι), min (HPow.hPow (α := ℝ) 2 (encode i))⁻¹ (dist (x i) (y i)))
⊢ 0 ≤ dist x y

Tactic:
simp [dist_eq_tsum]

Premises used: PiCountable.dist_eq_tsum
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ LE.le (α := ℝ) 0 (∑' (i : ι), min (HPow.hPow (α := ℝ) 2 (encode i))⁻¹ (dist (x i) (y i)))

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
x_2 : ι
⊢ 0 ≤ min (HPow.hPow (α := ℝ) 2⁻¹ (encode x_2)) (dist (x x_2) (y x_2))

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
rw :
  Eq (α := ℝ≥0∞) (∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)))
    (∑' (n : ι), ENNReal.ofReal (min (HPow.hPow (α := ℝ) 2⁻¹ (encode n)) (dist (x n) (y n))))
⊢ edist x y = ENNReal.ofReal (dist x y)

Tactic:
rw [edist_eq_tsum, dist_eq_tsum,
        ENNReal.ofReal_tsum_of_nonneg (fun _ ↦ by positivity) (dist_summable ..)]

Premises used: PiCountable.edist_eq_tsum, ENNReal.ofReal_tsum_of_nonneg, PiCountable.dist_summable, PiCountable.dist_eq_tsum
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
simp :
  Eq (α := ℝ≥0∞) (∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (PseudoMetricSpace.edist (x i) (y i)))
    (∑' (n : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (ENNReal.ofReal (dist (x n) (y n))))
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)))
    (∑' (n : ι), ENNReal.ofReal (min (HPow.hPow (α := ℝ) 2⁻¹ (encode n)) (dist (x n) (y n))))

Tactic:
simp [edist, ENNReal.inv_pow]

Premises used: EDist.edist, ENNReal.inv_pow
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
h : ∀ (a : ι), PseudoMetricSpace.edist (x a) (y a) = ENNReal.ofReal (dist (x a) (y a))
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (PseudoMetricSpace.edist (x i) (y i)))
    (∑' (n : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (ENNReal.ofReal (dist (x n) (y n))))

Tactic:
congr! with a
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
a : ι
⊢ PseudoMetricSpace.edist (x a) (y a) = ENNReal.ofReal (dist (x a) (y a))

Tactic:
PseudoMetricSpace.edist_dist (x a) (y a)

Premises used: PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → PseudoMetricSpace (F i)
x_1 y_1 : (i : ι) → F i
i : ι
x y : (i : ι) → F i
a : ι
⊢ PseudoMetricSpace.edist (x a) (y a) = ENNReal.ofReal (dist (x a) (y a))

Tactic:
exact PseudoMetricSpace.edist_dist (x a) (y a)

Premises used: PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → MetricSpace (F i)
⊢ ∀ (x y : (i : ι) → F i), 0 ≤ dist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → MetricSpace (F i)
⊢ ∀ (x y : (i : ι) → F i), edist x y = ENNReal.ofReal (dist x y)

Tactic:
simp [edist_dist]

Premises used: edist_dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
x y : PiNatEmbed X Y f
hxy : x.ofPiNat (Y := Y) = y.ofPiNat (Y := Y)
toPiNat :
  ∀ (ofPiNat : X)
    (hxy : PiNatEmbed.ofPiNat (Y := Y) (f := f) (PiNatEmbed.toPiNat (Y := Y) ofPiNat) = y.ofPiNat (Y := Y)),
    PiNatEmbed.toPiNat (Y := Y) ofPiNat = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
y : PiNatEmbed X Y f
ofPiNat : X
hxy : PiNatEmbed.ofPiNat (Y := Y) (f := f) (toPiNat (Y := Y) ofPiNat) = y.ofPiNat (Y := Y)
⊢ toPiNat (Y := Y) ofPiNat = y

Tactic:
congr!
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
x y : PiNatEmbed X Y f
⊢ x.ofPiNat (Y := Y) = y.ofPiNat (Y := Y) ↔ x = y

Tactic:
(toPiNatEquiv X Y f).symm.injective.eq_iff

Premises used: Metric.PiNatEmbed.toPiNatEquiv, Function.Injective.eq_iff, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
P : PiNatEmbed X Y f → Prop
⊢ (∀ (x : PiNatEmbed X Y f), P x) ↔ ∀ (x : X), P (toPiNat (Y := Y) x)

Tactic:
(toPiNatEquiv X Y f).symm.forall_congr_left

Premises used: Metric.PiNatEmbed.toPiNatEquiv, Equiv.forall_congr_left, Equiv.symm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
⊢ Injective (embed X Y f)

Tactic:
simpa [Pairwise, not_imp_comm (a := _ = _), funext_iff, Function.Injective] using separating_f

Premises used: not_imp_comm, funext_iff, Pairwise, Function.Injective
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoEMetricSpace (Y i)
x y : PiNatEmbed X Y f
⊢ edist x y =
    ∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (f i (x.ofPiNat (Y := Y))) (f i (y.ofPiNat (Y := Y))))

Tactic:
rfl

Premises used: setOf, Metric.PiNatEmbed.embed, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoEMetricSpace (Y i)
⊢ Isometry (embed X Y f)

Tactic:
PseudoEMetricSpace.isometry_induced _

Premises used: PseudoEMetricSpace.isometry_induced
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoMetricSpace (Y i)
x y : PiNatEmbed X Y f
⊢ dist x y =
    ∑' (i : ι), min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (f i (x.ofPiNat (Y := Y))) (f i (y.ofPiNat (Y := Y))))

Tactic:
rfl

Premises used: Metric.PiNatEmbed.embed, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoMetricSpace (Y i)
inst_2 : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
rw :
  Continuous[instTopologicalSpaceProd, _] fun (x : X × X) ↦
    dist (α := PiNatEmbed X Y f) (toPiNat (Y := Y) x.1) (toPiNat (Y := Y) x.2)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (toPiNat (Y := Y))

Tactic:
rw [continuous_iff_continuous_dist]

Premises used: continuous_iff_continuous_dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoMetricSpace (Y i)
inst_2 : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
simp :
  Continuous[instTopologicalSpaceProd, _] fun (x : X × X) ↦
    ∑' (i : ι), min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (f i x.1) (f i x.2))
⊢ Continuous[instTopologicalSpaceProd, _] fun (x : X × X) ↦
    dist (α := PiNatEmbed X Y f) (toPiNat (Y := Y) x.1) (toPiNat (Y := Y) x.2)

Tactic:
simp only [dist_def]

Premises used: Metric.PiNatEmbed.dist_def
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoMetricSpace (Y i)
inst_2 : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ∀ (i : ι),
    Continuous[instTopologicalSpaceProd, _] fun (x : X × X) ↦
      min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (f i x.1) (f i x.2))

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoMetricSpace (Y i)
inst_2 : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ∀ (n : ι) (x : X × X), ‖min (HPow.hPow (α := ℝ) 2⁻¹ (encode n)) (dist (f n x.1) (f n x.2))‖ ≤ (1 / 2) ^ encode n

Tactic:
simp [abs_of_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → PseudoMetricSpace (Y i)
inst_2 : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[instTopologicalSpaceProd, _] fun (x : X × X) ↦
    ∑' (i : ι), min (HPow.hPow (α := ℝ) 2⁻¹ (encode i)) (dist (f i x.1) (f i x.2))

Tactic:
apply continuous_tsum (by fun_prop) summable_geometric_two_encode <| by simp [abs_of_nonneg]

Premises used: continuous_tsum, summable_geometric_two_encode
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → EMetricSpace (Y i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
⊢ IsUniformEmbedding (embed X Y f)

Tactic:
let := emetricSpace separating_f; isometry_embed.isUniformEmbedding

Premises used: Isometry.isUniformEmbedding, Metric.PiNatEmbed.emetricSpace
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → MetricSpace (Y i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
x y : PiNatEmbed X Y f
⊢ edist x y ≠ ∞

Tactic:
simp [edist_dist]

Premises used: edist_dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → MetricSpace (Y i)
inst_2 : TopologicalSpace X
inst_3 : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace (Y := Y) separating_f
rw :
  Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (toPiNat (Y := Y)) ∧
    Bijective.{u_3 + 1, u_3 + 1} (α := X) (β := PiNatEmbed X Y f) (toPiNat (Y := Y))
⊢ IsHomeomorph.{u_3, u_3} (X := X) (Y := PiNatEmbed X Y f) (toPiNat (Y := Y))

Tactic:
rw [isHomeomorph_iff_continuous_bijective]

Premises used: isHomeomorph_iff_continuous_bijective
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → MetricSpace (Y i)
inst_2 : TopologicalSpace X
inst_3 : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace (Y := Y) separating_f
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (toPiNat (Y := Y)) ∧
    Bijective.{u_3 + 1, u_3 + 1} (α := X) (β := PiNatEmbed X Y f) (toPiNat (Y := Y))

Tactic:
⟨continuous_toPiNat continuous_f, (toPiNatEquiv X Y f).bijective⟩

Premises used: Metric.PiNatEmbed.toPiNatEquiv, Equiv.bijective, Metric.PiNatEmbed.continuous_toPiNat, And.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → MetricSpace (Y i)
inst_2 : TopologicalSpace X
inst_3 : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace (Y := Y) separating_f
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (toPiNat (Y := Y)) ∧
    Bijective.{u_3 + 1, u_3 + 1} (α := X) (β := PiNatEmbed X Y f) (toPiNat (Y := Y))

Tactic:
exact ⟨continuous_toPiNat continuous_f, (toPiNatEquiv X Y f).bijective⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
inst : Encodable ι
inst_1 : (i : ι) → MetricSpace (Y i)
inst_2 : TopologicalSpace X
inst_3 : CompactSpace X
f : (i : ι) → X → Y i
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
⊢ MetrizableSpace X

Tactic:
letI := Metric.PiNatEmbed.metricSpace separating_f
  (Metric.PiNatEmbed.toPiNatHomeo X Y f continuous_f separating_f).isEmbedding.metrizableSpace

Premises used: Topology.IsEmbedding.metrizableSpace, Homeomorph.isEmbedding, Metric.PiNatEmbed.toPiNatHomeo
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
inl : IsEmpty X → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
inr : Nonempty X → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
cases isEmpty_or_nonempty X

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : IsEmpty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : IsEmpty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
exact continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
continuous_projIcc.comp <| Continuous.dist continuous_id' ?_

Premises used: Set.Mem, Continuous.comp, continuous_id', Set.projIcc, Continuous.dist, continuous_projIcc
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : Nonempty X
inr :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : X) ↦ denseSeq X n
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
refine continuous_projIcc.comp <| Continuous.dist continuous_id' ?_

Premises used: Continuous.comp, continuous_id', Continuous.dist, continuous_projIcc