awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ closure[Pi.topologicalSpace] (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) =
    closure[Pi.topologicalSpace] (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i)))

Tactic:
(closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure

Premises used: closure_minimal, closure_mono, HasSubset.Subset.antisymm, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
refine_1 :
  (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) ⊆
    Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))
refine_2 :
  (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) ⊆
    closure[Pi.topologicalSpace] (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))
⊢ closure[Pi.topologicalSpace] (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) =
    closure[Pi.topologicalSpace] (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i)))

Tactic:
refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure

Premises used: closure_minimal, closure_mono, HasSubset.Subset.antisymm, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) ⊆
    Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))

Tactic:
SetLike.coe_mono <| iSup_map_single_le

Premises used: Submodule.iSup_map_single_le, Set.Mem, setOf, Set.pi, SetLike.coe_mono
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) ⊆
    Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))

Tactic:
exact SetLike.coe_mono <| iSup_map_single_le

Premises used: Submodule.iSup_map_single_le, SetLike.coe_mono
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
refine_2 :
  ∀ (x : (i : ι) → M i),
    Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x →
      ∀ (o : Set ((i : ι) → M i)),
        IsOpen[Pi.topologicalSpace] o →
          x ∈ o → (o ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty
⊢ (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) ⊆
    closure[Pi.topologicalSpace] (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))

Tactic:
simp only [Set.subset_def, mem_closure_iff]

Premises used: mem_closure_iff, Set.subset_def
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
refine_2 :
  ∀ (t : Finset ι) (V : (a : ι) → Set (M a)) (hV : ∀ a ∈ t, IsOpen[inst_3 a] (V a) ∧ x a ∈ V a)
    (hVU : (↑t : Set ι).pi (α := M) V ⊆ U),
    (U ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty
⊢ (U ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty

Tactic:
rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩

Premises used: isOpen_pi_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst_3 a] (V a) ∧ x a ∈ V a
hVU : (↑t : Set ι).pi (α := M) V ⊆ U
⊢ (U ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty

Tactic:
⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩

Premises used: Pi.single, Set.Nonempty, And.intro, Exists.intro, Finset.sum
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst_3 a] (V a) ∧ x a ∈ V a
hVU : (↑t : Set ι).pi (α := M) V ⊆ U
refine_2 : ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑t : Set ι).pi (α := M) V
refine_2₁ :
  ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))
⊢ (U ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty

Tactic:
refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst_3 a] (V a) ∧ x a ∈ V a
hVU : (↑t : Set ι).pi (α := M) V ⊆ U
⊢ ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑t : Set ι).pi (α := M) V

Tactic:
simp_all [Finset.sum_pi_single]

Premises used: Finset.sum_pi_single
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst_3 a] (V a) ∧ x a ∈ V a
hVU : (↑t : Set ι).pi (α := M) V ⊆ U
⊢ ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))

Tactic:
sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Premises used: Set.mem_univ, Submodule.mem_iSup_of_mem, Submodule.mem_map_of_mem, sum_mem
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : Membership.mem (γ := Set ((i : ι) → M i)) (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i))) x
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst_3 a] (V a) ∧ x a ∈ V a
hVU : (↑t : Set ι).pi (α := M) V ⊆ U
⊢ ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))

Tactic:
exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Premises used: Set.mem_univ, Submodule.mem_iSup_of_mem, Submodule.mem_map_of_mem, sum_mem
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
inst_5 : ∀ (i : ι), ContinuousAdd.{u_3} (M i)
inst_6 : ∀ (i : ι), ContinuousConstSMul.{u_2, u_3} R (M i)
s : (i : ι) → Submodule R (M i)
⊢ Eq (α := Submodule R ((i : ι) → M i)) (topologicalClosure (⨆ (i : ι), map (LinearMap.single R M i) (s i)))
    (pi (φ := M) Set.univ fun (i : ι) ↦ (s i).topologicalClosure)

Tactic:
SetLike.coe_injective <| closure_coe_iSup_map_single _

Premises used: SetLike.coe_injective, Submodule.closure_coe_iSup_map_single
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
intro : ∀ (val : Fintype ι), Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
h :
  ∀ (x : ι → R),
    Eq.{u_3 + 1} (α := M) ((f : (a : ι → R) → M) x : M)
      (∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M) : M)
