awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)

Tactic:
(balancedCore_balanced _).smul_mem ?_ hξ

Premises used: balancedCore_balanced, Balanced.smul_mem
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
neg : ‖ξ₀ * ξ⁻¹‖ ≤ 1
⊢ Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)

Tactic:
refine (balancedCore_balanced _).smul_mem ?_ hξ

Premises used: balancedCore_balanced, Balanced.smul_mem
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
neg : ‖ξ₀‖ ≤ ‖ξ‖
⊢ ‖ξ₀ * ξ⁻¹‖ ≤ 1

Tactic:
rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr hξ0), one_mul]

Premises used: Iff.mpr, norm_pos_iff, mul_inv_le_iff₀, norm_mul, norm_inv, one_mul
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ ‖ξ₀‖ ≤ ‖ξ‖

Tactic:
(hξ₀ε.trans h).le

Premises used: LT.lt.le, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ ‖ξ₀‖ ≤ ‖ξ‖

Tactic:
exact (hξ₀ε.trans h).le

Premises used: LT.lt.le, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ Eq.{u + 1} (α := Filter 𝕜) (𝓝 0) (map id (𝓝 0))

Tactic:
map_id.symm

Premises used: Filter.map_id, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ Eq.{u + 1} (α := Filter 𝕜) (map id (𝓝 0)) (map (fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (id x) 1) (𝓝 0))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ map (fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (id x) 1) (𝓝 0) ≤ 𝓝 (HSMul.hSMul (α := 𝕜) (β := 𝕜) 0 1)

Tactic:
(@Tendsto.smul_const _ _ _ hnorm.toUniformSpace.toTopologicalSpace t _ _ _ _ _
          tendsto_id (1 : 𝕜))

Premises used: Filter.tendsto_id, Filter.Tendsto, Filter.Tendsto.smul_const, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
rw rw₁ : Eq.{u + 1} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
⊢ 𝓝 (HSMul.hSMul (α := 𝕜) (β := 𝕜) 0 1) = 𝓝 0

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
𝕜₁ : Eq.{u + 1} (α := Filter 𝕜) (map id (𝓝 0)) (map (fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (id x) 1) (𝓝 0))
𝕜₂ : 𝓝 (HSMul.hSMul (α := 𝕜) (β := 𝕜) 0 1) = 𝓝 0
⊢ LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)

Tactic:
calc
      @nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0 =
          map id (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) :=
        map_id.symm
      _ = map (fun x => id x • (1 : 𝕜)) (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) := by
        simp
      _ ≤ @nhds 𝕜 t ((0 : 𝕜) • (1 : 𝕜)) :=
        (@Tendsto.smul_const _ _ _ hnorm.toUniformSpace.toTopologicalSpace t _ _ _ _ _
          tendsto_id (1 : 𝕜))
      _ = @nhds 𝕜 t 0 := by rw [zero_smul]

Premises used: Filter.tendsto_id, Filter.map, nhds, id, Filter.Tendsto.smul_const, Filter.map_id, HSMul.hSMul, OfNat.ofNat, 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)
pos :
  ∀ (H : finrank 𝕜 ↥l.range = 0),
    Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
neg :
  ∀ (H : ¬finrank 𝕜 ↥l.range = 0),
    Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)

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

Premises used: Membership.mem, LinearMap.range, Subtype, 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
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst_2] (↑l.ker : Set E)
H : finrank 𝕜 ↥l.range = 0
⊢ l = 0

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

Premises used: LinearMap.range_eq_bot, Submodule.finrank_eq_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
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 : l = 0
pos : Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑0 : (a : E) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)

Tactic:
rw [H]
-- 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 : l = 0
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑0 : (a : E) → 𝕜)

Tactic:
continuous_zero

Premises used: continuous_zero
-- 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 : l = 0
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑0 : (a : E) → 𝕜)

Tactic:
exact continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
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
⊢ finrank 𝕜 ↥l.range = 1

Tactic:
have : finrank 𝕜 (LinearMap.range l) = 1 :=
      le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range l).finrank_le) (zero_lt_iff.mpr H)
-- 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
rw : (l.ker.liftQ l ⋯).ker = ⊥
⊢ Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- 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
⊢ (l.ker.liftQ l ⋯).ker = ⊥

Tactic:
Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)

Premises used: le_refl, Submodule.ker_liftQ_eq_bot
-- 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
⊢ (l.ker.liftQ l ⋯).ker = ⊥

Tactic:
exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)

Premises used: le_refl, Submodule.ker_liftQ_eq_bot
-- 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
⊢ Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)

Tactic:
have hi : Function.Injective ((LinearMap.ker l).liftQ l (le_refl _)) := by
      rw [← LinearMap.ker_eq_bot]
      exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)
-- 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) → 𝕜)
rw : l.range = ⊤
⊢ Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)

Tactic:
rw [← LinearMap.range_eq_top, Submodule.range_liftQ]

Premises used: LinearMap.range_eq_top, Submodule.range_liftQ
-- 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) → 𝕜)
⊢ l.range = ⊤

Tactic:
Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)

Premises used: Eq.rec, Module.finrank_self, Eq.symm, Submodule.eq_top_of_finrank_eq
-- 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) → 𝕜)
⊢ l.range = ⊤

Tactic:
exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)

Premises used: Submodule.eq_top_of_finrank_eq
-- 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) → 𝕜)
⊢ Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l ⋯) : (a : E ⧸ l.ker) → 𝕜)

Tactic:
have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) := by
      rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
      exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
-- 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 ⋯) ⋯
h :
  ∀ (x : E),
    Eq.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
      (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker) x : 𝕜)
⊢ Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))

Tactic:
ext
-- 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 ⋯) ⋯
x : E
⊢ Eq.{u + 1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker) x : 𝕜)

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
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 ⋯) ⋯
⊢ Eq (α := (a : E) → 𝕜) (⇑l : (a : E) → 𝕜)
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))

Tactic:
have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext; 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
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 :
  Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
rw :
  Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)

Tactic:
rw [hlφ]
-- 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 :
  Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))

Tactic:
this.comp continuous_quot_mk

Premises used: Quotient.liftOn', AddCon.liftOn, Continuous.comp, continuous_quot_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
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 :
  Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))

Tactic:
exact this.comp continuous_quot_mk

Premises used: Continuous.comp, continuous_quot_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
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))
neg :
  Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)

Tactic:
suffices Continuous φ.toEquiv by
      rw [hlφ]
      exact this.comp continuous_quot_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
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:
unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
        (continuousSMul_induced φ.symm.toMulActionHom) ?_

Premises used: unique_topology_of_t2, LinearEquiv.symm, continuousSMul_induced, topologicalAddGroup_induced, LinearEquiv.toLinearMap, LinearMap.toMulActionHom
-- 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))
refine : T2Space 𝕜
⊢ Eq.{u + 1} (α := TopologicalSpace 𝕜)
    (induced.{u, v} (Y := E ⧸ l.ker) (⇑φ.toEquiv.symm : (a : 𝕜) → E ⧸ l.ker) inferInstance)
    UniformSpace.toTopologicalSpace

Tactic:
refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
        (continuousSMul_induced φ.symm.toMulActionHom) ?_

Premises used: unique_topology_of_t2, LinearEquiv.symm, continuousSMul_induced, topologicalAddGroup_induced, LinearEquiv.toLinearMap, LinearMap.toMulActionHom