awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (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 := ⋯ : 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
⊢ 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)

Tactic:
congr 1 with i
-- 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
i : Fin n
pos :
  ∀ (hi : x ∈ U i),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        (({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ : 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
neg :
  ∀ (hi : x ∉ U i),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        (({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ : 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
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      (({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ : 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:
by_cases hi : x ∈ U i
-- 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
i : Fin n
hi : x ∈ U i
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      (({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ : 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:
simp [hi]
-- 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
i : Fin n
hi : x ∉ U i
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      (({ toFun := (↑(U i) : Set X).indicator fun (x : X) ↦ 1, continuous_toFun := ⋯ : 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:
simp [hi]
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
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 : Ring R
inst_7 : UniformSpace R
inst_8 : IsUniformAddGroup R
f : C(X × Y, R)
S : Set (R × R)
hS : S ∈ 𝓤 R
⊢ ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, R)),
    ∀ (x : X) (y : Y),
      Membership.mem (α := R × R) S
        (((f : (a : X × Y) → R) (x, y),
            ∑ i : Fin n, HMul.hMul (α := R) (β := R) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → R) y : R)) :
          R × R)

Tactic:
exists_finite_sum_smul_approximation_of_mem_uniformity f hS

Premises used: Set.Mem, ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
f f' : C(X, R)
g : C(Y, R)
h :
  ∀ (a : X × Y),
    Eq.{u_7 + 1} (α := R)
      (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) (f + f') g : (a : X × Y) → R) a : R)
      ((HAdd.hAdd (α := C(X × Y, R)) ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)
              ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f' g) :
            (a : X × Y) → R)
          a :
        R)
⊢ (fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) (f + f') g =
    HAdd.hAdd (α := C(X × Y, R)) ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)
      ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f' g)

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
f f' : C(X, R)
g : C(Y, R)
a : X × Y
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) (f + f') g : (a : X × Y) → R) a : R)
    ((HAdd.hAdd (α := C(X × Y, R)) ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)
            ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f' g) :
          (a : X × Y) → R)
        a :
      R)

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
r : R
f : C(X, R)
g : C(Y, R)
h :
  ∀ (a : X × Y),
    Eq.{u_7 + 1} (α := R)
      (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) (r • f) g : (a : X × Y) → R) a : R)
      ((HSMul.hSMul (β := C(X × Y, R)) r ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g) :
            (a : X × Y) → R)
          a :
        R)
⊢ (fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) (r • f) g =
    HSMul.hSMul (β := C(X × Y, R)) r ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
r : R
f : C(X, R)
g : C(Y, R)
a : X × Y
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) (r • f) g : (a : X × Y) → R) a : R)
    ((HSMul.hSMul (β := C(X × Y, R)) r ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g) :
          (a : X × Y) → R)
        a :
      R)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
f : C(X, R)
g g' : C(Y, R)
h :
  ∀ (a : X × Y),
    Eq.{u_7 + 1} (α := R)
      (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f (g + g') : (a : X × Y) → R) a : R)
      ((HAdd.hAdd (α := C(X × Y, R)) ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)
              ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g') :
            (a : X × Y) → R)
          a :
        R)
⊢ (fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f (g + g') =
    HAdd.hAdd (α := C(X × Y, R)) ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)
      ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g')

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
f : C(X, R)
g g' : C(Y, R)
a : X × Y
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f (g + g') : (a : X × Y) → R) a : R)
    ((HAdd.hAdd (α := C(X × Y, R)) ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)
            ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g') :
          (a : X × Y) → R)
        a :
      R)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
r : R
f : C(X, R)
g : C(Y, R)
h :
  ∀ (a : X × Y),
    Eq.{u_7 + 1} (α := R)
      (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f (r • g) : (a : X × Y) → R) a : R)
      ((HSMul.hSMul (β := C(X × Y, R)) r ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g) :
            (a : X × Y) → R)
          a :
        R)
⊢ (fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f (r • g) =
    HSMul.hSMul (β := C(X × Y, R)) r ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g)

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X_1 : Type u_1
Y_1 : Type u_2
R_1 : Type u_3
V : Type u_4
inst : TopologicalSpace X_1
inst_1 : TotallyDisconnectedSpace X_1
inst_2 : T2Space X_1
inst_3 : CompactSpace X_1
inst_4 : TopologicalSpace Y_1
inst_5 : CompactSpace Y_1
inst_6 : AddCommGroup V
inst_7 : UniformSpace V
inst_8 : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst_9 : TopologicalSpace X
inst_10 : TopologicalSpace Y
inst_11 : CommRing R
inst_12 : TopologicalSpace R
inst_13 : IsTopologicalRing R
r : R
f : C(X, R)
g : C(Y, R)
a : X × Y
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f (r • g) : (a : X × Y) → R) a : R)
    ((HSMul.hSMul (β := C(X × Y, R)) r ((fun (f : C(X, R)) (g : C(Y, R)) ↦ f.comp fst * g.comp snd) f g) :
          (a : X × Y) → R)
        a :
      R)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
f : C(X, R)
g : C(Y, R)
p : X × Y
⊢ ((((((prodMul : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R)) → C(Y, R) →ₗ[R] C(X × Y, R)) f :
                C(Y, R) →ₗ[R] C(X × Y, R)) :
              (a : C(Y, R)) → C(X × Y, R))
            g :
          C(X × Y, R)) :
        (a : X × Y) → R)
      p =
    HMul.hMul (α := R) (β := R) ((f : (a : X) → R) p.1 : R) ((g : (a : Y) → R) p.2 : R)

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
f : C(X, R)
g : C(Y, R)
⊢ ((((prodMul : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R)) → C(Y, R) →ₗ[R] C(X × Y, R)) f :
          C(Y, R) →ₗ[R] C(X × Y, R)) :
        (a : C(Y, R)) → C(X × Y, R))
      g =
    f.comp fst * g.comp snd

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
f : C(X, R)
g : C(Y, R)
rw :
  Eq (α := C(X × Y, R))
    (((TensorProduct.lift prodMul : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
        (f ⊗ₜ[R] g) :
      C(X × Y, R))
    (((((prodMul : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R)) → C(Y, R) →ₗ[R] C(X × Y, R)) f :
            C(Y, R) →ₗ[R] C(X × Y, R)) :
          (a : C(Y, R)) → C(X × Y, R))
        g :
      C(X × Y, R))
rw₁ rw₂ :
  Eq (α := C(X × Y, R))
    (((((prodMul : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R)) → C(Y, R) →ₗ[R] C(X × Y, R)) f :
            C(Y, R) →ₗ[R] C(X × Y, R)) :
          (a : C(Y, R)) → C(X × Y, R))
        g :
      C(X × Y, R))
    (((((prodMul : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R)) → C(Y, R) →ₗ[R] C(X × Y, R)) f :
            C(Y, R) →ₗ[R] C(X × Y, R)) :
          (a : C(Y, R)) → C(X × Y, R))
        g :
      C(X × Y, R))