⊢ Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
x : ι → R
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ι → R) → M) x : M)
    (∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M) : M)

Tactic:
f.pi_apply_eq_sum_univ x

Premises used: LinearMap.pi_apply_eq_sum_univ
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
x : ι → R
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ι → R) → M) x : M)
    (∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M) : M)

Tactic:
exact f.pi_apply_eq_sum_univ x

Premises used: LinearMap.pi_apply_eq_sum_univ
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
⊢ Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)

Tactic:
have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
      ext x
      exact f.pi_apply_eq_sum_univ x
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
this :
  Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)
intro :
  Continuous[Pi.topologicalSpace, inst_5] fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
this :
  Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)
⊢ Continuous[Pi.topologicalSpace, inst_5] fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : TopologicalSpace M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val : Fintype ι
for :
  Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)
intro :
  ∀
    (this :
      Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
        ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)),
    Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
for₁ :
  Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
    ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)
intro₁ intro₂ :
  ∀
    (this :
      Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
        ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)),
    Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
intro₃ :
  ∀
    (this :
      Eq (α := (a : ι → R) → M) (⇑f : (a : ι → R) → M) fun (x : ι → R) ↦
        ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)),
    Continuous[Pi.topologicalSpace, inst_5] fun (x : ι → R) ↦
      ∑ i : ι, HSMul.hSMul (β := M) (x i) ((f : (a : ι → R) → M) fun (j : ι) ↦ if i = j then 1 else 0 : M)
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)

Tactic:
classical
    -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
    -- function.
    have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
      ext x
      exact f.pi_apply_eq_sum_univ x
    rw [this]
    fun_prop
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
M₁ : Type u_1
M₂ : Type u_2
R : Type u_4
S : Type u_5
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : Semiring R
inst_3 : Semiring S
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module S M₂
inst_8 : ContinuousConstSMul S M₂
inst_9 : ContinuousAdd M₂
σ : R →+* S
⊢ IsClosed[Pi.topologicalSpace] (Set.range (ι := M₁ →ₛₗ[σ] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))

Tactic:
isClosed_of_closure_subset fun f hf => ⟨linearMapOfMemClosureRangeCoe f hf, rfl⟩

Premises used: Exists.intro, isClosed_of_closure_subset, linearMapOfMemClosureRangeCoe, rfl
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : ContinuousAdd M
⊢ IsOpenMap (X := M) (Y := M ⧸ S) (⇑S.mkQ : (a : M) → M ⧸ S)

Tactic:
QuotientAddGroup.isOpenMap_coe

Premises used: Submodule.Quotient.mk, QuotientAddGroup.isOpenMap_coe, Submodule.quotientRel
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : ContinuousAdd M
⊢ IsOpenQuotientMap (X := M) (Y := M ⧸ S) (⇑S.mkQ : (a : M) → M ⧸ S)

Tactic:
QuotientAddGroup.isOpenQuotientMap_mk

Premises used: QuotientAddGroup.isOpenQuotientMap_mk, Submodule.Quotient.mk, Submodule.quotientRel
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
⊢ IsQuotientMap (X := M) (Y := M ⧸ S) (⇑S.mkQ : (a : M) → M ⧸ S)

Tactic:
isQuotientMap_quot_mk

Premises used: Submodule.Quotient.mk, Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
⊢ Continuous[inst_3, QuotientModule.Quotient.topologicalSpace S] (⇑S.mkQ : (a : M) → M ⧸ S)

Tactic:
continuous_quot_mk

Premises used: Submodule.Quotient.mk, Quotient, continuous_quot_mk, Quotient.mk'
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : IsTopologicalAddGroup M
⊢ IsTopologicalAddGroup.{u_2} (M ⧸ S)

Tactic:
inferInstanceAs <| IsTopologicalAddGroup (M ⧸ S.toAddSubgroup)

Premises used: _private.0.Submodule.topologicalAddGroup_quotient._proof_1
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup M
inst_6 : ContinuousSMul R M
rw :
  Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S]
    ((fun (p : Prod.{u_1, u_2} R (M ⧸ S)) ↦ p.1 • p.2) ∘ Prod.map id (⇑S.mkQ : (a : M) → M ⧸ S))
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S] fun (p : Prod.{u_1, u_2} R (M ⧸ S)) ↦
    p.1 • p.2

