awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 x
hU_tb : TotallyBounded U
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
FiniteDimensional.of_totallyBounded_nhds (𝕜 := 𝕜) hU_nhds hU_tb

Premises used: FiniteDimensional.of_totallyBounded_nhds
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 x
hU_tb : TotallyBounded U
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
exact FiniteDimensional.of_totallyBounded_nhds (𝕜 := 𝕜) hU_nhds hU_tb

Premises used: FiniteDimensional.of_totallyBounded_nhds
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : WeaklyLocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Tactic:
let : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
  have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  let ⟨_, hU_compact, hU_nhds⟩ := exists_compact_mem_nhds (0 : E)
  .of_totallyBounded_nhds_zero 𝕜 hU_nhds hU_compact.totallyBounded

Premises used: FiniteDimensional.of_totallyBounded_nhds_zero, IsCompact.totallyBounded, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, isUniformAddGroup_of_addCommGroup, _private.0.FiniteDimensional.of_locallyCompactSpace.match_1, FiniteDimensional, OfNat.ofNat, IsTopologicalAddGroup.rightUniformSpace
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
X : Type u_7
inst_8 : TopologicalSpace X
inst_9 : Zero X
inst_10 : T1Space X
f : E → X
hf : HasCompactSupport f
h'f : Continuous[inst_4, inst_8] f
⊢ f = 0 ∨ FiniteDimensional 𝕜 E

Tactic:
(HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup hf h'f).imp_right fun h ↦
    have : LocallyCompactSpace E := h; .of_locallyCompactSpace 𝕜

Premises used: FiniteDimensional.of_locallyCompactSpace, Or.imp_right, HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
X : Type u_7
inst_8 : TopologicalSpace X
inst_9 : One X
inst_10 : T1Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous[inst_4, inst_8] f
⊢ f = 1 ∨ FiniteDimensional 𝕜 E

Tactic:
have : T1Space (Additive X) := ‹_›
  HasCompactSupport.eq_zero_or_finiteDimensional 𝕜 (X := Additive X) hf h'f

Premises used: Additive, HasCompactSupport.eq_zero_or_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
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
φ : E ⧸ p →L[𝕜] ↥q :=
  ((LinearMap.toContinuousLinearMap : (E ⧸ p →ₗ[𝕜] ↥q) ≃ₗ[𝕜] E ⧸ p →L[𝕜] ↥q) : (a : E ⧸ p →ₗ[𝕜] ↥q) → E ⧸ p →L[𝕜] ↥q)
    (↑(p.quotientEquivOfIsCompl q h) : E ⧸ p →ₗ[𝕜] ↥q)
x : ↥q
⊢ (φ ∘SL p.mkQL : (a : E) → ↥q) (↑x : E) = x

Tactic:
simp [φ]
-- 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
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
φ : E ⧸ p →L[𝕜] ↥q :=
  ((LinearMap.toContinuousLinearMap : (E ⧸ p →ₗ[𝕜] ↥q) ≃ₗ[𝕜] E ⧸ p →L[𝕜] ↥q) : (a : E ⧸ p →ₗ[𝕜] ↥q) → E ⧸ p →L[𝕜] ↥q)
    (↑(p.quotientEquivOfIsCompl q h) : E ⧸ p →ₗ[𝕜] ↥q)
⊢ IsTopCompl q (↑(φ ∘SL p.mkQL) : E →ₗ[𝕜] ↥q).ker

Tactic:
have := (φ ∘L p.mkQL).isTopCompl_of_proj fun x ↦ by simp [φ]
-- 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
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
φ : E ⧸ p →L[𝕜] ↥q :=
  ((LinearMap.toContinuousLinearMap : (E ⧸ p →ₗ[𝕜] ↥q) ≃ₗ[𝕜] E ⧸ p →L[𝕜] ↥q) : (a : E ⧸ p →ₗ[𝕜] ↥q) → E ⧸ p →L[𝕜] ↥q)
    (↑(p.quotientEquivOfIsCompl q h) : E ⧸ p →ₗ[𝕜] ↥q)
this : IsTopCompl q (↑(φ ∘SL p.mkQL) : E →ₗ[𝕜] ↥q).ker
⊢ IsTopCompl p q

Tactic:
simpa [φ] using this.symm

Premises used: Submodule.IsTopCompl.symm
-- 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
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 ↥q
suffices : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
⊢ IsTopCompl p q

Tactic:
suffices FiniteDimensional 𝕜 (E ⧸ p) from h.isTopCompl_of_finiteDimensional_quotient hp
-- 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
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 ↥q
⊢ FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)

