awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
have 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 := 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: by_cases hi : x ∈ U i
-- 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
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
⊢ 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
have 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 := 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: by_cases hi : x ∈ U i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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)
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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)
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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)
⊢ (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')
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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)
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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)
⊢ 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))
have 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))
Tactic: rw [tensorHom, TensorProduct.lift.tmul]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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))
⊢ 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))
have 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))
Tactic: rw [tensorHom, TensorProduct.lift.tmul]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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)
⊢ 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
have 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))
Tactic: simp_rw [mem_closure_iff, Set.nonempty_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (hypothesis)
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
⊢ ∃ (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))
have 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}
Tactic: have := mem_nhds_uniformity_iff_right.mp (hUo.mem_nhds hUf)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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}
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨J, hJu, hJ'⟩ := (hasBasis_compactConvergenceUniformity_of_compact).mem_iff.mp this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (goal)
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}
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))
have obtain : ∀ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, R))
  (hgh :
    ∀ (x : X) (y : Y),
      Membership.mem (α := R × R) J
        (((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)),
  ∃ (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 ⟨n, g, h, hgh⟩ := exists_finite_sum_mul_approximation_of_mem_uniformity f hJu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (hypothesis)
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}
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}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh :
  ∀ (x : X) (y : Y),
    Membership.mem (α := R × R) J
      (((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)
⊢ ∃ (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))
have hG : Membership.mem (γ := 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)}
    (f,
      ((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))
        (∑ i : Fin n, g i ⊗ₜ[R] h i)) →
  Membership.mem (γ := Set (C(X × Y, R) × C(X × Y, R))) {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
    (f,
      ((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))
        (∑ i : Fin n, g i ⊗ₜ[R] h i))
Tactic: have hG := Set.mem_of_subset_of_mem hJ' (a := (f, tensorHom <| ∑ i, g i ⊗ₜ h i))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.ProdApproximation (hypothesis)
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}
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}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh :
  ∀ (x : X) (y : Y),
    Membership.mem (α := R × R) J
      (((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)
hG :
  Membership.mem (γ := 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)}
      (f,
        ((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))
          (∑ i : Fin n, g i ⊗ₜ[R] h i)) →
    Membership.mem (γ := Set (C(X × Y, R) × C(X × Y, R))) {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
      (f,
        ((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))
          (∑ i : Fin n, g i ⊗ₜ[R] h i))
⊢ ∃ (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))
have hG₁ : (∀ (a : X) (b : Y),
    Membership.mem (α := R × R) J
      (((f : (a : X × Y) → R) (a, b),
          (((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))
                (∑ i : Fin n, g i ⊗ₜ[R] h i) :
              (a : X × Y) → R)
            (a, b)) :
        R × 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))
      (∑ i : Fin n, g i ⊗ₜ[R] h i) ∈
    U
Tactic: simp only [Prod.forall, Set.mem_setOf_eq, forall_const] at hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Real (goal)
Goal:
⊢ CompleteSpace ℝ
have a : ∀ (u : ℕ → ℝ), CauchySeq u → ∃ (a : ℝ), Tendsto u atTop (nhds a)
Tactic: apply complete_of_cauchySeq_tendsto
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Real (goal)
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
⊢ ∃ (a : ℝ), Tendsto u atTop (nhds a)
have a : ∀ (s : Set ℝ) (h : s ∈ nhds c.lim), s ∈ map u atTop
Tactic: refine ⟨c.lim, fun s h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Real (goal)
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
⊢ s ∈ map u atTop
have a : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball c.lim ε ⊆ s), s ∈ map u atTop
Tactic: rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Real (hypothesis)
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
⊢ s ∈ map u atTop
have this : ∃ (i : ℕ), ∀ j ≥ i, |(↑(c - CauSeq.const abs c.lim) : ℕ → ℝ) j| < ε
Tactic: have := c.equiv_lim ε ε0
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Real (goal)
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, |(↑(c - CauSeq.const abs c.lim) : ℕ → ℝ) j| < ε
⊢ s ∈ map u atTop
have a : ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s
Tactic: simp only [mem_map, mem_atTop_sets]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
b : Bool
x : (↑(S b) : Type u)
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
have hST : Disjoint (S b) (closure[inst.toTopologicalSpace] (S !b))
Tactic: have hST : Disjoint (S b) (closure (S !b)) := b.casesOn (false := hsT) (true := hSt.symm)