awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
U₁ : (↑M : Set Eᵤ) + c ^ n • U ⊆ (↑M : Set Eᵤ) + c ^ n • ((↑M : Set Eᵤ) + c • U)
U₂ : (↑M : Set Eᵤ) + c ^ n • ((↑M : Set Eᵤ) + c • U) ⊆ (↑M : Set Eᵤ) + c ^ (n + 1) • U
⊢ U ⊆ (↑M : Set Eᵤ) + c ^ (n + 1) • U

Tactic:
calc
        U ⊆ M + c ^ n • U := ih
        _ ⊆ M + c ^ n • (M + c • U) := by gcongr
        _ ⊆ M + c ^ (n + 1) • U := by
          rw [smul_add, smul_smul, pow_succ, ← add_assoc]
          congr!
          lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
          simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]

Premises used: SetLike.coe, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
zero : U ⊆ (↑M : Set Eᵤ) + HPow.hPow (β := ℕ) c 0 • U
succ : ∀ (n : ℕ) (ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U), U ⊆ (↑M : Set Eᵤ) + c ^ (n + 1) • U
⊢ U ⊆ (↑M : Set Eᵤ) + c ^ n • U

Tactic:
induction n with
    | zero => simpa using fun x hx ↦ ⟨0, M.zero_mem, x, hx, zero_add x⟩
    | succ n ih =>
      calc
        U ⊆ M + c ^ n • U := ih
        _ ⊆ M + c ^ n • (M + c • U) := by gcongr
        _ ⊆ M + c ^ (n + 1) • U := by
          rw [smul_add, smul_smul, pow_succ, ← add_assoc]
          congr!
          lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
          simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]

Premises used: SetLike.coe, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
⊢ ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U

Tactic:
have h_ind (n : ℕ) : U ⊆ M + c ^ n • U := by
    induction n with
    | zero => simpa using fun x hx ↦ ⟨0, M.zero_mem, x, hx, zero_add x⟩
    | succ n ih =>
      calc
        U ⊆ M + c ^ n • U := ih
        _ ⊆ M + c ^ n • (M + c • U) := by gcongr
        _ ⊆ M + c ^ (n + 1) • U := by
          rw [smul_add, smul_smul, pow_succ, ← add_assoc]
          congr!
          lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
          simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
⊢ Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))

Tactic:
have h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets :=
    (TotallyBounded.isVonNBounded 𝕜 hU_tb).tendsto_smallSets_nhds.comp
    (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc1)
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
choose :
  ∀ (m : (n : ℕ) → Eᵤ) (hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)) (u : (n : ℕ) → Eᵤ) (hu : ∀ (n : ℕ), u n ∈ c ^ n • U)
    (h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x), x ∈ (↑M : Set Eᵤ)
⊢ x ∈ (↑M : Set Eᵤ)

Tactic:
choose m hm u hu h_eq using fun n ↦ h_ind n hx
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
W : Set Eᵤ
hW : Membership.mem (γ := Filter Eᵤ) (𝓝 0) W
⊢ W ∈ map u atTop

