awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EDist (F i)
x y : (i : ι) → F i
i : ι
⊢ min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)

Tactic:
min_le_left ..

Premises used: min_le_left
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EDist (F i)
x y : (i : ι) → F i
i : ι
⊢ min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)

Tactic:
exact min_le_left ..

Premises used: min_le_left
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EDist (F i)
x y : (i : ι) → F i
⊢ LT.lt (α := ℝ≥0∞) 2 ∞

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

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

Premises used: not_le, Iff.mpr, PiCountable.min_edist_le_edist_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 : ι) → PseudoEMetricSpace (F i)
x : (i : ι) → F i
⊢ edist x x = 0

Tactic:
simp [edist_eq_tsum]

Premises used: PiCountable.edist_eq_tsum
-- 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)
x y : (i : ι) → F i
⊢ edist x y = edist y x

Tactic:
simp [edist_eq_tsum, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, PiCountable.edist_eq_tsum
-- 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)
x y z : (i : ι) → F i
h :
  ∀ (n : ι),
    min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (z n)) ≤
      min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
        min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n))
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (z i)))
    (∑' (i : ι),
      (min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) +
        min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (y i) (z i))))

Tactic:
gcongr with n
-- 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)
x y z : (i : ι) → F i
n : ι
h :
  min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n) + edist (y n) (z n)) ≤
    min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
      min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n))
h₁ :
  min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n))
      (min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
        min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n))) ≤
    min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
      min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n))
h₂ h₃ :
  min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
      min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n)) ≤
    min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
      min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n))
⊢ min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (z n)) ≤
    min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (x n) (y n)) +
      min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode n)) (edist (y n) (z n))

Tactic:
grw [edist_triangle _ (y n), min_add_distrib, min_le_right]

Premises used: min_le_right, min_add_distrib, PseudoEMetricSpace.edist_triangle
-- 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)
simp :
  (∀ (i : ℝ≥0∞) (i_1 : 0 < i),
      Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
        (⨅ (i : ι),
          ⨅ (i_2 : ℝ≥0∞), ⨅ (_ : 0 < i_2), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_2})
        {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < i}) ∧
    ∀ (i : ι) (i_1 : ℝ≥0∞) (i_2 : 0 < i_1),
      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) < i_1}
⊢ Eq (α := Filter (((i : ι) → F i) × ((i : ι) → F i))) (uniformity ((i : ι) → F i))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε})

Tactic:
simp only [Pi.uniformity, comap_iInf, gt_iff_lt, preimage_setOf_eq, comap_principal,
      PseudoEMetricSpace.uniformity_edist, le_antisymm_iff, le_iInf_iff, le_principal_iff]

Premises used: Filter.le_principal_iff, le_iInf_iff, Filter.comap_iInf, Set.preimage_setOf_eq, le_antisymm_iff, gt_iff_lt, Filter.comap_principal, PseudoEMetricSpace.uniformity_edist, Pi.uniformity
-- 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)
left :
  ∀ (i : ℝ≥0∞) (i_1 : 0 < i),
    Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
      (⨅ (i : ι),
        ⨅ (i_2 : ℝ≥0∞), ⨅ (_ : 0 < i_2), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_2})
      {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < i}
right :
  ∀ (i : ι) (i_1 : ℝ≥0∞) (i_2 : 0 < i_1),
    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) < i_1}
⊢ (∀ (i : ℝ≥0∞) (i_1 : 0 < i),
      Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
        (⨅ (i : ι),
          ⨅ (i_2 : ℝ≥0∞), ⨅ (_ : 0 < i_2), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_2})
        {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < i}) ∧
    ∀ (i : ι) (i_1 : ℝ≥0∞) (i_2 : 0 < i_1),
      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) < i_1}

Tactic:
constructor
-- 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 < ε
⊢ ε / 2 > 0

Tactic:
simpa using hε.ne'

Premises used: LT.lt.ne'
-- 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 < ε
left :
  ∀ (K : Finset ι) (hK : ∑' (i : { j : ι // j ∉ K }), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι)) < ε / 2),
    Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
      (⨅ (i : ι),
        ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_1})
      {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε}
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (⨅ (i : ι),
      ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_1})
    {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε}

