awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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

Tactic:
have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
⊢ Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
    (⇑b.equivFun : (a : ↥s) → (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜)

Tactic:
have : Continuous b.equivFun := IH b inferInstance this
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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_7 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_8 : 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_6 : Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = n
this :
  Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
    (⇑b.equivFun : (a : ↥s) → (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜)
⊢ IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)

Tactic:
b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this

Premises used: LinearEquiv.symm, LinearEquiv.toLinearMap, LinearMap.continuous_on_pi, LinearEquiv.isUniformEmbedding, Module.Basis.equivFun
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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_7 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_8 : 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_6 : Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = n
this :
  Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
    (⇑b.equivFun : (a : ↥s) → (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜)
⊢ IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)

Tactic:
exact
          b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this

Premises used: LinearEquiv.symm, LinearEquiv.toLinearMap, LinearMap.continuous_on_pi, LinearEquiv.isUniformEmbedding, Module.Basis.equivFun
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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)

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
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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)
⊢ IsComplete (↑s : Set E)

Tactic:
have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
U :
  IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)
this : IsComplete (↑s : Set E)
⊢ IsClosed[inst_3] (↑s : Set E)

Tactic:
this.isClosed

Premises used: IsComplete.isClosed
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
U :
  IsUniformEmbedding (α := (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) (β := ↥s)
    (⇑b.equivFun.symm.toEquiv : (a : (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) → 𝕜) → ↥s)
this : IsComplete (↑s : Set E)
⊢ IsClosed[inst_3] (↑s : Set E)

Tactic:
exact this.isClosed

Premises used: IsComplete.isClosed
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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) → 𝕜)
neg :
  ∀ (H : ¬finrank 𝕜 ↥f.range = 0),
    Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)

Tactic:
by_cases H : finrank 𝕜 (LinearMap.range f) = 0

Premises used: Membership.mem, LinearMap.range, Subtype, Module.finrank
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
⊢ f = 0

Tactic:
rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H

Premises used: LinearMap.range_eq_bot, Submodule.finrank_eq_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
pos : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑0 : (a : E) → 𝕜)
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)

Tactic:
rw [H]
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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] (⇑0 : (a : E) → 𝕜)

Tactic:
continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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] (⇑0 : (a : E) → 𝕜)

Tactic:
exact continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = finrank 𝕜 E

Tactic:
have Z := f.finrank_range_add_finrank_ker
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 𝕜 ↥f.range + finrank.{u, v} 𝕜 ↥f.ker = n + 1

Tactic:
rw [finrank_eq_card_basis ξ, hn] at Z

Premises used: Module.finrank_eq_card_basis
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 𝕜 ↥f.range = 1

Tactic:
have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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).succ = n + 1

Tactic:
rw [this, add_comm, Nat.add_one] at Z

Premises used: add_comm, Nat.add_one