awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
    [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_5 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_6 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
this_4 : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
Z : finrank 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = n + 1
this : finrank 𝕜 ↥f.range = 1
⊢ finrank.{u, v} 𝕜 ↥f.ker = n
have Z₁ : (finrank.{u, v} 𝕜 ↥f.ker).succ = n + 1
Tactic: rw [this, add_comm, Nat.add_one] at Z
Cleared hypotheses: Z, this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
    [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_4 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_5 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
have this₁ : finrank.{u, v} 𝕜 ↥f.ker = n
Tactic: have : finrank 𝕜 (LinearMap.ker f) = n := by
          have Z := f.finrank_range_add_finrank_ker
          rw [finrank_eq_card_basis ξ, hn] at Z
          have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)
          rw [this, add_comm, Nat.add_one] at Z
          exact Nat.succ.inj Z
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
    [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_5 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_6 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
this_4 : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
this : finrank.{u, v} 𝕜 ↥f.ker = n
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
have this₁ : IsClosed[inst_3] (↑f.ker : Set E)
Tactic: have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
    [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_4 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_5 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
Tactic: have H₂ : ∀ f : E →ₗ[𝕜] 𝕜, Continuous f := by
      intro f
      by_cases H : finrank 𝕜 (LinearMap.range f) = 0
      · rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
        rw [H]
        exact continuous_zero
      · have : finrank 𝕜 (LinearMap.ker f) = n := by
          have Z := f.finrank_range_add_finrank_ker
          rw [finrank_eq_card_basis ξ, hn] at Z
          have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)
          rw [this, add_comm, Nat.add_one] at Z
          exact Nat.succ.inj Z
        have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
        exact LinearMap.continuous_of_isClosed_ker f this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
    [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_4 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_5 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have succ : ∀ (i : ι),
  Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E) ↦
    (ξ.equivFun : (a : E) → ι → 𝕜) a i
Tactic: rw [continuous_pi_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
    [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_4 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_5 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
i : ι
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E) ↦
    (ξ.equivFun : (a : E) → ι → 𝕜) a i
have succ : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(ξ.coord i) : (a : E) → 𝕜)
Tactic: change Continuous (ξ.coord i)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst : AddCommGroup E
inst_1 : Module 𝕜 E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : CompleteSpace 𝕜
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
n : ℕ
hn : Fintype.card ι = n
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have zero : ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι] (ξ : Basis ι 𝕜 E) (this : Fintype ι)
  (hn : Fintype.card ι = 0), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
Tactic: induction n generalizing ι E with
  | zero =>
    rw [Fintype.card_eq_zero_iff] at hn
    exact continuous_of_const fun x y => funext hn.elim
  | succ n IH =>
    haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite
    -- first step: thanks to the induction hypothesis, any n-dimensional subspace is equivalent
    -- to a standard space of dimension n, hence it is complete and therefore closed.
    have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by
      intro s s_dim
      letI : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup
      let b := Basis.ofVectorSpace 𝕜 s
      have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by
        have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
        have : Continuous b.equivFun := IH b inferInstance this
        exact
          b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
      have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)
      exact this.isClosed
    -- second step: any linear form is continuous, as its kernel is closed by the first step
    have H₂ : ∀ f : E →ₗ[𝕜] 𝕜, Continuous f := by
      intro f
      by_cases H : finrank 𝕜 (LinearMap.range f) = 0
      · rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
        rw [H]
        exact continuous_zero
      · have : finrank 𝕜 (LinearMap.ker f) = n := by
          have Z := f.finrank_range_add_finrank_ker
          rw [finrank_eq_card_basis ξ, hn] at Z
          have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)
          rw [this, add_comm, Nat.add_one] at Z
          exact Nat.succ.inj Z
        have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
        exact LinearMap.continuous_of_isClosed_ker f this
    rw [continuous_pi_iff]
    intro i
    change Continuous (ξ.coord i)
    exact H₂ (ξ.coord i)
