awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw₁ : Eq.{u_5 + 1} (α := Filter (X × X))
  (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X))) (⨅ (i : ι), 𝓤 X)
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X))) (⨅ (i : ι), 𝓤 X)
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw₂ : Eq.{u_5 + 1} (α := Filter (X × X))
  (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
    (⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
  (⨅ (i : ι), 𝓤 X)
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X))) (⨅ (i : ι), 𝓤 X)
simp_rw₂ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
      (⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw₃ : Eq.{u_5 + 1} (α := Filter (X × X))
  (⨅ (i : ι),
    Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
      (Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
  (⨅ (i : ι), 𝓤 X)
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X))) (⨅ (i : ι), 𝓤 X)
simp_rw₂ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
      (⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
simp_rw₃ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (⨅ (i : ι),
      Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
        (Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw₄ : Eq.{u_5 + 1} (α := Filter (X × X))
  (⨅ (i : ι),
    Filter.comap
      ((fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) ∘ fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 X))
  (⨅ (i : ι), 𝓤 X)
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X))) (⨅ (i : ι), 𝓤 X)
simp_rw₂ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
      (⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
simp_rw₃ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (⨅ (i : ι),
      Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
        (Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
simp_rw₄ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (⨅ (i : ι),
      Filter.comap
        ((fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) ∘ fun (x : X × X) ↦ (const ι x.1, const ι x.2))
        (𝓤 X))
    (⨅ (i : ι), 𝓤 X)
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw₅ : Eq.{u_5 + 1} (α := Filter (X × X)) (⨅ (i : ι), Filter.comap (fun (x : X × X) ↦ (const ι x.1 i, const ι x.2 i)) (𝓤 X))
  (⨅ (i : ι), 𝓤 X)
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
simp_rw : Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = 𝓤 X
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X))) (⨅ (i : ι), 𝓤 X)
simp_rw₂ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
      (⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
simp_rw₃ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (⨅ (i : ι),
      Filter.comap (β := (ι → X) × (ι → X)) (fun (x : X × X) ↦ (const ι x.1, const ι x.2))
        (Filter.comap (fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) (𝓤 X)))
    (⨅ (i : ι), 𝓤 X)
simp_rw₄ :
  Eq.{u_5 + 1} (α := Filter (X × X))
    (⨅ (i : ι),
      Filter.comap
        ((fun (a : ((i : ι) → X) × ((i : ι) → X)) ↦ (a.1 i, a.2 i)) ∘ fun (x : X × X) ↦ (const ι x.1, const ι x.2))
        (𝓤 X))
    (⨅ (i : ι), 𝓤 X)
simp_rw₅ :
  Eq.{u_5 + 1} (α := Filter (X × X)) (⨅ (i : ι), Filter.comap (fun (x : X × X) ↦ (const ι x.1 i, const ι x.2 i)) (𝓤 X))
    (⨅ (i : ι), 𝓤 X)
⊢ IsUniformInducing (α := X) (const ι)
have simp_rw₆ : Eq.{u_5 + 1} (α := Filter (X × X)) (⨅ (i : ι), Filter.comap (fun (x : X × X) ↦ (x.1, x.2)) (𝓤 X)) (⨅ (i : ι), 𝓤 X)
Tactic: simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (hypothesis)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
⊢ CompleteSpace X
have this : IsUniformInducing (α := X) (const ι)
Tactic: have : @IsUniformInducing X (ι → X) (⨅ i, u i) (Pi.uniformSpace (U := u)) (const ι) := by
    simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this : IsUniformInducing (α := X) (const ι)
⊢ CompleteSpace X
have simp_rw : IsComplete (α := ι → X) (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})
Tactic: simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
    setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (hypothesis)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this : IsUniformInducing (α := X) (const ι)
⊢ IsComplete (α := ι → X) (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})
have this₁ : LE.le (α := TopologicalSpace ((i : ι) → X)) (Pi.topologicalSpace (Y := fun (i : ι) ↦ X))
  (Pi.topologicalSpace (Y := fun (x : ι) ↦ X))
Tactic: have : Pi.topologicalSpace (t₂ := fun i ↦ (u i).toTopologicalSpace) ≤
         Pi.topologicalSpace (t₂ := fun _ ↦ t) :=
    iInf_mono fun i ↦ induced_mono <| hut i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
h : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this_1 : IsUniformInducing (α := X) (const ι)
this :
  LE.le (α := TopologicalSpace ((i : ι) → X)) (Pi.topologicalSpace (Y := fun (i : ι) ↦ X))
    (Pi.topologicalSpace (Y := fun (x : ι) ↦ X))
