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 : 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
have 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))
Tactic: rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
this :
  ∃ (f : (ℕ → Bool) → 𝕜),
    range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f
⊢ 𝔠 ≤ #𝕜
have rcases : ∀ (f : (ℕ → Bool) → 𝕜) (f_inj : Injective f), 𝔠 ≤ #𝕜
Tactic: rcases this with ⟨f, -, -, f_inj⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
⊢ 𝔠 ≤ #𝕜
have 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
⊢ ∃ (f : (ℕ → Bool) → 𝕜),
    range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f
have apply : Perfect.{u_1} (α := 𝕜) Set.univ
Tactic: apply Perfect.exists_nat_bool_injection _ univ_nonempty
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
⊢ Perfect.{u_1} (α := 𝕜) Set.univ
have refine : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → ∀ (U : Set 𝕜) (hU : U ∈ 𝓝 x), ∃ y ∈ U ∩ Set.univ, y ≠ x
Tactic: refine ⟨isClosed_univ, preperfect_iff_nhds.2 (fun x _ U hU ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
have rcases : ∀ (c : 𝕜) (c_pos : 0 < ‖c‖) (hc : ‖c‖ < 1), ∃ y ∈ U ∩ Set.univ, y ≠ x
Tactic: rcases NormedField.exists_norm_lt_one 𝕜 with ⟨c, c_pos, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
have A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 (x + 0))
Tactic: have A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 (x + 0)) :=
    tendsto_const_nhds.add (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 (x + 0))
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
have A₁ : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
Tactic: rw [add_zero] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
have B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
Tactic: have B : ∀ᶠ n in atTop, x + c ^ n ∈ U := tendsto_def.1 A U hU
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
have rcases : ∀ (n : ℕ) (hn : x + c ^ n ∈ U), ∃ y ∈ U ∩ Set.univ, y ≠ x
Tactic: rcases B.exists with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
have refine : x + c ^ n ≠ x
Tactic: refine ⟨x + c^n, by simpa using hn, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ≠ x
have simp : c ^ n ≠ 0
Tactic: simp only [add_ne_left]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h : Membership.mem (γ := Set 𝕜) Set.univ x
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ c ^ n ≠ 0
have h : c ≠ 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
⊢ 𝔠 ≤ #E
have A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜
Tactic: have A : lift.{v} (𝔠 : Cardinal.{u}) ≤ lift.{v} (#𝕜) := by
    simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ #(↑s : Type u_1) = #E
have obtain : ∀ (c : 𝕜) (hc : 1 < ‖c‖), #(↑s : Type u_1) = #E
Tactic: obtain ⟨c, hc⟩ : ∃ x : 𝕜, 1 < ‖x‖ := NormedField.exists_lt_norm 𝕜 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ c ^ n ≠ 0
have h : c ≠ 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
n : ℕ
hc : 1 < norm.{u_2} (E := 𝕜) 0
⊢ False
have hc₁ : LT.lt (α := ℝ) 1 0
Tactic: simp only [norm_zero] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
⊢ #(↑s : Type u_1) = #E
have cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
Tactic: have cn_ne : ∀ n, c ^ n ≠ 0 := by
    intro n
    apply pow_ne_zero
    rintro rfl
    simp only [norm_zero] at hc
    exact lt_irrefl _ (hc.trans zero_lt_one)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ (c ^ n)⁻¹) atTop (𝓝 0)
have simp_rw : Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ c⁻¹ ^ n) atTop (𝓝 0)
Tactic: simp_rw [← inv_pow]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ c⁻¹ ^ n) atTop (𝓝 0)
have h : ‖c⁻¹‖ < 1
Tactic: apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ‖c⁻¹‖ < 1
have h : ‖c‖⁻¹ < 1
Tactic: rw [norm_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) 0 x))
have this : Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ (c ^ n)⁻¹) atTop (𝓝 0)
Tactic: have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
        simp_rw [← inv_pow]
        apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
        rw [norm_inv]
        exact inv_lt_one_of_one_lt₀ hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
