awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ) (hm : m ≤ n + k), Set.Subsingleton.{u_1} (α := ι) {j : ι | (D m j ∩ B).Nonempty}
⊢ Set.Finite.{u_1} (α := ℕ × ι) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty}
have this₁ : Set.Finite.{u_1} (α := ℕ × ι)
  (⋃ (m : ℕ),
    ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
Tactic: have : (⋃ (m ≤ n + k) (i ∈ { i : ι | (D m i ∩ B).Nonempty }), {(m, i)}).Finite :=
      (finite_le_nat _).biUnion' fun i hi =>
        (Hle i hi).finite.biUnion' fun _ _ => finite_singleton _
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ) (hm : m ≤ n + k), Set.Subsingleton.{u_1} (α := ι) {j : ι | (D m j ∩ B).Nonempty}
this :
  Set.Finite.{u_1} (α := ℕ × ι)
    (⋃ (m : ℕ),
      ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
⊢ Set.Finite.{u_1} (α := ℕ × ι) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty}
have refine_2 : ∀ (I : ℕ × ι)
  (hI : Membership.mem (γ := Set (ℕ × ι)) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty} I),
  Membership.mem (γ := Set (ℕ × ι))
    (⋃ (m : ℕ),
      ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
    I
Tactic: refine this.subset fun I hI => ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ) (hm : m ≤ n + k), Set.Subsingleton.{u_1} (α := ι) {j : ι | (D m j ∩ B).Nonempty}
this :
  Set.Finite.{u_1} (α := ℕ × ι)
    (⋃ (m : ℕ),
      ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
I : ℕ × ι
hI : Membership.mem (γ := Set (ℕ × ι)) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty} I
⊢ Membership.mem (γ := Set (ℕ × ι))
    (⋃ (m : ℕ),
      ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
    I
have refine_2 : ∃ (i : ℕ) (_ : i ≤ n + k) (i_1 : ι) (_ : Membership.mem (γ := Set ι) {i_2 : ι | (D i i_2 ∩ B).Nonempty} i_1),
  Membership.mem (γ := Set (ℕ × ι)) {(i, i_1)} I
Tactic: simp only [mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ) (hm : m ≤ n + k), Set.Subsingleton.{u_1} (α := ι) {j : ι | (D m j ∩ B).Nonempty}
this :
  Set.Finite.{u_1} (α := ℕ × ι)
    (⋃ (m : ℕ),
      ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
I : ℕ × ι
hI : Membership.mem (γ := Set (ℕ × ι)) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty} I
⊢ ∃ (i : ℕ) (_ : i ≤ n + k) (i_1 : ι) (_ : Membership.mem (γ := Set ι) {i_2 : ι | (D i i_2 ∩ B).Nonempty} i_1),
    Membership.mem (γ := Set (ℕ × ι)) {(i, i_1)} I
have refine_2 : I.1 ≤ n + k
Tactic: refine ⟨I.1, ?_, I.2, hI, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
⊢ Eq (α := Filter (((b : β) → X b) × ((b : β) → X b))) (𝓤 ((b : β) → X b))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | edist p.1 p.2 < ε})
have simp : Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
  (⨅ (i : β), ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < i_1})
  (⨅ (ε : ℝ≥0∞),
    ⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
Tactic: simp only [Pi.uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf, gt_iff_lt,
      preimage_setOf_eq, comap_principal, edist_pi_def]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
⊢ Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
    (⨅ (i : β),
      ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < i_1})
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
have rw : Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
  (⨅ (j : ℝ≥0∞), ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
  (⨅ (ε : ℝ≥0∞),
    ⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
Tactic: rw [iInf_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
⊢ Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
    (⨅ (j : ℝ≥0∞), ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
have e_s : Eq (α := ℝ≥0∞ → Filter (((b : β) → X b) × ((b : β) → X b)))
  (fun (j : ℝ≥0∞) ↦ ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
  fun (ε : ℝ≥0∞) ↦
  ⨅ (_ : 0 < ε), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
⊢ Eq (α := ℝ≥0∞ → Filter (((b : β) → X b) × ((b : β) → X b)))
    (fun (j : ℝ≥0∞) ↦ ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
    fun (ε : ℝ≥0∞) ↦
    ⨅ (_ : 0 < ε), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}
have e_s : ∀ (ε : ℝ≥0∞),
  Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (i : β), ⨅ (_ : 0 < ε), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
Tactic: funext ε
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (i : β), ⨅ (_ : 0 < ε), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
have e_s : Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
  (⨅ (_ : 0 < ε), ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
  (⨅ (_ : 0 < ε), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
Tactic: rw [iInf_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (_ : 0 < ε), ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
have e_s : Eq (α := 0 < ε → Filter (((i : β) → X i) × ((i : β) → X i)))
  (fun (j : 0 < ε) ↦ ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε}) fun (x : 0 < ε) ↦
  𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Pi (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ Eq (α := 0 < ε → Filter (((i : β) → X i) × ((i : β) → X i)))
    (fun (j : 0 < ε) ↦ ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    fun (x : 0 < ε) ↦
    𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}
have e_s : ∀ (εpos : 0 < ε),
  Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
Tactic: funext εpos
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
⊢ ContinuousWithinAt φ B x
have suffices : ∀ V' ∈ 𝓝 (φ x), IsClosed[inst_1] V' → φ ⁻¹' V' ∈ 𝓝[B] x
Tactic: suffices ∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x by
    simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
⊢ ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'
have this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
Tactic: have := tendsto_extendFrom (hf x x_in)
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
⊢ ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'
have rcases : ∀ (V : Set X) (hV : MapsTo f (V ∩ A) V') (hxV : x ∈ V) (V_op : IsOpen[inst] V),
  ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'
Tactic: rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
have obtain : ∀ (V : Set X) (V_in : V ∈ 𝓝 x) (V_op : IsOpen[inst] V) (hV : V ∩ A ⊆ f ⁻¹' V'), φ ⁻¹' V' ∈ 𝓝[B] x
Tactic: obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V' := by
    have := tendsto_extendFrom (hf x x_in)
    rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
    exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
have suffices : ∀ y ∈ V ∩ B, φ y ∈ V'
Tactic: suffices ∀ y ∈ V ∩ B, φ y ∈ V' from
    mem_of_superset (inter_mem_inf V_in <| mem_principal_self B) this
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
⊢ φ y ∈ V'
have this : (𝓝[A] y).NeBot
Tactic: haveI := mem_closure_iff_nhdsWithin_neBot.mp (hB hyB)
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
⊢ φ y ∈ V'
have limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
Tactic: have limy : Tendsto f (𝓝[A] y) (𝓝 <| φ y) := tendsto_extendFrom (hf y hyB)
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
⊢ φ y ∈ V'
have hVy : V ∈ 𝓝 y
Tactic: have hVy : V ∈ 𝓝 y := IsOpen.mem_nhds V_op hyV
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
⊢ φ y ∈ V'
have this₁ : V ∩ A ∈ 𝓝[A] y
Tactic: have : V ∩ A ∈ 𝓝[A] y := by simpa only [inter_comm] using inter_mem_nhdsWithin A hVy
-- Lean 4 proof step from Mathlib.Topology.ExtendFrom (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
⊢ Continuous[inst, inst_1] (extendFrom A f)
have rw : ContinuousOn (extendFrom A f) univ
Tactic: rw [← continuousOn_univ]