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
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
Z₁ : (finrank.{u, v} 𝕜 ↥f.ker).succ = n + 1
⊢ finrank 𝕜 ↥f.range = 1

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

Premises used: add_comm, Nat.add_one
-- 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.{u, v} 𝕜 ↥f.ker).succ = n + 1
this : finrank 𝕜 ↥f.range = 1
⊢ finrank.{u, v} 𝕜 ↥f.ker = n

Tactic:
Nat.succ.inj Z

Premises used: Nat.succ.inj
-- 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.{u, v} 𝕜 ↥f.ker).succ = n + 1
this : finrank 𝕜 ↥f.range = 1
⊢ finrank.{u, v} 𝕜 ↥f.ker = n

Tactic:
exact Nat.succ.inj Z

Premises used: Nat.succ.inj
-- 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.{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
-- 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
this : finrank.{u, v} 𝕜 ↥f.ker = n
⊢ IsClosed[inst_3] (↑f.ker : Set E)

Tactic:
have : IsClosed (LinearMap.ker f : Set E) := H₁ _ 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_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
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
this_5 : finrank.{u, v} 𝕜 ↥f.ker = n
this : IsClosed[inst_3] (↑f.ker : Set E)
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)

Tactic:
LinearMap.continuous_of_isClosed_ker f this

Premises used: LinearMap.continuous_of_isClosed_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_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
H₁ : ∀ (s : Submodule 𝕜 E), finrank.{u, v} 𝕜 ↥s = n → IsClosed[inst_3] (↑s : Set E)
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
this_5 : finrank.{u, v} 𝕜 ↥f.ker = n
this : IsClosed[inst_3] (↑f.ker : Set E)
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)

Tactic:
exact LinearMap.continuous_of_isClosed_ker f this

Premises used: LinearMap.continuous_of_isClosed_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 →ₗ[𝕜] 𝕜), 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
-- 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)
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
succ :
  ∀ (i : ι),
    Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E) ↦
      (ξ.equivFun : (a : E) → ι → 𝕜) a i
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
rw [continuous_pi_iff]

Premises used: continuous_pi_iff
-- 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)
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
i : ι
succ : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(ξ.coord i) : (a : E) → 𝕜)
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E) ↦
    (ξ.equivFun : (a : E) → ι → 𝕜) a i

Tactic:
change Continuous (ξ.coord i)

Premises used: Continuous, Module.Basis.coord, DFunLike.coe
-- 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)
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
i : ι
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(ξ.coord i) : (a : E) → 𝕜)

Tactic:
H₂ (ξ.coord i)

Premises used: Module.Basis.coord
-- 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)
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → 𝕜)
i : ι
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(ξ.coord i) : (a : E) → 𝕜)

Tactic:
exact H₂ (ξ.coord i)

Premises used: Module.Basis.coord
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
⊢ IsModuleTopology 𝕜 E

Tactic:
let b := Basis.ofVectorSpace 𝕜 E
  have continuousEquiv : E ≃L[𝕜] (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜 :=
    { __ := b.equivFun
      continuous_toFun := continuous_equivFun_basis_aux b
      continuous_invFun := IsModuleTopology.continuous_of_linearMap (R := 𝕜)
        (A := (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜) (B := E) b.equivFun.symm }
  IsModuleTopology.iso continuousEquiv.symm

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.mk, _private.0.continuous_equivFun_basis_aux, IsModuleTopology.iso, IsModuleTopology.continuous_of_linearMap, LinearEquiv.toLinearMap, Module.Basis.ofVectorSpace, Module.Basis.equivFun
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 x
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 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ Continuous[inst_2, inst_7] (⇑f : (a : E) → F')

Tactic:
IsModuleTopology.continuous_of_linearMap f

Premises used: IsModuleTopology.continuous_of_linearMap
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 𝕜
inst_16 : T2Space E
inst_17 : FiniteDimensional 𝕜 E
⊢ ContinuousLinearMapClass (E →ₗ[𝕜] F') 𝕜 E F'

Tactic:
{ LinearMap.semilinearMapClass with map_continuous := fun f => f.continuous_of_finiteDimensional }

Premises used: LinearMap.semilinearMapClass, ContinuousSemilinearMapClass.mk
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 u_1
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite
  ξ.equivFun.toLinearMap.continuous_of_finiteDimensional

Premises used: LinearEquiv.toLinearMap, LinearMap.continuous_of_finiteDimensional, Module.Basis.equivFun
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 x
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 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ Eq (α := (a : E) → F')
    (⇑(((toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F') : (a : E →ₗ[𝕜] F') → E →L[𝕜] F') f : E →L[𝕜] F') :
      (a : E) → F')
    (⇑f : (a : E) → F')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 x
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 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F') : (a : E →ₗ[𝕜] F') → E →L[𝕜] F') f) : E →ₗ[𝕜] F') = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 x
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 : FiniteDimensional 𝕜 E
⊢ Eq (α := (a : E →L[𝕜] F') → E →ₗ[𝕜] F')
    (⇑(LinearEquiv.symm toContinuousLinearMap : (E →L[𝕜] F') ≃ₗ[𝕜] E →ₗ[𝕜] F') : (a : E →L[𝕜] F') → E →ₗ[𝕜] F')
    ContinuousLinearMap.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 →ₗ[𝕜] E
⊢ Eq.{u + 1} (α := 𝕜)
    (ContinuousLinearMap.det.{u, v} (M := E)
        (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) f) :
      𝕜)
    ((LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 x
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 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ ker.{u, u, v, x} (R₂ := 𝕜) (M₂ := F') (τ₁₂ := RingHom.id 𝕜)
      (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F') : (a : E →ₗ[𝕜] F') → E →L[𝕜] F') f) : E →ₗ[𝕜] F') =
    f.ker

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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 x
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 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ range.{u, u, v, x} (R := 𝕜) (M := E) (τ₁₂ := RingHom.id 𝕜)
      (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F') : (a : E →ₗ[𝕜] F') → E →L[𝕜] F') f) : E →ₗ[𝕜] F') =
    f.range

Tactic:
rfl

Premises used: rfl