Tactic:
(tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.tendsto_smallSets_iff, Set.Subset, Filter.Eventually.mono, Set.preimage, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
W : Set Eᵤ
hW : Membership.mem (γ := Filter Eᵤ) (𝓝 0) W
⊢ W ∈ map u atTop

Tactic:
exact (tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)

Premises used: Filter.tendsto_smallSets_iff, Filter.Eventually.mono, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
⊢ Tendsto u atTop (𝓝 0)

Tactic:
have hu_tendsto : Tendsto u atTop (𝓝 0) := by
      intro W hW
      exact (tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
⊢ m = fun (n : ℕ) ↦ x - u n

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
⊢ Tendsto m atTop (𝓝 x)

Tactic:
simpa [show m = fun n ↦ x - u n by grind] using tendsto_const_nhds.sub hu_tendsto

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
⊢ Tendsto m atTop (𝓝 x)

Tactic:
have hm_tendsto : Tendsto m atTop (𝓝 x) := by
      simpa [show m = fun n ↦ x - u n by grind] using tendsto_const_nhds.sub hu_tendsto
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
hm_tendsto : Tendsto m atTop (𝓝 x)
⊢ x ∈ (↑M : Set Eᵤ)

Tactic:
M.closed_of_finiteDimensional.mem_of_tendsto hm_tendsto (Eventually.of_forall hm)

Premises used: Submodule.closed_of_finiteDimensional, IsClosed.mem_of_tendsto, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
x : Eᵤ
hx : x ∈ U
m : (n : ℕ) → Eᵤ
hm : ∀ (n : ℕ), m n ∈ (↑M : Set Eᵤ)
u : (n : ℕ) → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun (x1 x2 : Eᵤ) ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
hm_tendsto : Tendsto m atTop (𝓝 x)
⊢ x ∈ (↑M : Set Eᵤ)

Tactic:
exact M.closed_of_finiteDimensional.mem_of_tendsto hm_tendsto (Eventually.of_forall hm)

Premises used: Submodule.closed_of_finiteDimensional, IsClosed.mem_of_tendsto, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
⊢ U ⊆ (↑M : Set Eᵤ)

Tactic:
have hU_sub_M : U ⊆ M := by
    intro x hx
    choose m hm u hu h_eq using fun n ↦ h_ind n hx
    have hu_tendsto : Tendsto u atTop (𝓝 0) := by
      intro W hW
      exact (tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)
    have hm_tendsto : Tendsto m atTop (𝓝 x) := by
      simpa [show m = fun n ↦ x - u n by grind] using tendsto_const_nhds.sub hu_tendsto
    exact M.closed_of_finiteDimensional.mem_of_tendsto hm_tendsto (Eventually.of_forall hm)
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
hU_sub_M : U ⊆ (↑M : Set Eᵤ)
⊢ M = ⊤

Tactic:
have hM_top : M = ⊤ := absorbent_nhds_zero (𝕜 := 𝕜) hU_nhds |>.mono hU_sub_M |>.submodule_eq_top
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
hU_sub_M : U ⊆ (↑M : Set Eᵤ)
hM_top : M = ⊤
x : Eᵤ
⊢ x ∈ M

Tactic:
simp [hM_top]
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
h_ind : ∀ (n : ℕ), U ⊆ (↑M : Set Eᵤ) + c ^ n • U
h_small : Tendsto.{0, u_6} (β := Set Eᵤ) (fun (n : ℕ) ↦ c ^ n • U) atTop (smallSets (𝓝 0))
hU_sub_M : U ⊆ (↑M : Set Eᵤ)
hM_top : M = ⊤
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
exact FiniteDimensional.of_surjective M.subtype fun x ↦ ⟨⟨x, by simp [hM_top]⟩, rfl⟩

Premises used: FiniteDimensional.of_surjective, Subtype.mk, Exists.intro, Submodule.subtype, rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 x
hU_tb : TotallyBounded U
⊢ x +ᵥ -x +ᵥ U ∈ 𝓝 x

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 x
hU_tb : TotallyBounded U
⊢ x +ᵥ -x +ᵥ U ∈ 𝓝 x

Tactic:
replace hU_nhds : x +ᵥ (-x) +ᵥ U ∈ 𝓝 x := by simpa
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : x +ᵥ -x +ᵥ U ∈ 𝓝 x
⊢ Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)

Tactic:
rw [vadd_mem_nhds_self] at hU_nhds

Premises used: vadd_mem_nhds_self
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
.of_totallyBounded_nhds_zero _ hU_nhds ?_

Premises used: FiniteDimensional.of_totallyBounded_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
refine : TotallyBounded (-x +ᵥ U)
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
refine .of_totallyBounded_nhds_zero _ hU_nhds ?_
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
⊢ -x +ᵥ U = (fun (x_1 : Eᵤ) ↦ x_1 - x) '' U

Tactic:
simp [← Set.image_vadd, neg_add_eq_sub]

Premises used: neg_add_eq_sub, Set.image_vadd
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
⊢ -x +ᵥ U = (fun (x_1 : Eᵤ) ↦ x_1 - x) '' U

Tactic:
have : -x +ᵥ U = (· - x) '' U := by simp [← Set.image_vadd, neg_add_eq_sub]
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
this : -x +ᵥ U = (fun (x_1 : Eᵤ) ↦ x_1 - x) '' U
⊢ TotallyBounded (-x +ᵥ U)

Tactic:
this ▸ hU_tb.image (uniformContinuous_id.sub uniformContinuous_const)

Premises used: Eq.rec, TotallyBounded.image, uniformContinuous_id, uniformContinuous_const, UniformContinuous.sub, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
this : -x +ᵥ U = (fun (x_1 : Eᵤ) ↦ x_1 - x) '' U
⊢ TotallyBounded (-x +ᵥ U)

Tactic:
exact this ▸ hU_tb.image (uniformContinuous_id.sub uniformContinuous_const)
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
h : ∃ (x : Eᵤ), ∃ U ∈ 𝓝 x, TotallyBounded U
rcases : ∀ (x : Eᵤ) (U : Set Eᵤ) (hU_nhds : U ∈ 𝓝 x) (hU_tb : TotallyBounded U), FiniteDimensional 𝕜 Eᵤ
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
rcases h with ⟨x, U, hU_nhds, hU_tb⟩