Tactic:
obtain ⟨K, hK⟩ : ∃ K : Finset ι, ∑' i : {j // j ∉ K}, 2⁻¹ ^ encode (i : ι) < ε / 2 :=
        ((tendsto_order.1 <| ENNReal.tendsto_tsum_compl_atTop_zero
          (tsum_geometric_encode_lt_top ENNReal.one_half_lt_one).ne).2 _
            <| by simpa using hε.ne').exists

Premises used: tsum_geometric_encode_lt_top, Finset, ENNReal.tendsto_tsum_compl_atTop_zero, tendsto_order, Filter.Eventually.exists, And.right, Iff.mp, ENNReal.one_half_lt_one, LT.lt.ne
-- 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
⊢ Ne (α := ℝ≥0∞) (↑K.card : ℝ≥0∞) ∞

Tactic:
simp
-- 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
⊢ ε / 2 ≠ 0

Tactic:
simpa using hε.ne'

Premises used: LT.lt.ne'
-- 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
left :
  ∀ (δ : ℝ≥0∞) (δpos : 0 < δ) (hδ : δ * (↑K.card : ℝ≥0∞) < ε / 2),
    Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
      (⨅ (i : ι),
        ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_1})
      {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε}
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (⨅ (i : ι),
      ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_1})
    {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε}

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ δ * K.card < ε / 2 :=
        ENNReal.exists_pos_mul_lt (by simp) (by simpa using hε.ne')

Premises used: ENNReal.exists_pos_mul_lt, Finset.card
-- 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
left :
  ∀ (i : (↑(↑K : Set ι) : Type u_2)),
    Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
      (⨅ (i_1 : ℝ≥0∞),
        ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 (↑i : ι)) (a.2 (↑i : ι)) < i_1})
      {p : ((i : ι) → F i) × ((i : ι) → F i) | edist (p.1 (↑i : ι)) (p.2 (↑i : ι)) < δ}
left₁ :
  Subset (α := Set (((i : ι) → F i) × ((i : ι) → F i)))
    (⋂ (i : (↑(↑K : Set ι) : Type u_2)),
      {p : ((i : ι) → F i) × ((i : ι) → F i) | edist (p.1 (↑i : ι)) (p.2 (↑i : ι)) < δ})
    {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε}
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (⨅ (i : ι),
      ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : ι) → F i) × ((i : ι) → F i) | edist (a.1 i) (a.2 i) < i_1})
    {p : ((i : ι) → F i) × ((i : ι) → F i) | edist p.1 p.2 < ε}

Tactic:
apply @mem_iInf_of_iInter _ _ _ _ _ K.finite_toSet fun i =>
          {p : (∀ i : ι, F i) × ∀ i : ι, F i | edist (p.fst i) (p.snd i) < δ}

Premises used: Filter.mem_iInf_of_iInter, Finset.finite_toSet
-- 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
i : ι
hi : i ∈ (↑K : Set ι)
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (⨅ (i_1 : ℝ≥0∞),
      ⨅ (_ : 0 < i_1),
        𝓟
          {a : ((i : ι) → F i) × ((i : ι) → F i) |
            edist (a.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
                (a.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
              i_1})
    {p : ((i : ι) → F i) × ((i : ι) → F i) |
      edist (p.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
          (p.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
        δ}

Tactic:
mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)

Premises used: Set.Mem, Filter.mem_iInf_of_mem
-- 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
i : ι
hi : i ∈ (↑K : Set ι)
left :
  Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (𝓟
      {a : ((i : ι) → F i) × ((i : ι) → F i) |
        edist (a.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
            (a.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
          δ})
    {p : ((i : ι) → F i) × ((i : ι) → F i) |
      edist (p.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
          (p.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
        δ}
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (⨅ (i_1 : ℝ≥0∞),
      ⨅ (_ : 0 < i_1),
        𝓟
          {a : ((i : ι) → F i) × ((i : ι) → F i) |
            edist (a.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
                (a.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
              i_1})
    {p : ((i : ι) → F i) × ((i : ι) → F i) |
      edist (p.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
          (p.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
        δ}

Tactic:
refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)

Premises used: Filter.mem_iInf_of_mem
-- 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
i : ι
hi : i ∈ (↑K : Set ι)
⊢ Membership.mem (γ := Filter (((i : ι) → F i) × ((i : ι) → F i)))
    (𝓟
      {a : ((i : ι) → F i) × ((i : ι) → F i) |
        edist (a.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
            (a.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
          δ})
    {p : ((i : ι) → F i) × ((i : ι) → F i) |
      edist (p.1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι))
          (p.2 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑K : Set ι)) i hi) : ι)) <
        δ}

Tactic:
simp only [mem_principal, Subset.rfl]

Premises used: Filter.mem_principal, Set.Subset.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)
ε : ℝ≥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 :
  Membership.mem (γ := Set (((i : ι) → F i) × ((i : ι) → F i)))
    (⋂ (i : (↑(↑K : Set ι) : Type u_2)),
      {p : ((i : ι) → F i) × ((i : ι) → F i) | edist (p.1 (↑i : ι)) (p.2 (↑i : ι)) < δ})
    (x, y)
⊢ ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ

Tactic:
simp only [mem_iInter, mem_setOf_eq, SetCoe.forall, Finset.mem_coe] at hxy

Premises used: Set.mem_setOf_eq, Set.mem_iInter, SetCoe.forall, Finset.mem_coe
-- 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 (x x_1) (y x_1) < δ
⊢ edist x y = ∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i))

Tactic:
rfl

Premises used: setOf, 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)
ε : ℝ≥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 (x x_1) (y x_1) < δ
⊢ ∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)),
        min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) (edist (α := F (↑i : ι)) (x (↑i : ι)) (y (↑i : ι))))

