awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective.{w + 1, v + 1} (α := F) (β := E) (⇑f : (a : F) → E)
⊢ IsOpenMap.{w, v} (X := F) (Y := E) (⇑f : (a : F) → E)

Tactic:
IsModuleTopology.isOpenMap_of_surjective hf

Premises used: IsModuleTopology.isOpenMap_of_surjective
-- 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
⊢ CanLift (E →ₗ[𝕜] F) (E →L[𝕜] F) ContinuousLinearMap.toLinearMap fun (x : E →ₗ[𝕜] F) ↦ True

Tactic:
⟨fun f _ => ⟨LinearMap.toContinuousLinearMap f, rfl⟩⟩

Premises used: Exists.intro, CanLift.mk, DFunLike.coe, rfl, LinearMap.toContinuousLinearMap
-- 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
g : E →L[𝕜] E
⊢ ((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) f = g ↔ f = (↑g : E →ₗ[𝕜] E)

Tactic:
simp [ContinuousLinearMap.ext_iff, LinearMap.ext_iff]

Premises used: LinearMap.ext_iff, ContinuousLinearMap.ext_iff
-- 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
g : E →L[𝕜] E
f : E →ₗ[𝕜] E
⊢ (↑g : E →ₗ[𝕜] E) = f ↔ g = ((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) f

Tactic:
simp [ContinuousLinearMap.ext_iff, LinearMap.ext_iff]

Premises used: LinearMap.ext_iff, ContinuousLinearMap.ext_iff
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ (↑(↑e.toContinuousLinearEquiv : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) = (↑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 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
⊢ Eq (α := (a : E) → F) (⇑e.toContinuousLinearEquiv : (a : E) → F) (⇑e : (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 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).symm : F →ₗ[𝕜] E) = (↑e.symm : F →ₗ[𝕜] E)

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 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
⊢ Eq (α := (a : F) → E) (⇑(ContinuousLinearEquiv.symm e.toContinuousLinearEquiv) : (a : F) → E) (⇑e.symm : (a : F) → E)

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 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
h :
  ∀ (x : E),
    Eq.{w + 1} (α := F) (((↑e.toContinuousLinearEquiv : E ≃ₗ[𝕜] F) : (a : E) → F) x : F) ((e : (a : E) → F) x : F)
⊢ (↑e.toContinuousLinearEquiv : E ≃ₗ[𝕜] F) = e

Tactic:
ext x
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : E
⊢ Eq.{w + 1} (α := F) (((↑e.toContinuousLinearEquiv : E ≃ₗ[𝕜] F) : (a : E) → F) x : F) ((e : (a : E) → F) x : F)

Tactic:
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 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
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)
⊢ (↑(ContinuousLinearEquiv.symm e.toContinuousLinearEquiv) : F ≃ₗ[𝕜] E) = e.symm

Tactic:
ext x
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
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:
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 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 : T2Space F
inst_18 : FiniteDimensional 𝕜 E
⊢ CanLift (E ≃ₗ[𝕜] F) (E ≃L[𝕜] F) ContinuousLinearEquiv.toLinearEquiv fun (x : E ≃ₗ[𝕜] F) ↦ True

Tactic:
⟨fun f _ => ⟨_, f.toLinearEquiv_toContinuousLinearEquiv⟩⟩

Premises used: LinearEquiv.toLinearEquiv_toContinuousLinearEquiv, Exists.intro, CanLift.mk, LinearEquiv.toContinuousLinearEquiv
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
inst_14 : FiniteDimensional 𝕜 F
cond : finrank 𝕜 E = finrank 𝕜 F
⊢ Nonempty (E ≃L[𝕜] F)

Tactic:
(nonempty_linearEquiv_of_finrank_eq cond).map LinearEquiv.toContinuousLinearEquiv

Premises used: FiniteDimensional.nonempty_linearEquiv_of_finrank_eq, LinearEquiv.toContinuousLinearEquiv, Nonempty.map
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 E
inst_14 : FiniteDimensional 𝕜 F
⊢ Nonempty (E ≃L[𝕜] F) ↔ finrank 𝕜 E = finrank 𝕜 F

Tactic:
⟨fun ⟨h⟩ => h.toLinearEquiv.finrank_eq, fun h =>
    FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq h⟩

Premises used: ContinuousLinearEquiv.toLinearEquiv, _private.0.FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq.match_1, LinearEquiv.finrank_eq, FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq, Iff.intro, Eq, Module.finrank
-- 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
inst_10 : CompleteSpace 𝕜
ι : Type u_1
inst_11 : Finite ι
inst_12 : T2Space E
v : Basis ι 𝕜 E
f : ι → F
⊢ Eq (α := E →ₗ[𝕜] F) (↑(v.constrL f) : E →ₗ[𝕜] F) ((v.constr 𝕜 : (a : ι → 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 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
change : Continuous[Pi.topologicalSpace, inst_2] (↑v.equivFun.symm : (ι → 𝕜) →ₗ[𝕜] E).toFun
⊢ Continuous[Pi.topologicalSpace, inst_2] v.equivFun.invFun

Tactic:
change Continuous v.equivFun.symm.toFun

Premises used: LinearEquiv.symm, Continuous, LinearMap.toAddHom, LinearEquiv.toLinearMap, AddHom.toFun, 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 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.symm : (ι → 𝕜) →ₗ[𝕜] E).toFun

Tactic:
v.equivFun.symm.toLinearMap.continuous_of_finiteDimensional

Premises used: LinearEquiv.symm, 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 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.symm : (ι → 𝕜) →ₗ[𝕜] E).toFun

Tactic:
exact v.equivFun.symm.toLinearMap.continuous_of_finiteDimensional

Premises used: LinearEquiv.symm, 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
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Finite ι
inst_7 : T2Space E
v : Basis ι 𝕜 E
x : E
⊢ (ContinuousLinearEquiv.symm v.equivFunL : (a : ι → 𝕜) → E) (⇑((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) =
    x

Tactic:
v.equivFunL.symm_apply_apply x

Premises used: Module.Basis.equivFunL, ContinuousLinearEquiv.symm_apply_apply
-- 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
inst_10 : CompleteSpace 𝕜
inst_11 : T2Space E
ι : Type u_2
inst_12 : Fintype ι
v : Basis ι 𝕜 E
f : ι → F
e : E
⊢ Eq.{w + 1} (α := F) ((v.constrL f : (a : E) → F) e : F)
    (∑ i : ι, HSMul.hSMul.{u, w, w} (α := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) (f i) : F)

Tactic:
v.constr_apply_fintype 𝕜 _ _

Premises used: Module.Basis.constr_apply_fintype
-- 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
inst_10 : CompleteSpace 𝕜
ι : Type u_1
inst_11 : Finite ι
inst_12 : T2Space E
v : Basis ι 𝕜 E
f : ι → F
i : ι
⊢ (v.constrL f : (a : E) → F) ((v : (a : ι) → E) i : E) = f i

Tactic:
v.constr_basis 𝕜 _ _

Premises used: Module.Basis.constr_basis
-- 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 →L[𝕜] E
hf : f.det ≠ 0
h :
  ∀ (x : E),
    Eq (α := E) (((↑(f.toContinuousLinearEquivOfDetNeZero hf) : E →L[𝕜] E) : (a : E) → E) x : E)
      ((f : (a : E) → E) x : E)
⊢ (↑(f.toContinuousLinearEquivOfDetNeZero hf) : E →L[𝕜] E) = f

Tactic:
ext x
-- 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 →L[𝕜] E
hf : f.det ≠ 0
x : E
⊢ Eq (α := E) (((↑(f.toContinuousLinearEquivOfDetNeZero hf) : E →L[𝕜] E) : (a : E) → E) x : E) ((f : (a : E) → E) x : E)

Tactic:
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 →L[𝕜] E
hf : f.det ≠ 0
x : E
⊢ Eq (α := E) ((f.toContinuousLinearEquivOfDetNeZero hf : (a : E) → E) x : E) ((f : (a : E) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
a b c d : 𝕜
⊢ ((LinearMap.toContinuousLinearMap.{u, u, u} (𝕜 := 𝕜) (E := 𝕜 × 𝕜) (F' := 𝕜 × 𝕜) :
          (𝕜 × 𝕜 →ₗ[𝕜] 𝕜 × 𝕜) ≃ₗ[𝕜] 𝕜 × 𝕜 →L[𝕜] 𝕜 × 𝕜) :
        (a : 𝕜 × 𝕜 →ₗ[𝕜] 𝕜 × 𝕜) → 𝕜 × 𝕜 →L[𝕜] 𝕜 × 𝕜)
      ((Matrix.toLin (Basis.finTwoProd 𝕜) (Basis.finTwoProd 𝕜) : (a : Matrix (Fin 2) (Fin 2) 𝕜) → 𝕜 × 𝕜 →ₗ[𝕜] 𝕜 × 𝕜)
        !![a, b; c, d]) =
    (HSMul.hSMul (β := 𝕜 × 𝕜 →L[𝕜] 𝕜) a (fst 𝕜 𝕜 𝕜) + HSMul.hSMul (β := 𝕜 × 𝕜 →L[𝕜] 𝕜) b (snd 𝕜 𝕜 𝕜)).prod
      (HSMul.hSMul (β := 𝕜 × 𝕜 →L[𝕜] 𝕜) c (fst 𝕜 𝕜 𝕜) + HSMul.hSMul (β := 𝕜 × 𝕜 →L[𝕜] 𝕜) d (snd 𝕜 𝕜 𝕜))

Tactic:
ContinuousLinearMap.ext <| Matrix.toLin_finTwoProd_apply _ _ _ _

Premises used: Matrix.toLin_finTwoProd_apply, ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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) → 𝕜) ⋯
⊢ 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
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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) → 𝕜) ⋯
this :
  IsUniformEmbedding.{u_1, u_2} (α := Fin (finrank 𝕜 E) → 𝕜) (β := E)
    (⇑(↑e : E ≃ₗ[𝕜] Fin (finrank 𝕜 E) → 𝕜).toEquiv.symm : (a : Fin (finrank 𝕜 E) → 𝕜) → E)
⊢ CompleteSpace E

Tactic:
(completeSpace_congr this).1 inferInstance

Premises used: completeSpace_congr, inferInstance, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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) → 𝕜) ⋯
this :
  IsUniformEmbedding.{u_1, u_2} (α := Fin (finrank 𝕜 E) → 𝕜) (β := E)
    (⇑(↑e : E ≃ₗ[𝕜] Fin (finrank 𝕜 E) → 𝕜).toEquiv.symm : (a : Fin (finrank 𝕜 E) → 𝕜) → E)
⊢ CompleteSpace E

Tactic:
exact (completeSpace_congr this).1 inferInstance

Premises used: completeSpace_congr, inferInstance, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
s : Submodule 𝕜 E
inst_8 : FiniteDimensional.{u_1, u_2} 𝕜 ↥s
⊢ IsComplete (↑s : Set E)

Tactic:
haveI : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup
  completeSpace_coe_iff_isComplete.1 (FiniteDimensional.complete 𝕜 s)

Premises used: Membership.mem, Subtype, Iff.mp, FiniteDimensional.complete, completeSpace_coe_iff_isComplete
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
s : Submodule 𝕜 E
inst_8 : FiniteDimensional.{u_1, u_2} 𝕜 ↥s
⊢ IsClosed[inst_3] (↑s : Set E)

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace E
  haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  s.complete_of_finiteDimensional.isClosed

Premises used: IsComplete.isClosed, Submodule.complete_of_finiteDimensional
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
⊢ t = comap s.mkQ (map s.mkQ t)

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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
rw : IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)
⊢ IsClosed[inst_3] (↑t : Set E)

Tactic:
rw [show t = comap s.mkQ (map s.mkQ t) by simpa]
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
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] (↑(comap s.mkQ (map s.mkQ t)) : Set E)

Tactic:
(map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

Premises used: Set.Mem, Submodule.Quotient.mk, setOf, Submodule.closed_of_finiteDimensional, Set.preimage, continuous_quot_mk, IsClosed.preimage, Submodule.mkQ, Set.image, Submodule.map