awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 𝕜 {ξ₀}ᶜ) ξ
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
have pos : ∀ (hξ0 : ξ = 0), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
Tactic: by_cases hξ0 : ξ = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 𝕜 {ξ₀}ᶜ) ξ
pos : ∀ (hξ0 : ξ = 0), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
have neg : ∀ (hξ0 : ¬ξ = 0), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
Tactic: by_cases hξ0 : ξ = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
have pos : Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) 0
Tactic: rw [hξ0]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
have neg : ‖ξ‖ ≤ ε
Tactic: rw [mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
⊢ ‖ξ‖ ≤ ε
have neg : ∀ (h : ε < ‖ξ‖), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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_2 : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
this : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)
⊢ False
have this₁ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ₀
Tactic: rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 : ε < ‖ξ‖
⊢ False
have neg : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)
Tactic: suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ by
        rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this
        exact notMem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)
have neg : ‖ξ₀ * ξ⁻¹‖ ≤ 1
Tactic: refine (balancedCore_balanced _).smul_mem ?_ hξ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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 : ε < ‖ξ‖
⊢ ‖ξ₀ * ξ⁻¹‖ ≤ 1
have neg : ‖ξ₀‖ ≤ ‖ξ‖
Tactic: rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr hξ0), one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ 𝓝 (HSMul.hSMul (α := 𝕜) (β := 𝕜) 0 1) = 𝓝 0
have rw : Eq.{u + 1} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
have 𝕜₁ : Eq.{u + 1} (α := Filter 𝕜) (map id (𝓝 0)) (map (fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (id x) 1) (𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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))
⊢ LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
have 𝕜₂ : 𝓝 (HSMul.hSMul (α := 𝕜) (β := 𝕜) 0 1) = 𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have pos : ∀ (H : finrank 𝕜 ↥l.range = 0),
  Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
Tactic: by_cases H : finrank 𝕜 (LinearMap.range l) = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have neg : ∀ (H : ¬finrank 𝕜 ↥l.range = 0),
  Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
Tactic: by_cases H : finrank 𝕜 (LinearMap.range l) = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have H₁ : l = 0
Tactic: rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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] (⇑l : (a : E) → 𝕜)
have pos : Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑0 : (a : E) → 𝕜)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have this : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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) → 𝕜)
have rw : (l.ker.liftQ l sorry).ker = ⊥
Tactic: rw [← LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have hi : Function.Injective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l sorry) : (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 _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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) → 𝕜)
have rw : l.range = ⊤
Tactic: rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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) → 𝕜)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have hs : Function.Surjective.{v + 1, u + 1} (α := E ⧸ l.ker) (β := 𝕜) (⇑(l.ker.liftQ l sorry) : (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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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))
have 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 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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 ⋯) ⋯
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have hlφ : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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] (⇑l : (a : E) → 𝕜)
have rw : Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (Function.comp (β := E ⧸ l.ker) (⇑φ : (a : E ⧸ l.ker) → 𝕜) (⇑l.ker.mkQ : (a : E) → E ⧸ l.ker))
Tactic: rw [hlφ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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))
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑l : (a : E) → 𝕜)
have neg : Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
Tactic: suffices Continuous φ.toEquiv by
      rw [hlφ]
      exact this.comp continuous_quot_mk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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
have refine : T2Space 𝕜
Tactic: refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
        (continuousSMul_induced φ.symm.toMulActionHom) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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))
⊢ T2Space 𝕜
have 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
Tactic: rw [t2Space_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
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))
⊢ Continuous[QuotientModule.Quotient.topologicalSpace l.ker, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
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, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
have neg : Continuous[QuotientModule.Quotient.topologicalSpace l.ker, coinduced (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜) inferInstance]
  (⇑φ.toEquiv : (a : E ⧸ l.ker) → 𝕜)
Tactic: simp_rw +instances [this.symm, Equiv.induced_symm]