have this : Tendsto (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) 0 x))
Tactic: have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) := by
      have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
        simp_rw [← inv_pow]
        apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
        rw [norm_inv]
        exact inv_lt_one_of_one_lt₀ hc
      exact Tendsto.smul_const this x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) 0 x))
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
have this₁ : Tendsto.{0, u_1} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)
Tactic: rw [zero_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto.{0, u_1} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)
n : ℕ
⊢ Membership.mem (γ := Set ℕ) ((fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) ⁻¹' s) n → x ∈ c ^ n • s
have h : ∀ (hn : (c ^ n)⁻¹ • x ∈ s), x ∈ c ^ n • s
Tactic: (hn : (c ^ n)⁻¹ • x ∈ s)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto.{0, u_1} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
have h : ∀ (n : ℕ) (hn : (c ^ n)⁻¹ • x ∈ s), x ∈ c ^ n • s
Tactic: filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
⊢ #(↑s : Type u_1) = #E
have A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
Tactic: have A : ∀ (x : E), ∀ᶠ n in (atTop : Filter ℕ), x ∈ c ^ n • s := by
    intro x
    have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) := by
      have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
        simp_rw [← inv_pow]
        apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
        rw [norm_inv]
        exact inv_lt_one_of_one_lt₀ hc
      exact Tendsto.smul_const this x
    rw [zero_smul] at this
    filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
    exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
n : ℕ
⊢ #(↑(c ^ n • s) : Type u_1) = #(↑s : Type u_1)
have have : ∀ (this : (↑(c ^ n • s) : Type u_1) ≃ (↑s : Type u_1)), #(↑(c ^ n • s) : Type u_1) = #(↑s : Type u_1)
Tactic: have : (c ^ n • s :) ≃ s :=
    { toFun := fun x ↦ ⟨(c ^ n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩
      invFun := fun x ↦ ⟨(c^n) • x.1, smul_mem_smul_set x.2⟩
      left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel₀ (cn_ne n)]
      right_inv := fun x ↦ by simp [smul_smul, inv_mul_cancel₀ (cn_ne n)] }
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Zero E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
⊢ #(↑s : Type u_1) = #E
have B : ∀ (n : ℕ), #(↑(c ^ n • s) : Type u_1) = #(↑s : Type u_1)
Tactic: have B : ∀ n, #(c ^ n • s :) = #s := by
    intro n
    have : (c ^ n • s :) ≃ s :=
    { toFun := fun x ↦ ⟨(c ^ n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩
      invFun := fun x ↦ ⟨(c^n) • x.1, smul_mem_smul_set x.2⟩
      left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel₀ (cn_ne n)]
      right_inv := fun x ↦ by simp [smul_smul, inv_mul_cancel₀ (cn_ne n)] }
    exact Cardinal.mk_congr this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := (⇑g : (a : E) → E) ⁻¹' s
