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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
rw :
  Pairwise fun (x y : 𝕜) ↦
    ∃ (u : Set 𝕜) (v : Set 𝕜),
      IsOpen[induced (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance] u ∧
        IsOpen[induced (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
⊢ T2Space 𝕜

Tactic:
rw [t2Space_iff]

Premises used: t2Space_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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
⊢ Pairwise fun (x y : 𝕜) ↦
    ∃ (u : Set 𝕜) (v : Set 𝕜),
      IsOpen[induced (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance] u ∧
        IsOpen[induced (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
fun x y hxy =>
        @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
          (φ.toEquiv.symm.injective.ne hxy)

Premises used: separated_by_continuous, Function.Injective.ne, continuous_induced_dom, Pairwise, LinearEquiv.toEquiv, Equiv.injective, Equiv.symm
-- 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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
⊢ Pairwise fun (x y : 𝕜) ↦
    ∃ (u : Set 𝕜) (v : Set 𝕜),
      IsOpen[induced (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance] u ∧
        IsOpen[induced (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
exact fun x y hxy =>
        @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
          (φ.toEquiv.symm.injective.ne hxy)

Premises used: separated_by_continuous, Function.Injective.ne, continuous_induced_dom, LinearEquiv.toEquiv, Equiv.injective, Equiv.symm
-- 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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
⊢ Eq.{u + 1} (α := TopologicalSpace 𝕜)
    (induced.{u, v} (Y := E ⧸ l.ker) (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance)
    UniformSpace.toTopologicalSpace

Tactic:
have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace := by
      refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
        (continuousSMul_induced φ.symm.toMulActionHom) ?_
      rw [t2Space_iff]
      exact fun x y hxy =>
        @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
          (φ.toEquiv.symm.injective.ne hxy)
-- 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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this_1 : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
this :
  Eq.{u + 1} (α := TopologicalSpace 𝕜)
    (induced.{u, v} (Y := E ⧸ l.ker) (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance)
    UniformSpace.toTopologicalSpace
neg :
  Continuous[QuotientModule.Quotient.topologicalSpace l.ker, coinduced (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜) inferInstance]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
⊢ Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)

Tactic:
simp_rw +instances [this.symm, Equiv.induced_symm]

Premises used: Equiv.induced_symm, Eq.symm
-- 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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this_1 : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
this :
  Eq.{u + 1} (α := TopologicalSpace 𝕜)
    (induced.{u, v} (Y := E ⧸ l.ker) (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance)
    UniformSpace.toTopologicalSpace
⊢ Continuous[QuotientModule.Quotient.topologicalSpace l.ker, coinduced (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜) inferInstance]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)

Tactic:
continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- 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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : ¬finrank 𝕜 ↥l.range = 0
this_1 : finrank 𝕜 ↥l.range = 1
hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)
φ : LinearEquiv.{u, u, v, u} (RingHom.id 𝕜) (E ⧸ l.ker) 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ :
  Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
this :
  Eq.{u + 1} (α := TopologicalSpace 𝕜)
    (induced.{u, v} (Y := E ⧸ l.ker) (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance)
    UniformSpace.toTopologicalSpace
⊢ Continuous[QuotientModule.Quotient.topologicalSpace l.ker, coinduced (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜) inferInstance]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)

Tactic:
exact continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- 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
l : E →ₗ[𝕜] 𝕜
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜) ↔
    IsClosed[inst_2] (↑l.ker : Set E)

Tactic:
⟨fun h => isClosed_singleton.preimage h, l.continuous_of_isClosed_ker⟩

Premises used: Iff.intro, LinearMap.continuous_of_isClosed_ker, IsClosed.preimage, isClosed_singleton
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₂ : s.Nonempty
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)

Tactic:
l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => ?_)

Premises used: LinearMap.isClosed_or_dense_ker, LinearMap.continuous_of_isClosed_ker, Or.resolve_right
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₂ : s.Nonempty
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
refine : ∀ (hl : Dense (↑l.ker : Set E)), False
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)

Tactic:
refine l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => ?_)

Premises used: LinearMap.isClosed_or_dense_ker, LinearMap.continuous_of_isClosed_ker, Or.resolve_right
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₂ : s.Nonempty
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
rcases : ∀ (x : E) (hx : x ∈ s), False
⊢ False

Tactic:
rcases hs₂ with ⟨x, hx⟩
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
rw : (↑l.ker : Set E)ᶜ ∈ 𝓝 x
⊢ x ∈ interior (↑l.ker : Set E)ᶜ

Tactic:
rw [mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
⊢ (↑l.ker : Set E)ᶜ ∈ 𝓝 x

Tactic:
mem_of_superset (hs₁.mem_nhds hx) hs₃

Premises used: IsOpen.mem_nhds, Filter.mem_of_superset
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
⊢ (↑l.ker : Set E)ᶜ ∈ 𝓝 x

Tactic:
exact mem_of_superset (hs₁.mem_nhds hx) hs₃

Premises used: IsOpen.mem_nhds, Filter.mem_of_superset
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
⊢ x ∈ interior (↑l.ker : Set E)ᶜ

Tactic:
have : x ∈ interior (LinearMap.ker l : Set E)ᶜ := by
    rw [mem_interior_iff_mem_nhds]
    exact mem_of_superset (hs₁.mem_nhds hx) hs₃
-- 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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst_2] s
hs₃ : ∀ x ∈ s, Ne.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
hl : Dense (↑l.ker : Set E)
x : E
hx : x ∈ s
this : x ∈ interior (↑l.ker : Set E)ᶜ
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Membership.mem (γ := Set E) ∅ x), False
⊢ False

Tactic:
rwa [hl.interior_compl] at this

Premises used: Dense.interior_compl
-- 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 v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
have : ∀ (this : Fintype ι), Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
have := Fintype.ofFinite ι
-- 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 v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
this : ∀ (n : ℕ), Fintype.card ι = n → Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
this _ 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
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_3 : IsUniformAddGroup E := ⋯
this : ∀ (n : ℕ), Fintype.card ι = n → Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
exact this _ 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
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
suffices : ∀ (n : ℕ), Fintype.card ι = n → Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
suffices ∀ n, Fintype.card ι = n → Continuous ξ.equivFun by exact this _ rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = 0
⊢ IsEmpty ι

Tactic:
rw [Fintype.card_eq_zero_iff] at hn

Premises used: Fintype.card_eq_zero_iff
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
hn : IsEmpty ι
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
continuous_of_const fun x y => funext hn.elim

Premises used: IsEmpty.elim, continuous_of_const, funext
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst : CompleteSpace 𝕜
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
hn : IsEmpty ι
⊢ Continuous[inst_3, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
exact continuous_of_const fun x y => funext hn.elim

Premises used: IsEmpty.elim, continuous_of_const, funext
-- 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_3 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_4 : IsUniformAddGroup E := ⋯;
    ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
E : Type v
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
hn : Fintype.card ι = n + 1
⊢ FiniteDimensional 𝕜 E

Tactic:
haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite
-- 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
rw : Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = finrank.{u, v} 𝕜 ↥s
⊢ Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) : Type v) = n

Tactic:
rw [← s_dim]
-- 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) = finrank.{u, v} 𝕜 ↥s

Tactic:
(finrank_eq_card_basis b).symm

Premises used: Module.finrank_eq_card_basis, Eq.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_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) = finrank.{u, v} 𝕜 ↥s

Tactic:
exact (finrank_eq_card_basis b).symm

Premises used: Module.finrank_eq_card_basis, Eq.symm