awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
this : ∀ (i : ι), (l i).NeBot
⊢ Cauchy (Filter.pi (α := α) l)

Tactic:
simpa [cauchy_pi_iff]

Premises used: cauchy_pi_iff
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
⊢ f.NeBot

Tactic:
have := hf.1
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : f.NeBot
⊢ ∀ (i : ι), ∃ (x : α i), map (eval (β := α) i) f ≤ 𝓝 x

Tactic:
simp_rw [cauchy_pi_iff', cauchy_iff_exists_le_nhds] at hf

Premises used: cauchy_pi_iff', cauchy_iff_exists_le_nhds
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
hf : ∀ (i : ι), ∃ (x : α i), map (eval (β := α) i) f ≤ 𝓝 x
choose : ∀ (x : (i : ι) → α i) (hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)), ∃ (x : (i : ι) → α i), f ≤ 𝓝 x
⊢ ∃ (x : (i : ι) → α i), f ≤ 𝓝 x

Tactic:
choose x hx using hf
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)
h : f ≤ 𝓝 x
⊢ ∃ (x : (i : ι) → α i), f ≤ 𝓝 x

Tactic:
use x
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)
h : f ≤ Filter.pi (α := α) fun (i : ι) ↦ 𝓝 (x i)
h₁ h₂ h₃ h₄ : ∀ (i : ι), Tendsto (eval (β := α) i) f (𝓝 (x i))
⊢ f ≤ 𝓝 x

Tactic:
rwa [nhds_pi, le_pi]

Premises used: nhds_pi, Filter.le_pi
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
simp_rw :
  Eq (α := UniformSpace ((a : ι) → α a)) (⨅ i ∈ ⋃₀ 𝔖, UniformSpace.comap (eval (β := α) i) (U i))
    (⨅ S ∈ 𝔖, ⨅ i ∈ S, UniformSpace.comap (eval (β := α) i) (U i))
⊢ Eq (α := UniformSpace ((a : ι) → α a))
    (UniformSpace.comap ((⋃₀ 𝔖).restrict (π := α)) (uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_1)) ↦ α (↑i : ι)))
    (⨅ S ∈ 𝔖, UniformSpace.comap (S.restrict (π := α)) (uniformSpace fun (i : (↑S : Type u_1)) ↦ α (↑i : ι)))

Tactic:
simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]

Premises used: Pi.uniformSpace_comap_restrict, iInf_sUnion
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ (t : TopologicalSpace X), T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
⊢ Nontrivial X

Tactic:
nontriviality X
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ (t : TopologicalSpace X), T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
h : Nontrivial X
rcases : ∀ (t : TopologicalSpace X) (ht : T2Space X) (hut : ∀ (i : ι), toTopologicalSpace ≤ t), CompleteSpace X
⊢ CompleteSpace X

Tactic:
rcases ht with ⟨t, ht, hut⟩
-- Module: Mathlib.Topology.UniformSpace.Pi
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)
simp_rw₆ :
  Eq.{u_5 + 1} (α := Filter (X × X)) (⨅ (i : ι), Filter.comap (fun (x : X × X) ↦ (x.1, x.2)) (𝓤 X)) (⨅ (i : ι), 𝓤 X)
simp_rw₇ : Eq.{u_5 + 1} (α := Filter (X × X)) (⨅ (i : ι), Filter.comap (fun (x : X × X) ↦ x) (𝓤 X)) (⨅ (i : ι), 𝓤 X)
⊢ IsUniformInducing (α := X) (const ι)

Tactic:
simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']

Premises used: Prod.eta, iInf_uniformity, Filter.comap_iInf, Function.comp_def, Filter.comap_comap, isUniformInducing_iff, Function.const, Filter.comap_id', Pi.uniformity
-- Module: Mathlib.Topology.UniformSpace.Pi
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 ι)

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']
-- Module: Mathlib.Topology.UniformSpace.Pi
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 ι)
simp_rw : IsComplete (α := ι → X) (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})
⊢ CompleteSpace X

Tactic:
simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
    setOf_forall]

Premises used: Set.range_const_eq_diagonal, completeSpace_iff_isComplete_range, Set.setOf_forall
-- Module: Mathlib.Topology.UniformSpace.Pi
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 ι)
⊢ 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
-- Module: Mathlib.Topology.UniformSpace.Pi
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})

Tactic:
IsClosed.isComplete <| .mono ?_ this

Premises used: IsClosed.mono, IsClosed.isComplete
-- Module: Mathlib.Topology.UniformSpace.Pi
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))
refine : IsClosed[Pi.topologicalSpace] (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})
⊢ IsComplete (α := ι → X) (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})

Tactic:
refine IsClosed.isComplete <| .mono ?_ this

Premises used: IsClosed.isComplete
-- Module: Mathlib.Topology.UniformSpace.Pi
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))
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})

Tactic:
isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
    isClosed_eq (continuous_apply _) (continuous_apply _)

Premises used: isClosed_eq, isClosed_iInter
-- Module: Mathlib.Topology.UniformSpace.Pi
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))
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : ι), ⋂ (i_1 : ι), {x : ι → X | x i = x i_1})

Tactic:
exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
    isClosed_eq (continuous_apply _) (continuous_apply _)

Premises used: isClosed_eq, continuous_apply, isClosed_iInter
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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
⊢ Subset (α := Set (C(Y, V) × C(Y, V)))
    {fg : C(Y, V) × C(Y, V) |
      ∀ (x : Y),
        Membership.mem (γ := Set Y) Set.univ x →
          Membership.mem (α := V × V) S (((fg.1 : (a : Y) → V) x, (fg.2 : (a : Y) → V) x) : V × 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:
simp only [Set.mem_univ, true_implies, subset_refl]

Premises used: subset_refl, true_implies, Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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
⊢ 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]⟩
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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)}
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)
⊢ ∃ (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')

Premises used: ContinuousMap.curry, ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal, nhdsSet_diagonal_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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)

Tactic:
⟨n, fun i ↦ ⟨_, (U i).isClopen.continuous_indicator <| continuous_const (y := 1)⟩,
    v, fun x y ↦ ?_⟩

Premises used: Set.indicator, ContinuousMap.mk, continuous_const, TopologicalSpace.Clopens.isClopen, IsClopen.continuous_indicator, SetLike.coe, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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))
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 := ⋯ } : C(X, R)))
                      i :
                    (a : X) → R)
                  x :
                R)
              ((v i : (a : Y) → V) y : V)) :
        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)

Tactic:
refine ⟨n, fun i ↦ ⟨_, (U i).isClopen.continuous_indicator <| continuous_const (y := 1)⟩,
    v, fun x y ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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.curry : (a : X) → C(Y, V)) x : C(Y, V)) : (a : Y) → V) y,
        (∑ n : Fin n, (↑(U n) : Set X).indicator (fun (x : X) ↦ v n) x : (a : Y) → V) y) :
      V × V)

Tactic:
hv x y
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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
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 := ⋯ } : 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)
⊢ 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)

Tactic:
convert! hv x y using 2
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
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
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 := ⋯ } : (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)
⊢ 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)

Tactic:
simp only [sum_apply]

Premises used: ContinuousMap.sum_apply