⊢ #(↑s : Type u_1) = #E
have this : Membership.mem (γ := Filter E) (𝓝 0) t
Tactic: have : t ∈ 𝓝 0 := g.continuous.continuousAt.preimage_mem_nhds (by simpa [g] using hs)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := (⇑g : (a : E) → E) ⁻¹' s
this : Membership.mem (γ := Filter E) (𝓝 0) t
⊢ #(↑s : Type u_1) = #E
have A : #(↑t : Type u_1) = #E
Tactic: have A : #t = #E := cardinal_eq_of_mem_nhds_zero 𝕜 this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (hypothesis)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := (⇑g : (a : E) → E) ⁻¹' s
this : Membership.mem (γ := Filter E) (𝓝 0) t
A : #(↑t : Type u_1) = #E
⊢ #(↑s : Type u_1) = #E
have B : #(↑t : Type u_1) = #(↑s : Type u_1)
Tactic: have B : #t = #s := Cardinal.mk_subtype_of_equiv (· ∈ s) g.toEquiv
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := (⇑g : (a : E) → E) ⁻¹' s
this : Membership.mem (γ := Filter E) (𝓝 0) t
A : #(↑t : Type u_1) = #E
B : #(↑t : Type u_1) = #(↑s : Type u_1)
⊢ #(↑s : Type u_1) = #E
have rwa : ∀ (A : #(↑s : Type u_1) = #E) (B : #(↑t : Type u_1) = #(↑s : Type u_1)), #(↑s : Type u_1) = #E
Tactic: rwa [B] at A
Cleared hypotheses: A, B
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst_3] s
h's : s.Nonempty
⊢ #(↑s : Type u_1) = #E
have rcases : ∀ (x : E) (hx : x ∈ s), #(↑s : Type u_1) = #E
Tactic: rcases h's with ⟨x, hx⟩
Cleared hypotheses: h's
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ Dense sᶜ
have rw : interior s = ∅
Tactic: rw [← interior_eq_empty_iff_dense_compl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ interior s = ∅
have by_contra : ∀ (H : ¬interior s = ∅), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Cardinality (goal)
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ False
have apply : ℵ₀ < ℵ₀
Tactic: apply lt_irrefl (ℵ₀ : Cardinal.{u})
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s t : ClosedSubmodule R M
h : (↑s : Submodule R M) = (↑t : Submodule R M)
⊢ s = t
have mk : ∀ (toSubmodule : Submodule R M) (isClosed' : IsClosed toSubmodule.carrier)
  (h :
    (↑{ toSubmodule := toSubmodule, isClosed' := isClosed' : ClosedSubmodule R M } : Submodule R M) =
      (↑t : Submodule R M)),
  { toSubmodule := toSubmodule, isClosed' := isClosed' : ClosedSubmodule R M } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
f : ι → ClosedSubmodule R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑(⨅ (i : ι), f i) : Submodule R M) (⨅ (i : ι), (↑(f i) : Submodule R M))
have rw : Eq.{u_3 + 1} (α := Submodule R M) (↑(sInf (Set.range fun (i : ι) ↦ f i)) : Submodule R M)
  (⨅ (i : ι), (↑(f i) : Submodule R M))
Tactic: rw [iInf, toSubmodule_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
f : ι → ClosedSubmodule R M
rw :
  Eq.{u_3 + 1} (α := Submodule R M) (↑(sInf (Set.range fun (i : ι) ↦ f i)) : Submodule R M)
    (⨅ (i : ι), (↑(f i) : Submodule R M))
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑(⨅ (i : ι), f i) : Submodule R M) (⨅ (i : ι), (↑(f i) : Submodule R M))
have rw₁ : Eq.{u_3 + 1} (α := Submodule R M)
  (⨅ (s : ClosedSubmodule R M),
    ⨅ (_ : Membership.mem (γ := Set (ClosedSubmodule R M)) (Set.range fun (i : ι) ↦ f i) s), (↑s : Submodule R M))
  (⨅ (i : ι), (↑(f i) : Submodule R M))
Tactic: rw [iInf, toSubmodule_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
f : ι → ClosedSubmodule R M
rw :
  Eq.{u_3 + 1} (α := Submodule R M) (↑(sInf (Set.range fun (i : ι) ↦ f i)) : Submodule R M)
    (⨅ (i : ι), (↑(f i) : Submodule R M))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨅ (s : ClosedSubmodule R M),
      ⨅ (_ : Membership.mem (γ := Set (ClosedSubmodule R M)) (Set.range fun (i : ι) ↦ f i) s), (↑s : Submodule R M))
    (⨅ (i : ι), (↑(f i) : Submodule R M))
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑(⨅ (i : ι), f i) : Submodule R M) (⨅ (i : ι), (↑(f i) : Submodule R M))
have rw₂ : Eq.{u_3 + 1} (α := Submodule R M) (⨅ (i : ι), (↑(f i) : Submodule R M)) (⨅ (i : ι), (↑(f i) : Submodule R M))
Tactic: rw [iInf, toSubmodule_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
⊢ (↑s : Submodule R M).closure = s
have carrier : ∀ (x : M), x ∈ (↑(↑s : Submodule R M).closure : Submodule R M).carrier ↔ x ∈ (↑s : Submodule R M).carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
x : M
⊢ x ∈ closure (↑s : Set M) ↔ x ∈ s
have carrier : x ∈ (↑s : Set M) ↔ x ∈ s
Tactic: rw [closure_eq_iff_isClosed.mpr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
x : M
carrier : x ∈ (↑s : Set M) ↔ x ∈ s
⊢ x ∈ closure (↑s : Set M) ↔ x ∈ s
have carrier₁ : IsClosed (↑s : Set M)
Tactic: rw [closure_eq_iff_isClosed.mpr]