⊢ IsComplete (α := ι → X) (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})
have refine : IsClosed[Pi.topologicalSpace] (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})
Tactic: refine IsClosed.isComplete <| .mono ?_ this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
inst_9 : TopologicalSpace R
inst_10 : MonoidWithZero R
inst_11 : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
⊢ ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)),
    ∀ (x : X) (y : Y),
      Membership.mem (α := V × V) S
        (((f : (a : X × Y) → V) (x, y),
            ∑ i : Fin n,
              HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → V) y : V)) :
          V × V)
have hS' : Membership.mem (γ := Filter (C(Y, V) × C(Y, V))) (𝓤 C(Y, V))
  {x : C(Y, V) × C(Y, V) |
    match (motive := C(Y, V) × C(Y, V) → Prop) x with
    | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
Tactic: have hS' : {(f, g) | ∀ y, (f y, g y) ∈ S} ∈ 𝓤 C(Y, V) :=
    (mem_compactConvergence_entourage_iff _).mpr
      ⟨_, _, isCompact_univ, hS, by simp only [Set.mem_univ, true_implies, subset_refl]⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
inst_9 : TopologicalSpace R
inst_10 : MonoidWithZero R
inst_11 : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' :
  Membership.mem (γ := Filter (C(Y, V) × C(Y, V))) (𝓤 C(Y, V))
    {x : C(Y, V) × C(Y, V) |
      match (motive := C(Y, V) × C(Y, V) → Prop) x with
      | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
⊢ ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)),
    ∀ (x : X) (y : Y),
      Membership.mem (α := V × V) S
        (((f : (a : X × Y) → V) (x, y),
            ∑ i : Fin n,
              HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → V) y : V)) :
          V × V)
have obtain : ∀ (n : ℕ) (U : Fin n → TopologicalSpace.Clopens X) (v : Fin n → C(Y, V))
  (hv :
    ∀ (x : X),
      Membership.mem (α := C(Y, V) × C(Y, V)) (γ := Set (C(Y, V) × C(Y, V)))
        {x : C(Y, V) × C(Y, V) |
          match (motive := C(Y, V) × C(Y, V) → Prop) x with
          | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
        (((f.curry : (a : X) → C(Y, V)) x, ∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x) :
          C(Y, V) × C(Y, V))),
  ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)),
    ∀ (x : X) (y : Y),
      Membership.mem (α := V × V) S
        (((f : (a : X × Y) → V) (x, y),
            ∑ i : Fin n,
              HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → V) y : V)) :
          V × V)
Tactic: obtain ⟨n, U, v, hv⟩ := exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal
    f.curry (nhdsSet_diagonal_le_uniformity hS')
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
inst_9 : TopologicalSpace R
inst_10 : MonoidWithZero R
inst_11 : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' :
  Membership.mem (γ := Filter (C(Y, V) × C(Y, V))) (𝓤 C(Y, V))
    {x : C(Y, V) × C(Y, V) |
      match (motive := C(Y, V) × C(Y, V) → Prop) x with
      | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv :
  ∀ (x : X),
    Membership.mem (α := C(Y, V) × C(Y, V)) (γ := Set (C(Y, V) × C(Y, V)))
      {x : C(Y, V) × C(Y, V) |
        match (motive := C(Y, V) × C(Y, V) → Prop) x with
        | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
      (((f.curry : (a : X) → C(Y, V)) x, ∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x) :
        C(Y, V) × C(Y, V))
⊢ ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)),
    ∀ (x : X) (y : Y),
      Membership.mem (α := V × V) S
        (((f : (a : X × Y) → V) (x, y),
            ∑ i : Fin n,
              HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → V) y : V)) :
          V × V)
have refine : ∀ (x : X) (y : Y),
  Membership.mem (α := V × V) S
    (((f : (a : X × Y) → V) (x, y),
        ∑ i : Fin n,
          HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            (((fun (i : Fin n) ↦
                      ({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := sorry } : C(X, R)))
                    i :
                  (a : X) → R)
                x :
              R)
            ((v i : (a : Y) → V) y : V)) :
      V × V)
Tactic: refine ⟨n, fun i ↦ ⟨_, (U i).isClopen.continuous_indicator <| continuous_const (y := 1)⟩,
    v, fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