Tactic:
rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]

Premises used: Submodule.isOpenQuotientMap_mkQ, IsOpenQuotientMap.prodMap, IsOpenQuotientMap.id, IsOpenQuotientMap.continuous_comp_iff
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup M
inst_6 : ContinuousSMul R M
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S]
    ((fun (p : Prod.{u_1, u_2} R (M ⧸ S)) ↦ p.1 • p.2) ∘ Prod.map id (⇑S.mkQ : (a : M) → M ⧸ S))

Tactic:
continuous_quot_mk.comp continuous_smul

Premises used: Continuous.comp, Quotient, continuous_quot_mk, Quotient.mk', Quot.map, Quotient.map', ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup M
inst_6 : ContinuousSMul R M
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S]
    ((fun (p : Prod.{u_1, u_2} R (M ⧸ S)) ↦ p.1 • p.2) ∘ Prod.map id (⇑S.mkQ : (a : M) → M ⧸ S))

Tactic:
exact continuous_quot_mk.comp continuous_smul

Premises used: Continuous.comp, continuous_quot_mk, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
S : Submodule R M
inst_4 : IsTopologicalAddGroup M
inst_5 : IsClosed[inst_3] (↑S : Set M)
⊢ T3Space.{u_2} (M ⧸ S)

Tactic:
letI : IsClosed (S.toAddSubgroup : Set M) := ‹_›
  QuotientAddGroup.instT3Space S.toAddSubgroup

Premises used: QuotientAddGroup.instT3Space, Submodule.toAddSubgroup, Submodule.quotientRel
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
this :
  ∃ (f : (ℕ → Bool) → 𝕜),
    range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f
rcases : ∀ (f : (ℕ → Bool) → 𝕜) (f_inj : Injective f), 𝔠 ≤ #𝕜
⊢ 𝔠 ≤ #𝕜

Tactic:
rcases this with ⟨f, -, -, f_inj⟩
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : (ℕ → Bool) → 𝕜
f_inj : Injective f
⊢ 𝔠 ≤ #𝕜

Tactic:
simpa using lift_mk_le_lift_mk_of_injective f_inj

Premises used: Cardinal.lift_mk_le_lift_mk_of_injective
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
suffices :
  ∃ (f : (ℕ → Bool) → 𝕜),
    range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f
⊢ 𝔠 ≤ #𝕜

Tactic:
suffices ∃ f : (ℕ → Bool) → 𝕜, range f ⊆ univ ∧ Continuous f ∧ Injective f by
    rcases this with ⟨f, -, -, f_inj⟩
    simpa using lift_mk_le_lift_mk_of_injective f_inj
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
apply : Perfect.{u_1} (α := 𝕜) Set.univ
⊢ ∃ (f : (ℕ → Bool) → 𝕜),
    range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f

Tactic:
apply Perfect.exists_nat_bool_injection _ univ_nonempty

Premises used: Set.univ_nonempty, Perfect.exists_nat_bool_injection
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
⊢ Perfect.{u_1} (α := 𝕜) Set.univ

Tactic:
⟨isClosed_univ, preperfect_iff_nhds.2 (fun x _ U hU ↦ ?_)⟩

Premises used: isClosed_univ, Iff.mpr, preperfect_iff_nhds, Perfect.mk
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
refine : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → ∀ (U : Set 𝕜) (hU : U ∈ 𝓝 x), ∃ y ∈ U ∩ Set.univ, y ≠ x
⊢ Perfect.{u_1} (α := 𝕜) Set.univ

Tactic:
refine ⟨isClosed_univ, preperfect_iff_nhds.2 (fun x _ U hU ↦ ?_)⟩
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
rcases : ∀ (c : 𝕜) (c_pos : 0 < ‖c‖) (hc : ‖c‖ < 1), ∃ y ∈ U ∩ Set.univ, y ≠ x
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x

Tactic:
rcases NormedField.exists_norm_lt_one 𝕜 with ⟨c, c_pos, hc⟩

Premises used: NormedField.exists_norm_lt_one