⊢ Eq (α := C(X × Y, R))
    (((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R)) (f ⊗ₜ[R] g) :
      C(X × Y, R))
    (((((prodMul : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R)) → C(Y, R) →ₗ[R] C(X × Y, R)) f :
            C(Y, R) →ₗ[R] C(X × Y, R)) :
          (a : C(Y, R)) → C(X × Y, R))
        g :
      C(X × Y, R))

Tactic:
rw [tensorHom, TensorProduct.lift.tmul]

Premises used: TensorProduct.lift.tmul, ContinuousMap.tensorHom
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
simp_rw :
  ∀ (o : Set C(X × Y, R)),
    IsOpen o →
      f ∈ o →
        ∃ (x : C(X × Y, R)),
          x ∈
            o ∩
              Set.range (ι := C(X, R) ⊗[R] C(Y, R))
                (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
⊢ Membership.mem (γ := Set C(X × Y, R))
    (closure
      (Set.range (ι := C(X, R) ⊗[R] C(Y, R))
        (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))))
    f

Tactic:
simp_rw [mem_closure_iff, Set.nonempty_def]

Premises used: mem_closure_iff, Set.nonempty_def
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
⊢ Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}

Tactic:
have := mem_nhds_uniformity_iff_right.mp (hUo.mem_nhds hUf)
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this_2 : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this :
  Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
obtain :
  ∀ (J : Set (R × R)) (hJu : J ∈ 𝓤 R)
    (hJ' :
      Subset (α := Set (C(X × Y, R) × C(X × Y, R)))
        {fg : C(X × Y, R) × C(X × Y, R) |
          ∀ (x : X × Y),
            Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
        {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}),
    ∃ (x : C(X × Y, R)),
      x ∈
        U ∩
          Set.range (ι := C(X, R) ⊗[R] C(Y, R))
            (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
⊢ ∃ (x : C(X × Y, R)),
    x ∈
      U ∩
        Set.range (ι := C(X, R) ⊗[R] C(Y, R))
          (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))

Tactic:
obtain ⟨J, hJu, hJ'⟩ := (hasBasis_compactConvergenceUniformity_of_compact).mem_iff.mp this

Premises used: Filter.HasBasis.mem_iff, Iff.mp, ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact