awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + (↑u : R) • x ∈ s
hy' : y ∈ s
⊢ x ∈ s
have rwa : ∀ (hu : (↑u : R) • x ∈ s) (hy' : y ∈ s), x ∈ s
Tactic: rwa [s.add_mem_iff_right hy', ← Units.smul_def, s.smul_mem_iff' u] at hu
Cleared hypotheses: hu, hy'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + (↑u : R) • x ∈ s
hy' : y ∈ s
rwa : ∀ (hu : (↑u : R) • x ∈ s) (hy' : y ∈ s), x ∈ s
⊢ x ∈ s
have rwa₁ : ∀ (hu : u • x ∈ s) (hy' : y ∈ s), x ∈ s
Tactic: rwa [s.add_mem_iff_right hy', ← Units.smul_def, s.smul_mem_iff' u] at hu
Cleared hypotheses: hu, hy'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + (↑u : R) • x ∈ s
hy' : y ∈ s
rwa : ∀ (hu : (↑u : R) • x ∈ s) (hy' : y ∈ s), x ∈ s
rwa₁ : ∀ (hu : u • x ∈ s) (hy' : y ∈ s), x ∈ s
⊢ x ∈ s
have rwa₂ : ∀ (hu : x ∈ s) (hy' : y ∈ s), x ∈ s
Tactic: rwa [s.add_mem_iff_right hy', ← Units.smul_def, s.smul_mem_iff' u] at hu
Cleared hypotheses: hu, hy'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x : M
⊢ (𝓝[≠] x).NeBot
have rcases : ∀ (y : M) (hy : y ≠ 0), (𝓝[≠] x).NeBot
Tactic: rcases exists_ne (0 : M) with ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ (𝓝[≠] x).NeBot
have suffices : Tendsto (fun (c : R) ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)
Tactic: suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun (c : R) ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)
have refine_1 : Tendsto (fun (c : R) ↦ x + c • y) (𝓝 0) (𝓝 x)
Tactic: refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
refine_1 : Tendsto (fun (c : R) ↦ x + c • y) (𝓝 0) (𝓝 x)
⊢ Tendsto (fun (c : R) ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)
have refine_2 : ∀ (a : R), Membership.mem (γ := Set R) {0}ᶜ a → Membership.mem (γ := Set M) {x}ᶜ (x + a • y)
Tactic: refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun (c : R) ↦ x + c • y) (𝓝 0) (𝓝 x)
have h : x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 y
Tactic: convert! tendsto_const_nhds.add ((@tendsto_id R _).smul_const y)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 y
have h : x = x + 0
Tactic: rw [zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
h : x = x + 0
⊢ x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 y
have h₁ : x = x
Tactic: rw [zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
⊢ IsSeparable (↑(Submodule.span R s) : Set M)
have rw : IsSeparable.{u_2} (α := M)
  (⋃ (n : ℕ),
    (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
Tactic: rw [Submodule.span_eq_iUnion_nat]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
⊢ IsSeparable.{u_2} (α := M)
    (⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
have refine_1 : ∀ (n : ℕ), IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
Tactic: refine .iUnion fun n ↦ .image ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
refine_1 : ∀ (n : ℕ), IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
⊢ IsSeparable.{u_2} (α := M)
    (⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
have refine_2 : ∀ (n : ℕ), Continuous[Pi.topologicalSpace, inst_3] fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2
Tactic: refine .iUnion fun n ↦ .image ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
have this : IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ SProd.sprod (α := Set R) Set.univ s}
Tactic: have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
      apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
this : IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ SProd.sprod (α := Set R) Set.univ s}
⊢ IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
have refine_1 : ∀
  (this :
    IsSeparable (α := Fin n → R × M)
      {f : Fin n → R × M | ∀ (i : Fin n), Membership.mem (γ := Set (R × M)) (Prod.snd ⁻¹' s) (f i)}),
  IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
Tactic: rwa [Set.univ_prod] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ Continuous[Pi.topologicalSpace, inst_3] fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2
have apply : ∀ (i : Fin n),
  Membership.mem (γ := Finset (Fin n)) Finset.univ i →
    Continuous[Pi.topologicalSpace, inst_3] fun (a : Fin n → R × M) ↦ (a i).1 • (a i).2
Tactic: apply continuous_finsetSum _ (fun i _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
⊢ Dense (↑s : Set M) ↔ s.topologicalClosure = ⊤
have rw : closure[inst_1] (↑s : Set M) = Set.univ ↔ (↑s.topologicalClosure : Set M) = (↑⊤ : Set M)
Tactic: rw [← SetLike.coe_set_eq, dense_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ IsClosed[inst_1] (↑s : Set M) ∨ Dense (↑s : Set M)
have refine : s.topologicalClosure = s → IsClosed[inst_1] (↑s : Set M)
Tactic: refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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)) =
    Set.pi (α := M) Set.univ fun (i : ι) ↦ closure[inst_3 i] (↑(s i) : Set (M i))
have rw : 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: rw [← closure_pi_set]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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)))
have 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))
Tactic: refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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))
⊢ 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)))
have 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))
Tactic: refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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)
⊢ (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))
have 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
Tactic: simp only [Set.subset_def, mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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
⊢ (U ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty
have 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
Tactic: rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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
have refine_2 : ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑t : Set ι).pi (α := M) V
Tactic: refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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
⊢ (U ∩ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))).Nonempty
have refine_2₁ : ∑ i ∈ t, Pi.single (M := M) i (x i) ∈ (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i))
Tactic: refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
have intro : ∀ (val : Fintype ι), Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (hypothesis)
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 ι
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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] (⇑f : (a : ι → R) → M)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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 ι
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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)
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
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)
⊢ Continuous[Pi.topologicalSpace, inst_5] (⇑f : (a : ι → R) → M)
have 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)
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