Cleared hypotheses: E, inst, inst_1, inst_2, inst_3, inst_4, inst_6, ι, inst_7, ξ, this_1, this_2, this, n, hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst : AddCommGroup E
inst_1 : Module 𝕜 E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul 𝕜 E
F : Type w
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousSMul 𝕜 F
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ (↑e.toContinuousLinearEquiv : E ≃ₗ[𝕜] F) = e
have h : ∀ (x : E),
  Eq.{w + 1} (α := F) (((↑e.toContinuousLinearEquiv : E ≃ₗ[𝕜] F) : (a : E) → F) x : F) ((e : (a : E) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst : AddCommGroup E
inst_1 : Module 𝕜 E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul 𝕜 E
F : Type w
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousSMul 𝕜 F
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ (↑(ContinuousLinearEquiv.symm e.toContinuousLinearEquiv) : F ≃ₗ[𝕜] E) = e.symm
have h : ∀ (x : F),
  Eq.{v + 1} (α := E) (((↑(ContinuousLinearEquiv.symm e.toContinuousLinearEquiv) : F ≃ₗ[𝕜] E) : (a : F) → E) x : E)
    ((e.symm : (a : F) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst : AddCommGroup E
inst_1 : Module 𝕜 E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul 𝕜 E
F : Type w
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousSMul 𝕜 F
F' : Type x
inst_10 : AddCommGroup F'
inst_11 : Module 𝕜 F'
inst_12 : TopologicalSpace F'
inst_13 : IsTopologicalAddGroup F'
inst_14 : ContinuousSMul 𝕜 F'
inst_15 : CompleteSpace 𝕜
ι : Type u_1
inst_16 : Finite ι
inst_17 : T2Space E
v : Basis ι 𝕜 E
⊢ Continuous[Pi.topologicalSpace, inst_2] v.equivFun.invFun
have change : Continuous[Pi.topologicalSpace, inst_2] (↑v.equivFun.symm : (ι → 𝕜) →ₗ[𝕜] E).toFun
Tactic: change Continuous v.equivFun.symm.toFun
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst : AddCommGroup E
inst_1 : Module 𝕜 E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : CompleteSpace 𝕜
inst_6 : T2Space E
inst_7 : FiniteDimensional 𝕜 E
f : E →L[𝕜] E
hf : f.det ≠ 0
⊢ (↑(f.toContinuousLinearEquivOfDetNeZero hf) : E →L[𝕜] E) = f
have h : ∀ (x : E),
  Eq (α := E) (((↑(f.toContinuousLinearEquivOfDetNeZero hf) : E →L[𝕜] E) : (a : E) → E) x : E) ((f : (a : E) → E) x : E)
Tactic: ext x
-- 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 : UniformSpace E
inst_4 : T2Space E
inst_5 : IsUniformAddGroup E
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 :=
  ContinuousLinearEquiv.ofFinrankEq.{u_1, u_2, u_1} (𝕜 := 𝕜) (E := E) (F := Fin (finrank 𝕜 E) → 𝕜) ⋯
⊢ CompleteSpace E
have this : IsUniformEmbedding.{u_1, u_2} (α := Fin (finrank 𝕜 E) → 𝕜) (β := E)
  (⇑(↑e : E ≃ₗ[𝕜] Fin (finrank 𝕜 E) → 𝕜).toEquiv.symm : (a : Fin (finrank 𝕜 E) → 𝕜) → E)
Tactic: have : IsUniformEmbedding e.toEquiv.symm := e.symm.isUniformEmbedding
-- 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
s t : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ s)
s_closed : IsClosed[inst_3] (↑s : Set E)
s_le_t : s ≤ t
⊢ IsClosed[inst_3] (↑t : Set E)
have rw : IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)
Tactic: rw [show t = comap s.mkQ (map s.mkQ t) by simpa]
-- 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
s t : Submodule 𝕜 E
hs : IsClosed[inst_3] (↑s : Set E)
ht : FiniteDimensional.{u_1, u_2} 𝕜 ↥t
⊢ IsClosed[inst_3] (↑(s ⊔ t) : Set E)
have rw : IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)
Tactic: rw [← comap_map_mkQ]
-- 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
inst_7 : T2Space E
c : E
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
have pos : ∀ (hc : c = 0), IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
Tactic: by_cases hc : c = 0
-- 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
inst_7 : T2Space E
c : E
pos : ∀ (hc : c = 0), IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
have neg : ∀ (hc : ¬c = 0), IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
Tactic: by_cases hc : c = 0
-- 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
inst_7 : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
have pos : IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ 0
Tactic: simp_rw [hc, smul_zero]
-- 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
⊢ FiniteDimensional 𝕜 Eᵤ
have obtain : ∀ (c : 𝕜) (hc0 : 0 < ‖c‖) (hc1 : ‖c‖ < 1), FiniteDimensional 𝕜 Eᵤ
Tactic: obtain ⟨c, hc0, hc1⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < 1 := NormedField.exists_norm_lt 𝕜 zero_lt_one
-- 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
⊢ FiniteDimensional 𝕜 Eᵤ
have hc_ne : c ≠ 0
Tactic: have hc_ne : c ≠ 0 := norm_pos_iff.mp hc0
-- 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
⊢ FiniteDimensional 𝕜 Eᵤ
have obtain : ∀ (F : Set Eᵤ) (hF_finite : F.Finite) (hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U), FiniteDimensional 𝕜 Eᵤ
Tactic: obtain ⟨F, hF_finite, hF_cover⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hU_tb
    (c • U) ((set_smul_mem_nhds_zero_iff hc_ne).mpr 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ᵤ
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 := ⋯
x : Eᵤ
hx : x ∈ U
⊢ x ∈ (↑M : Set Eᵤ) + c • U
have obtain : ∀ (f : Eᵤ) (hf : f ∈ F) (y : Eᵤ) (hy : y ∈ c • U) (hx : (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ U),
  (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ (↑M : Set Eᵤ) + c • U
Tactic: obtain ⟨f, hf, y, hy, rfl⟩ := Set.mem_iUnion₂.mp <| hF_cover hx
Cleared hypotheses: x, 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 := ⋯
⊢ FiniteDimensional 𝕜 Eᵤ
have h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
Tactic: have h_cover : U ⊆ M + c • U := fun x hx ↦ by
    obtain ⟨f, hf, y, hy, rfl⟩ := Set.mem_iUnion₂.mp <| hF_cover hx
    exact ⟨f, Submodule.subset_span hf, y, hy, rfl⟩
-- 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ᵤ) + c • U) ⊆ (↑M : Set Eᵤ) + c ^ (n + 1) • U
have rw : (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) + (c ^ n * c) • U ⊆ (↑M : Set Eᵤ) + (c ^ n * c) • U
Tactic: rw [smul_add, smul_smul, pow_succ, ← add_assoc]
-- 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ᵤ) + (c ^ n * c) • U ⊆ (↑M : Set Eᵤ) + (c ^ n * c) • U
have hxy : (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)
Tactic: congr!