awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₂ : s.Nonempty
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have refine : ∀ (hl : Dense (↑l.ker : Set E)), False
Tactic: refine l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => ?_)
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₂ : s.Nonempty
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
⊢ False
have rcases : ∀ (x : E) (hx : x ∈ s), False
Tactic: rcases hs₂ with ⟨x, hx⟩
Cleared hypotheses: hs₂
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
⊢ x ∈ interior (↑l.ker : Set E)ᶜ
have rw : (↑l.ker : Set E)ᶜ ∈ 𝓝 x
Tactic: rw [mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
⊢ False
have this : x ∈ interior (↑l.ker : Set E)ᶜ
Tactic: have : x ∈ interior (LinearMap.ker l : Set E)ᶜ := by
    rw [mem_interior_iff_mem_nhds]
    exact mem_of_superset (hs₁.mem_nhds hx) hs₃
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
this : x ∈ interior (↑l.ker : Set E)ᶜ
⊢ False
have rwa : ∀ (this : Membership.mem (γ := Set E) ∅ x), False
Tactic: rwa [hl.interior_compl] at this
Cleared hypotheses: this
-- 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
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have have : ∀ (this : Fintype ι), Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
Tactic: have := Fintype.ofFinite ι
-- 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 := ⋯
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have suffices : ∀ (n : ℕ), Fintype.card ι = n → Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
Tactic: suffices ∀ n, Fintype.card ι = n → Continuous ξ.equivFun by exact this _ rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
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 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = 0
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have hn₁ : IsEmpty ι
Tactic: rw [Fintype.card_eq_zero_iff] at hn
Cleared hypotheses: hn
-- 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_3 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_4 : 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 : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
have this₁ : FiniteDimensional 𝕜 E
Tactic: haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite
-- 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_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
s : Submodule 𝕜 E
s_dim : finrank.{u, v} 𝕜 ↥s = n
this : IsUniformAddGroup.{v} ↥s := ⋯
b : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
⊢ Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = n
have rw : Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = finrank.{u, v} 𝕜 ↥s
Tactic: rw [← s_dim]
-- 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
s : Submodule 𝕜 E
s_dim : finrank.{u, v} 𝕜 ↥s = n
this : IsUniformAddGroup.{v} ↥s := ⋯
b : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
⊢ IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)
have this₁ : Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = n
Tactic: have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
-- 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_6 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_7 : 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
s : Submodule 𝕜 E
s_dim : finrank.{u, v} 𝕜 ↥s = n
this_5 : IsUniformAddGroup.{v} ↥s := ⋯
b : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
this : Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = n
⊢ IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)
have this₁ : Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
  (⇑b.equivFun : (a : ↥s) → (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜)
Tactic: have : Continuous b.equivFun := IH b inferInstance 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_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
s : Submodule 𝕜 E
s_dim : finrank.{u, v} 𝕜 ↥s = n
this : IsUniformAddGroup.{v} ↥s := ⋯
b : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
⊢ IsClosed[inst_3] (↑s : Set E)
have U : IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
  (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)
Tactic: 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
-- 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
s : Submodule 𝕜 E
s_dim : finrank.{u, v} 𝕜 ↥s = n
this : IsUniformAddGroup.{v} ↥s := ⋯
b : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
U :
  IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)
⊢ IsClosed[inst_3] (↑s : Set E)
have this₁ : IsComplete (↑s : Set E)
Tactic: have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)
-- 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)
f : E →ₗ[𝕜] 𝕜
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
have pos : ∀ (H : finrank 𝕜 ↥f.range = 0),
  Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
Tactic: by_cases H : finrank 𝕜 (LinearMap.range f) = 0
-- 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)
f : E →ₗ[𝕜] 𝕜
pos :
  ∀ (H : finrank 𝕜 ↥f.range = 0),
    Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
have neg : ∀ (H : ¬finrank 𝕜 ↥f.range = 0),
  Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
Tactic: by_cases H : finrank 𝕜 (LinearMap.range f) = 0
-- 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 H₂ : f = 0
Tactic: rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
Cleared hypotheses: H
-- 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)
f : E →ₗ[𝕜] 𝕜
H : f = 0
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
have pos : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑0 : (a : E) → 𝕜)
Tactic: rw [H]
-- 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
⊢ finrank.{u, v} 𝕜 ↥f.ker = n
have Z : finrank 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = finrank 𝕜 E
Tactic: have Z := f.finrank_range_add_finrank_ker
-- 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
Z : finrank 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = finrank 𝕜 E
⊢ finrank.{u, v} 𝕜 ↥f.ker = n
have Z₁ : finrank 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = n + 1
Tactic: rw [finrank_eq_card_basis ξ, hn] at Z
Cleared hypotheses: 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_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
Z : finrank 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = n + 1
⊢ finrank.{u, v} 𝕜 ↥f.ker = n
have this₁ : finrank 𝕜 ↥f.range = 1
Tactic: have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)