inst_9 : TopologicalSpace R
inst_10 : MonoidWithZero R
inst_11 : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' :
  Membership.mem (γ := Filter (C(Y, V) × C(Y, V))) (𝓤 C(Y, V))
    {x : C(Y, V) × C(Y, V) |
      match (motive := C(Y, V) × C(Y, V) → Prop) x with
      | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv :
  ∀ (x : X),
    Membership.mem (α := C(Y, V) × C(Y, V)) (γ := Set (C(Y, V) × C(Y, V)))
      {x : C(Y, V) × C(Y, V) |
        match (motive := C(Y, V) × C(Y, V) → Prop) x with
        | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
      (((f.curry : (a : X) → C(Y, V)) x, ∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x) :
        C(Y, V) × C(Y, V))
x : X
y : Y
⊢ Membership.mem (α := V × V) S
    (((f : (a : X × Y) → V) (x, y),
        ∑ i : Fin n,
          HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            (((fun (i : Fin n) ↦
                      ({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ } : C(X, R)))
                    i :
                  (a : X) → R)
                x :
              R)
            ((v i : (a : Y) → V) y : V)) :
      V × V)
have h : Eq.{u_4 + 1} (α := V)
  (∑ i : Fin n,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        (((fun (i : Fin n) ↦ ({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := sorry } : C(X, R)))
                i :
              (a : X) → R)
            x :
          R)
        ((v i : (a : Y) → V) y : V) :
    V)
  ((∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x : (a : Y) → V) y : V)
Tactic: convert! hv x y using 2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
inst_9 : TopologicalSpace R
inst_10 : MonoidWithZero R
inst_11 : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' :
  Membership.mem (γ := Filter (C(Y, V) × C(Y, V))) (𝓤 C(Y, V))
    {x : C(Y, V) × C(Y, V) |
      match (motive := C(Y, V) × C(Y, V) → Prop) x with
      | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv :
  ∀ (x : X),
    Membership.mem (α := C(Y, V) × C(Y, V)) (γ := Set (C(Y, V) × C(Y, V)))
      {x : C(Y, V) × C(Y, V) |
        match (motive := C(Y, V) × C(Y, V) → Prop) x with
        | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
      (((f.curry : (a : X) → C(Y, V)) x, ∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x) :
        C(Y, V) × C(Y, V))
x : X
y : Y
⊢ Eq.{u_4 + 1} (α := V)
    (∑ i : Fin n,
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
          (((fun (i : Fin n) ↦
                    ({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ } : C(X, R)))
                  i :
                (a : X) → R)
              x :
            R)
          ((v i : (a : Y) → V) y : V) :
      V)
    ((∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x : (a : Y) → V) y : V)
have h : Eq.{u_4 + 1} (α := V)
  (∑ x_1 : Fin n,
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      (({ toFun := (↑(U x_1) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := sorry } : (a : X) → R) x : R)
      ((v x_1 : (a : Y) → V) y : V))
  (∑ i : Fin n, ((↑(U i) : Set X).indicator (fun (x : X) ↦ v i) x : (a : Y) → V) y)
Tactic: simp only [sum_apply]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
inst_9 : TopologicalSpace R
inst_10 : MonoidWithZero R
inst_11 : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' :
  Membership.mem (γ := Filter (C(Y, V) × C(Y, V))) (𝓤 C(Y, V))
    {x : C(Y, V) × C(Y, V) |
      match (motive := C(Y, V) × C(Y, V) → Prop) x with
      | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv :
  ∀ (x : X),
    Membership.mem (α := C(Y, V) × C(Y, V)) (γ := Set (C(Y, V) × C(Y, V)))
      {x : C(Y, V) × C(Y, V) |
        match (motive := C(Y, V) × C(Y, V) → Prop) x with
        | (f, g) => ∀ (y : Y), Membership.mem (α := V × V) S (((f : (a : Y) → V) y, (g : (a : Y) → V) y) : V × V)}
      (((f.curry : (a : X) → C(Y, V)) x, ∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x) :
        C(Y, V) × C(Y, V))
x : X
y : Y
⊢ Eq.{u_4 + 1} (α := V)
    (∑ x_1 : Fin n,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        (({ toFun := (↑(U x_1) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ } : (a : X) → R) x : R)
        ((v x_1 : (a : Y) → V) y : V))
    (∑ i : Fin n, ((↑(U i) : Set X).indicator (fun (x : X) ↦ v i) x : (a : Y) → V) y)
have h : ∀ (i : Fin n),
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      (({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := sorry : C(X, R) } : (a : X) → R) x : R)
      ((v i : (a : Y) → V) y : V) =
    ((↑(U i) : Set X).indicator (fun (x : X) ↦ v i) x : (a : Y) → V) y
Tactic: congr 1 with i