awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
⊢ 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)
-- 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
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 (x + 0))
⊢ Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)

Tactic:
rw [add_zero] at A

Premises used: add_zero
-- 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
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun (n : ℕ) ↦ x + c ^ n) atTop (𝓝 x)
⊢ ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U

Tactic:
have B : ∀ᶠ n in atTop, x + c ^ n ∈ U := tendsto_def.1 A 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
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
rcases : ∀ (n : ℕ) (hn : x + c ^ n ∈ U), ∃ y ∈ U ∩ Set.univ, y ≠ x
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x

Tactic:
rcases B.exists with ⟨n, hn⟩

Premises used: Filter.Eventually.exists
-- 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
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 ∈ U ∩ Set.univ

Tactic:
simpa using hn
-- 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
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
refine : x + c ^ n ≠ x
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x

Tactic:
refine ⟨x + c^n, by simpa using hn, ?_⟩
-- 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
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
simp : c ^ n ≠ 0
⊢ x + c ^ n ≠ x

Tactic:
simp only [add_ne_left]

Premises used: add_ne_left
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
x : 𝕜
h_1 : 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
h : c ≠ 0
⊢ c ^ n ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- 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
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 ≠ 0

Tactic:
simpa using c_pos
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
⊢ lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜

Tactic:
simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜

Premises used: continuum_le_cardinal_of_nontriviallyNormedField
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
⊢ lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜

Tactic:
have A : lift.{v} (𝔠 : Cardinal.{u}) ≤ lift.{v} (#𝕜) := by
    simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜
⊢ 𝔠 ≤ #E

Tactic:
simpa using A.trans (Cardinal.mk_le_of_module 𝕜 E)

Premises used: Cardinal.mk_le_of_module, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
NormedField.exists_lt_norm 𝕜 1

Premises used: NormedField.exists_lt_norm, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
obtain : ∀ (c : 𝕜) (hc : 1 < ‖c‖), #(↑s : Type u_1) = #E
⊢ #(↑s : Type u_1) = #E

Tactic:
obtain ⟨c, hc⟩ : ∃ x : 𝕜, 1 < ‖x‖ := NormedField.exists_lt_norm 𝕜 1

Premises used: NormedField.exists_lt_norm, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
h : c ≠ 0
⊢ c ^ n ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
⊢ LT.lt (α := ℝ) 1 0

Tactic:
simp only [norm_zero] at hc

Premises used: norm_zero
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : LT.lt (α := ℝ) 1 0
⊢ False

Tactic:
lt_irrefl _ (hc.trans zero_lt_one)

Premises used: lt_irrefl, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : LT.lt (α := ℝ) 1 0
⊢ False

Tactic:
exact lt_irrefl _ (hc.trans zero_lt_one)

Premises used: lt_irrefl, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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

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)
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
simp_rw : Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ c⁻¹ ^ n) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ (c ^ n)⁻¹) atTop (𝓝 0)

Tactic:
simp_rw [← inv_pow]

Premises used: inv_pow
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
h : ‖c⁻¹‖ < 1
⊢ Tendsto.{0, u_2} (β := 𝕜) (fun (n : ℕ) ↦ c⁻¹ ^ n) atTop (𝓝 0)

Tactic:
apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one

Premises used: tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
h : ‖c‖⁻¹ < 1
⊢ ‖c⁻¹‖ < 1

Tactic:
rw [norm_inv]

Premises used: norm_inv
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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

Tactic:
inv_lt_one_of_one_lt₀ hc

Premises used: inv_lt_one_of_one_lt₀
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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

Tactic:
exact inv_lt_one_of_one_lt₀ hc

Premises used: inv_lt_one_of_one_lt₀
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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)

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
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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_2} (β := 𝕜) (fun (n : ℕ) ↦ (c ^ n)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) 0 x))

Tactic:
Tendsto.smul_const this x

Premises used: Filter.Tendsto.smul_const
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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_2} (β := 𝕜) (fun (n : ℕ) ↦ (c ^ n)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) 0 x))

Tactic:
exact Tendsto.smul_const this x

Premises used: Filter.Tendsto.smul_const
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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))

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
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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))
⊢ Tendsto.{0, u_1} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)