Tactic:
(p.quotientEquivOfIsCompl q h).symm.finiteDimensional

Premises used: LinearEquiv.symm, LinearEquiv.finiteDimensional, Submodule.quotientEquivOfIsCompl
-- 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
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 ↥q
⊢ FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)

Tactic:
exact (p.quotientEquivOfIsCompl q h).symm.finiteDimensional

Premises used: LinearEquiv.symm, LinearEquiv.finiteDimensional, Submodule.quotientEquivOfIsCompl
-- 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
p : Submodule 𝕜 E
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
⊢ ∃ (q : Submodule 𝕜 E), IsCompl p q

Tactic:
p.exists_isCompl

Premises used: Submodule.exists_isCompl
-- 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
p : Submodule 𝕜 E
hp : IsClosed[inst_3] (↑p : Set E)
hq : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
obtain : ∀ (q : Submodule 𝕜 E) (hq : IsCompl p q), p.ClosedComplemented
⊢ p.ClosedComplemented

Tactic:
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl

Premises used: Submodule.exists_isCompl
-- 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
p : Submodule 𝕜 E
hp : IsClosed[inst_3] (↑p : Set E)
hq_1 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
q : Submodule 𝕜 E
hq : IsCompl p q
⊢ p.ClosedComplemented

Tactic:
hq.isTopCompl_of_finiteDimensional_quotient hp |>.closedComplemented

Premises used: Submodule.IsCompl.isTopCompl_of_finiteDimensional_quotient, Submodule.IsTopCompl.closedComplemented
-- 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
p : Submodule 𝕜 E
hp : IsClosed[inst_3] (↑p : Set E)
hq_1 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ p)
q : Submodule 𝕜 E
hq : IsCompl p q
⊢ p.ClosedComplemented

Tactic:
exact hq.isTopCompl_of_finiteDimensional_quotient hp |>.closedComplemented

Premises used: Submodule.IsCompl.isTopCompl_of_finiteDimensional_quotient, Submodule.IsTopCompl.closedComplemented
-- 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
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
hA : A.ClosedComplemented
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
obtain : ∀ (p : E →L[𝕜] ↥A) (hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x), B.ClosedComplemented
⊢ B.ClosedComplemented

Tactic:
obtain ⟨p, hp⟩ := hA
-- 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
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x
obtain : ∀ (C : Submodule 𝕜 E) (hBC : IsCompl B C), B.ClosedComplemented
⊢ B.ClosedComplemented

Tactic:
obtain ⟨C, hBC⟩ := B.exists_isCompl

Premises used: Submodule.exists_isCompl
-- 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
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x
C : Submodule 𝕜 E
hBC : IsCompl B C
⊢ B.ClosedComplemented

Tactic:
⟨((projectionOnto B C hBC).domRestrict A).toContinuousLinearMap ∘SL p, fun x ↦ ?_⟩

Premises used: ContinuousLinearMap.comp, Submodule.ClosedComplemented, LinearMap.domRestrict, Submodule.projectionOnto, Exists.intro, DFunLike.coe, LinearMap.toContinuousLinearMap
-- 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
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x
C : Submodule 𝕜 E
hBC : IsCompl B C
refine :
  ∀ (x : ↥B),
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (((LinearMap.toContinuousLinearMap : (↥A →ₗ[𝕜] ↥B) ≃ₗ[𝕜] ↥A →L[𝕜] ↥B) : (a : ↥A →ₗ[𝕜] ↥B) → ↥A →L[𝕜] ↥B)
              ((B.projectionOnto C hBC).domRestrict A))
            p :
          (a : E) → ↥B)
        (↑x : E) =
      x
⊢ B.ClosedComplemented

Tactic:
refine ⟨((projectionOnto B C hBC).domRestrict A).toContinuousLinearMap ∘SL p, fun x ↦ ?_⟩
-- 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
A B : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 ↥A
inst_8 : T2Space.{u_2} ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), (p : (a : E) → ↥A) (↑x : E) = x
C : Submodule 𝕜 E
hBC : IsCompl B C
x : ↥B
⊢ (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (((LinearMap.toContinuousLinearMap : (↥A →ₗ[𝕜] ↥B) ≃ₗ[𝕜] ↥A →L[𝕜] ↥B) : (a : ↥A →ₗ[𝕜] ↥B) → ↥A →L[𝕜] ↥B)
            ((B.projectionOnto C hBC).domRestrict A))
          p :
        (a : E) → ↥B)
      (↑x : E) =
    x

Tactic:
simp [hp ⟨x, hB x.2⟩]