Tactic:
(ENNReal.sum_add_tsum_compl ..).symm

Premises used: ENNReal.sum_add_tsum_compl, Eq.symm
-- 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 (x x_1) (y x_1) < δ
h₁ : ∀ i ∈ K, min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) ≤ edist (x i) (y i)
h₂ :
  ∀ (i : (↑(↑K : Set ι)ᶜ : Type u_2)),
    min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) (edist (α := F (↑i : ι)) (x (↑i : ι)) (y (↑i : ι))) ≤
      HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)),
        min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) (edist (α := F (↑i : ι)) (x (↑i : ι)) (y (↑i : ι)))) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, edist (x i) (y i))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι)))

Tactic:
gcongr
-- 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 (x x_1) (y x_1) < δ
i : ι
h : i ∈ K
⊢ min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) ≤ edist (x i) (y i)

Tactic:
apply min_le_right

Premises used: min_le_right
-- 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 (x x_1) (y x_1) < δ
i : (↑(↑K : Set ι)ᶜ : Type u_2)
⊢ min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) (edist (α := F (↑i : ι)) (x (↑i : ι)) (y (↑i : ι))) ≤
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))

Tactic:
apply min_le_left

Premises used: min_le_left
-- 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 (x x_1) (y x_1) < δ
⊢ Ne (α := ℝ≥0∞) (∑ i ∈ K, edist (x i) (y i)) ∞

Tactic:
simpa using fun i hi ↦ (hxy i hi).ne_top

Premises used: LT.lt.ne_top
-- 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 (x x_1) (y x_1) < δ
refine : LE.le (α := ℝ≥0∞) (∑ i ∈ K, edist (x i) (y i)) (∑ _i ∈ K, δ)
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ K, edist (x i) (y i))
      (∑' (i : (↑(↑K : Set ι)ᶜ : Type u_2)), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode (↑i : ι))) <
    ∑ _i ∈ K, δ + ε / 2

Tactic:
refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK

Premises used: ENNReal.add_lt_add_of_le_of_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)
ε : ℝ≥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 (x x_1) (y x_1) < δ
h : ∀ (i : ι) (hi : i ∈ K), edist (x i) (y i) ≤ δ
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ K, edist (x i) (y i)) (∑ _i ∈ K, δ)

Tactic:
gcongr with i hi
-- 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 (x x_1) (y x_1) < δ
i : ι
hi : i ∈ K
⊢ edist (x i) (y i) ≤ δ

Tactic:
(hxy i hi).le

Premises used: LT.lt.le
-- 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 (x x_1) (y x_1) < δ
i : ι
hi : i ∈ K
⊢ edist (x i) (y i) ≤ δ

Tactic:
exact (hxy i hi).le

Premises used: LT.lt.le
-- 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 (x x_1) (y x_1) < δ
bc : ∑ _i ∈ K, δ ≤ ε / 2
⊢ ∑ _i ∈ K, δ + ε / 2 ≤ ε / 2 + ε / 2

Tactic:
gcongr
-- 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 (x x_1) (y x_1) < δ
⊢ ∑ _i ∈ K, δ ≤ ε / 2

Tactic:
simpa [mul_comm] using hδ.le

Premises used: LT.lt.le, mul_comm
-- 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 (x x_1) (y x_1) < δ
⊢ ε / 2 + ε / 2 = ε

Tactic:
ENNReal.add_halves _

Premises used: ENNReal.add_halves