awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)
have hxy : ∀ (c : 𝕜ˣ) (hc0 : 0 < ‖(↑c : 𝕜)‖) (hc1 : ‖(↑c : 𝕜)‖ < 1) (hc_ne : (↑c : 𝕜) ≠ 0)
  (hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ (↑c : 𝕜) • U) (h_cover : U ⊆ (↑M : Set Eᵤ) + (↑c : 𝕜) • U)
  (ih : U ⊆ (↑M : Set Eᵤ) + (↑c : 𝕜) ^ n • U), (↑M : Set Eᵤ) + (↑c : 𝕜) ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)
Tactic: lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
Cleared hypotheses: c, hc0, hc1, hc_ne, hF_cover, h_cover, ih
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 + 1) • U
have U₁ : (↑M : Set Eᵤ) + c ^ n • U ⊆ (↑M : Set Eᵤ) + c ^ n • ((↑M : Set Eᵤ) + c • 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 + 1) • U
have U₂ : (↑M : Set Eᵤ) + c ^ n • ((↑M : Set Eᵤ) + c • 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
have zero : U ⊆ (↑M : Set Eᵤ) + HPow.hPow (β := ℕ) c 0 • 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ U ⊆ (↑M : Set Eᵤ) + c ^ n • U
have succ : ∀ (n : ℕ) (ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U), U ⊆ (↑M : Set Eᵤ) + c ^ (n + 1) • 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ FiniteDimensional 𝕜 Eᵤ
have h_ind : ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ FiniteDimensional 𝕜 Eᵤ
have h_small : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ x ∈ (↑M : Set Eᵤ)
have 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ᵤ)
Tactic: choose m hm u hu h_eq using fun n ↦ h_ind n hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ x ∈ (↑M : Set Eᵤ)
have hu_tendsto : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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)
⊢ x ∈ (↑M : Set Eᵤ)
have hm_tendsto : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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))
⊢ FiniteDimensional 𝕜 Eᵤ
have hU_sub_M : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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ᵤ)
⊢ FiniteDimensional 𝕜 Eᵤ
have hM_top : M = ⊤
Tactic: have hM_top : M = ⊤ := absorbent_nhds_zero (𝕜 := 𝕜) hU_nhds |>.mono hU_sub_M |>.submodule_eq_top
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ FiniteDimensional 𝕜 Eᵤ
have hU_nhds₁ : x +ᵥ -x +ᵥ U ∈ 𝓝 x
Tactic: replace hU_nhds : x +ᵥ (-x) +ᵥ U ∈ 𝓝 x := by simpa
Cleared hypotheses: hU_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ FiniteDimensional 𝕜 Eᵤ
have hU_nhds₁ : Membership.mem (γ := Filter Eᵤ) (𝓝 0) (-x +ᵥ U)
Tactic: rw [vadd_mem_nhds_self] at hU_nhds
Cleared hypotheses: hU_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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ᵤ
have refine : TotallyBounded (-x +ᵥ U)
Tactic: refine .of_totallyBounded_nhds_zero _ hU_nhds ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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)
⊢ TotallyBounded (-x +ᵥ U)
have this : -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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ FiniteDimensional 𝕜 Eᵤ
have rcases : ∀ (x : Eᵤ) (U : Set Eᵤ) (hU_nhds : U ∈ 𝓝 x) (hU_tb : TotallyBounded U), FiniteDimensional 𝕜 Eᵤ
Tactic: rcases h with ⟨x, U, hU_nhds, hU_tb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
φ : E ⧸ p →L[𝕜] ↥q :=
  ((LinearMap.toContinuousLinearMap : (E ⧸ p →ₗ[𝕜] ↥q) ≃ₗ[𝕜] E ⧸ p →L[𝕜] ↥q) : (a : E ⧸ p →ₗ[𝕜] ↥q) → E ⧸ p →L[𝕜] ↥q)
    (↑(p.quotientEquivOfIsCompl q h) : E ⧸ p →ₗ[𝕜] ↥q)
⊢ IsTopCompl p q
have this : IsTopCompl q (↑(φ ∘SL p.mkQL) : E →ₗ[𝕜] ↥q).ker
Tactic: have := (φ ∘L p.mkQL).isTopCompl_of_proj fun x ↦ by simp [φ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 ↥q
⊢ IsTopCompl p q
have suffices : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
Tactic: suffices FiniteDimensional 𝕜 (E ⧸ p) from h.isTopCompl_of_finiteDimensional_quotient hp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
p : Submodule 𝕜 E
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
⊢ p.ClosedComplemented
have obtain : ∀ (q : Submodule 𝕜 E) (hq : IsCompl p q), p.ClosedComplemented
Tactic: obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
hA : A.ClosedComplemented
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
⊢ B.ClosedComplemented
have obtain : ∀ (p : E →L[𝕜] ↥A) (hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x), B.ClosedComplemented
Tactic: obtain ⟨p, hp⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x
⊢ B.ClosedComplemented
have obtain : ∀ (C : Submodule 𝕜 E) (hBC : IsCompl B C), B.ClosedComplemented
Tactic: obtain ⟨C, hBC⟩ := B.exists_isCompl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x
C : Submodule 𝕜 E
hBC : IsCompl B C
⊢ B.ClosedComplemented
have refine : ∀ (x : ↥B),
  (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (((LinearMap.toContinuousLinearMap : (↥A →ₗ[𝕜] ↥B) ≃ₗ[𝕜] ↥A →L[𝕜] ↥B) : (a : ↥A →ₗ[𝕜] ↥B) → ↥A →L[𝕜] ↥B)
            ((B.projectionOnto C hBC).domRestrict A))
          p :
        (a : E) → ↥B)
      (↑x : E) =
    x
Tactic: refine ⟨((projectionOnto B C hBC).domRestrict A).toContinuousLinearMap ∘SL p, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜 F
inst_10 : T2Space F
f : E →L[𝕜] F
inst_11 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : E →ₗ[𝕜] F).range
⊢ (↑f : E →ₗ[𝕜] F).ker.ClosedComplemented
have suffices : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ (↑f : E →ₗ[𝕜] F).ker)
Tactic: suffices FiniteDimensional 𝕜 (E ⧸ f.ker) from .of_finiteDimensional_quotient f.isClosed_ker
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
⊢ IsLinearMap 𝕜 (M₂ := F →L[𝕜] G) fun (x : E) ↦
    ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G) ((f : (a : E) → F →ₗ[𝕜] G) x)
have map_add : ∀ (x y : E),
  ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
      ((f : (a : E) → F →ₗ[𝕜] G) (x + y)) =
    HAdd.hAdd (α := F →L[𝕜] G) (β := F →L[𝕜] G)
      (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
          ((f : (a : E) → F →ₗ[𝕜] G) x) :
        F →L[𝕜] G)
      (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
          ((f : (a : E) → F →ₗ[𝕜] G) y) :
        F →L[𝕜] G)
Tactic: constructor