Tactic:
rw [zero_smul] at this

Premises used: zero_smul
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
h : ∀ (hn : (c ^ n)⁻¹ • x ∈ s), x ∈ c ^ n • s
⊢ Membership.mem (γ := Set ℕ) ((fun (n : ℕ) ↦ (c ^ n)⁻¹ • x) ⁻¹' s) n → x ∈ c ^ n • s

Tactic:
(hn : (c ^ n)⁻¹ • x ∈ s)
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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)
h : ∀ (n : ℕ) (hn : (c ^ n)⁻¹ • x ∈ s), x ∈ c ^ n • s
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s

Tactic:
filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
hn : (c ^ n)⁻¹ • x ∈ s
⊢ x ∈ c ^ n • s

Tactic:
(mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn

Premises used: Iff.mpr, Set.Mem, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
hn : (c ^ n)⁻¹ • x ∈ s
⊢ x ∈ c ^ n • s

Tactic:
exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn

Premises used: Iff.mpr, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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

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
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
x : (↑(c ^ n • s) : Type u_1)
⊢ (fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ c ^ n • s) (c ^ n • (↑x : E)) ⋯)
      ((fun (x : (↑(c ^ n • s) : Type u_1)) ↦
          (Subtype.mk (p := fun (x : E) ↦ x ∈ s) ((c ^ n)⁻¹ • (↑x : E)) ⋯ : { x : E // x ∈ s }))
        x) =
    x

Tactic:
simp [smul_smul, mul_inv_cancel₀ (cn_ne n)]

Premises used: mul_inv_cancel₀, smul_smul
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
x : (↑s : Type u_1)
⊢ (fun (x : (↑(c ^ n • s) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : E) ↦ x ∈ s) ((c ^ n)⁻¹ • (↑x : E)) ⋯ : { x : E // x ∈ s }))
      ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ c ^ n • s) (c ^ n • (↑x : E)) ⋯) x) =
    x

Tactic:
simp [smul_smul, inv_mul_cancel₀ (cn_ne n)]

Premises used: smul_smul, inv_mul_cancel₀
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
have : ∀ (this : (↑(c ^ n • s) : Type u_1) ≃ (↑s : Type u_1)), #(↑(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)] }
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
this : (↑(c ^ n • s) : Type u_1) ≃ (↑s : Type u_1)
⊢ #(↑(c ^ n • s) : Type u_1) = #(↑s : Type u_1)

Tactic:
Cardinal.mk_congr this

Premises used: Cardinal.mk_congr
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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 : ℕ
this : (↑(c ^ n • s) : Type u_1) ≃ (↑s : Type u_1)
⊢ #(↑(c ^ n • s) : Type u_1) = #(↑s : Type u_1)

Tactic:
exact Cardinal.mk_congr this

Premises used: Cardinal.mk_congr
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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)

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
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
B : ∀ (n : ℕ), #(↑(c ^ n • s) : Type u_1) = #(↑s : Type u_1)
⊢ #(↑s : Type u_1) = #E

Tactic:
apply (Cardinal.mk_of_countable_eventually_mem A B).symm

Premises used: Cardinal.mk_of_countable_eventually_mem, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
⊢ Membership.mem (γ := Filter E) (𝓝 ((g : (a : E) → E) 0) : Filter E) s

Tactic:
simpa [g] using hs
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
have : t ∈ 𝓝 0 := g.continuous.continuousAt.preimage_mem_nhds (by simpa [g] using hs)
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
⊢ #(↑t : Type u_1) = #E

Tactic:
have A : #t = #E := cardinal_eq_of_mem_nhds_zero 𝕜 this
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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
⊢ #(↑t : Type u_1) = #(↑s : Type u_1)

Tactic:
have B : #t = #s := Cardinal.mk_subtype_of_equiv (· ∈ s) g.toEquiv
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (A : #(↑s : Type u_1) = #E) (B : #(↑t : Type u_1) = #(↑s : Type u_1)), #(↑s : Type u_1) = #E
⊢ #(↑s : Type u_1) = #E

Tactic:
rwa [B] at A