Premises used: Subtype.mk, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜 F
inst_10 : T2Space F
f : E →L[𝕜] F
inst_11 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : E →ₗ[𝕜] F).range
suffices : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ (↑f : E →ₗ[𝕜] F).ker)
⊢ (↑f : E →ₗ[𝕜] F).ker.ClosedComplemented

Tactic:
suffices FiniteDimensional 𝕜 (E ⧸ f.ker) from .of_finiteDimensional_quotient f.isClosed_ker
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜 F
inst_10 : T2Space F
f : E →L[𝕜] F
inst_11 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : E →ₗ[𝕜] F).range
⊢ FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ (↑f : E →ₗ[𝕜] F).ker)

Tactic:
f.toLinearMap.quotKerEquivRange.symm.finiteDimensional

Premises used: LinearEquiv.symm, LinearEquiv.finiteDimensional, ContinuousLinearMap.toLinearMap, LinearMap.quotKerEquivRange
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜 F
inst_10 : T2Space F
f : E →L[𝕜] F
inst_11 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : E →ₗ[𝕜] F).range
⊢ FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ (↑f : E →ₗ[𝕜] F).ker)

Tactic:
exact f.toLinearMap.quotKerEquivRange.symm.finiteDimensional

Premises used: LinearEquiv.symm, LinearEquiv.finiteDimensional, ContinuousLinearMap.toLinearMap, LinearMap.quotKerEquivRange
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
map_add :
  ∀ (x y : E),
    ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
        ((f : (a : E) → F →ₗ[𝕜] G) (x + y)) =
      HAdd.hAdd (α := F →L[𝕜] G) (β := F →L[𝕜] G)
        (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
            ((f : (a : E) → F →ₗ[𝕜] G) x) :
          F →L[𝕜] G)
        (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
            ((f : (a : E) → F →ₗ[𝕜] G) y) :
          F →L[𝕜] G)
map_smul :
  ∀ (c : 𝕜) (x : E),
    ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
        ((f : (a : E) → F →ₗ[𝕜] G) (c • x)) =
      HSMul.hSMul (β := F →L[𝕜] G) c
        (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
            ((f : (a : E) → F →ₗ[𝕜] G) x) :
          F →L[𝕜] G)
⊢ IsLinearMap 𝕜 (M₂ := F →L[𝕜] G) fun (x : E) ↦
    ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G) ((f : (a : E) → F →ₗ[𝕜] G) x)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
x y : E
⊢ ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
      ((f : (a : E) → F →ₗ[𝕜] G) (x + y)) =
    HAdd.hAdd (α := F →L[𝕜] G) (β := F →L[𝕜] G)
      (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
          ((f : (a : E) → F →ₗ[𝕜] G) x) :
        F →L[𝕜] G)
      (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
          ((f : (a : E) → F →ₗ[𝕜] G) y) :
        F →L[𝕜] G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
c : 𝕜
x : E
⊢ ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
      ((f : (a : E) → F →ₗ[𝕜] G) (c • x)) =
    HSMul.hSMul (β := F →L[𝕜] G) c
      (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
          ((f : (a : E) → F →ₗ[𝕜] G) x) :
        F →L[𝕜] G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
x : E
y : F
⊢ Eq.{u_4 + 1} (α := G)
    (((((f.toContinuousBilinearMap : E →L[𝕜] F →L[𝕜] G) : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →ₗ[𝕜] G) x : F →ₗ[𝕜] G) : (a : F) → G) y : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E → F → G
h : IsBilinearMap 𝕜 f
x : E
y : F
⊢ ((((h.toContinuousBilinearMap : E →L[𝕜] F →L[𝕜] G) : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y = f x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
x : E
φ : E →L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F)
    (((((evalL 𝕜 E F : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F) : (a : E) → (E →L[𝕜] F) →L[𝕜] F) x : (E →L[𝕜] F) →L[𝕜] F) :
          (a : E →L[𝕜] F) → F)
        φ :
      F)
    ((φ : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosed
⊢ f.IsClosable

Tactic:
⟨f, hf.submodule_topologicalClosure_eq⟩

Premises used: IsClosed.submodule_topologicalClosure_eq, Exists.intro, LinearPMap.IsClosable
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hf : f.IsClosable
hfg : g ≤ f
obtain : ∀ (f' : E →ₗ.[R] F) (hf : f.graph.topologicalClosure = f'.graph), g.IsClosable
⊢ g.IsClosable

Tactic:
obtain ⟨f', hf⟩ := hf
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
rw : g.graph.topologicalClosure ≤ f.graph.topologicalClosure
⊢ g.graph.topologicalClosure ≤ f'.graph

Tactic:
rw [← hf]