awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ Eq.{u_4 + 1} (α := M₂)
    ((↑((e.submoduleMap p : (a : ↥p) → ↥(Submodule.map (↑(↑e : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) p)) x) : M₂) : M₂)
    ((e : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
p : Submodule R M
x : ↥(Submodule.map (↑(↑e : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) p)
⊢ Eq.{u_3 + 1} (α := M)
    ((↑(((e.submoduleMap p).symm : (a : ↥(Submodule.map (↑(↑e : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) p)) → ↥p) x) : M) : M)
    ((e.symm : (a : M₂) → M) (↑x : M₂) : M)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : Submodule.map (↑(↑e : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) p = q
x : ↥p
⊢ Eq.{u_4 + 1} (α := M₂) ((↑((e.ofSubmodules p q h : (a : ↥p) → ↥q) x) : M₂) : M₂) ((e : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : Submodule.map (↑(↑e : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) p = q
x : ↥q
⊢ Eq.{u_3 + 1} (α := M) ((↑(((e.ofSubmodules p q h).symm : (a : ↥q) → ↥p) x) : M) : M)
    ((e.symm : (a : M₂) → M) (↑x : M₂) : M)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
x_1 : ↥(Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U)
x : M
hx : x ∈ Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U
⊢ Membership.mem (α := M₂) U
    (((↑f : M →SL[σ₁₂] M₂) ∘SL (Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U).subtypeL :
          (a : ↥(Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U)) → M₂)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U) x hx) :
      M₂)

Tactic:
simpa [Submodule.mem_comap]

Premises used: Submodule.mem_comap
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ (↑(f.ofSubmodule' U) : ↥(Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U) →SL[σ₁₂] ↥U) =
    ((↑f : M →SL[σ₁₂] M₂) ∘SL (Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U).subtypeL).codRestrict U ⋯

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
x : ↥(Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U)
⊢ Eq.{u_4 + 1} (α := M₂)
    ((↑((f.ofSubmodule' U : (a : ↥(Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U)) → ↥U) x) : M₂) : M₂)
    ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
x : ↥U
⊢ Eq.{u_3 + 1} (α := M)
    ((↑(((f.ofSubmodule' U).symm : (a : ↥U) → ↥(Submodule.comap (↑(↑f : M ≃ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₂] M₂) U)) x) : M) : M)
    ((f.symm : (a : M₂) → M) (↑x : M₂) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : SMulCommClass R S W
inst_13 : SMul S R
inst_14 : IsScalarTower S R V
inst_15 : IsScalarTower S R W
α : Sˣ
e : V ≃L[R] W
x : V
⊢ (α • e : (a : V) → W) x = HSMul.hSMul (β := W) (↑α : S) ((e : (a : V) → W) x : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : SMulCommClass R S W
inst_13 : SMul S R
inst_14 : IsScalarTower S R V
inst_15 : IsScalarTower S R W
e : V ≃L[R] W
α : Sˣ
x : W
⊢ ((α • e).symm : (a : W) → V) x = HSMul.hSMul (β := V) (↑α⁻¹ : S) ((e.symm : (a : W) → V) x : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : SMulCommClass R S W
inst_13 : SMul S R
inst_14 : IsScalarTower S R V
inst_15 : IsScalarTower S R W
inst_16 : SMulCommClass R S V
e : V ≃L[R] W
α : Sˣ
⊢ (α • e).symm = α⁻¹ • e.symm

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : SMulCommClass R S W
inst_13 : SMul S R
inst_14 : IsScalarTower S R V
inst_15 : IsScalarTower S R W
e : V ≃L[R] W
α : Sˣ
⊢ (↑(α • e) : V ≃ₗ[R] W) = α • (↑e : V ≃ₗ[R] W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddCommMonoid G
inst_13 : Module R G
inst_14 : TopologicalSpace G
inst_15 : Module S G
inst_16 : ContinuousConstSMul S G
inst_17 : SMulCommClass R S W
inst_18 : SMul S R
inst_19 : IsScalarTower S R V
inst_20 : IsScalarTower S R W
inst_21 : SMulCommClass R S V
inst_22 : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
h :
  ∀ (x : G),
    Eq.{u_4 + 1} (α := W) (((α • e).trans f : (a : G) → W) x : W)
      ((HSMul.hSMul (β := G ≃L[R] W) α (e.trans f) : (a : G) → W) x : W)
⊢ (α • e).trans f = HSMul.hSMul (β := G ≃L[R] W) α (e.trans f)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddCommMonoid G
inst_13 : Module R G
inst_14 : TopologicalSpace G
inst_15 : Module S G
inst_16 : ContinuousConstSMul S G
inst_17 : SMulCommClass R S W
inst_18 : SMul S R
inst_19 : IsScalarTower S R V
inst_20 : IsScalarTower S R W
inst_21 : SMulCommClass R S V
inst_22 : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x : G
⊢ Eq.{u_4 + 1} (α := W) (((α • e).trans f : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃L[R] W) α (e.trans f) : (a : G) → W) x : W)

Tactic:
simp [LinearMapClass.map_smul_of_tower f]

Premises used: LinearMapClass.map_smul_of_tower
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddCommMonoid G
inst_13 : Module R G
inst_14 : TopologicalSpace G
inst_15 : Module S G
inst_16 : ContinuousConstSMul S G
inst_17 : SMulCommClass R S W
inst_18 : SMul S R
inst_19 : IsScalarTower S R V
inst_20 : IsScalarTower S R W
inst_21 : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
h :
  ∀ (x : G),
    Eq.{u_4 + 1} (α := W) ((e.trans (α • f) : (a : G) → W) x : W)
      ((HSMul.hSMul (β := G ≃L[R] W) α (e.trans f) : (a : G) → W) x : W)
⊢ e.trans (α • f) = HSMul.hSMul (β := G ≃L[R] W) α (e.trans f)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddCommMonoid G
inst_13 : Module R G
inst_14 : TopologicalSpace G
inst_15 : Module S G
inst_16 : ContinuousConstSMul S G
inst_17 : SMulCommClass R S W
inst_18 : SMul S R
inst_19 : IsScalarTower S R V
inst_20 : IsScalarTower S R W
inst_21 : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x : G
⊢ Eq.{u_4 + 1} (α := W) ((e.trans (α • f) : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃L[R] W) α (e.trans f) : (a : G) → W) x : W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : AddCommMonoid M
inst_6 : Module R M
N : Type u_4
inst_7 : TopologicalSpace N
inst_8 : AddCommMonoid N
inst_9 : Module S N
e : M ≃ₛₗ[σ] N
⊢ IsHomeomorph.{u_3, u_4} (X := M) (Y := N) (⇑e : (a : M) → N) ↔
    Continuous[inst_4, inst_7] (⇑e : (a : M) → N) ∧ Continuous[inst_7, inst_4] (⇑e.symm : (a : N) → M)

Tactic:
e.toEquiv.isHomeomorph_iff

Premises used: LinearEquiv.toEquiv, Equiv.isHomeomorph_iff
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : CommRing 𝕜
inst_6 : Module 𝕜 E
inst_7 : Module.Finite 𝕜 E
inst_8 : Module 𝕜 F
inst_9 : IsNoetherian 𝕜 F
inst_10 : ContinuousConstSMul 𝕜 F
⊢ Module.Finite 𝕜 (E →L[𝕜] F)

Tactic:
.of_injective (ContinuousLinearMap.coeLM 𝕜 : (E →L[𝕜] F) →ₗ[𝕜] E →ₗ[𝕜] F)
    ContinuousLinearMap.coe_injective

Premises used: Module.Finite.of_injective, ContinuousLinearMap.coeLM, ContinuousLinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : Field 𝕜
inst_6 : Module 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : Module 𝕜 F
inst_9 : FiniteDimensional 𝕜 F
inst_10 : ContinuousConstSMul 𝕜 F
⊢ FiniteDimensional 𝕜 (E →L[𝕜] F)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ t = UniformSpace.toTopologicalSpace

Tactic:
IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)

Premises used: inferInstance, IsTopologicalAddGroup.ext, le_antisymm
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
refine_1 : LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
refine_2 : LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
⊢ t = UniformSpace.toTopologicalSpace

Tactic:
refine IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)

Premises used: inferInstance, IsTopologicalAddGroup.ext, le_antisymm
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
refine_1 : ∀ (i' : ℝ), 0 < i' → Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 i')
⊢ LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)

Tactic:
rw [Metric.nhds_basis_closedBall.ge_iff]

Premises used: Filter.HasBasis.ge_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
refine_1 : ∀ (ξ₀ : 𝕜) (hξ₀ : 0 < ‖ξ₀‖) (hξ₀ε : ‖ξ₀‖ < ε), Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)

Tactic:
rcases NormedField.exists_norm_lt 𝕜 hε with ⟨ξ₀, hξ₀, hξ₀ε⟩

Premises used: NormedField.exists_norm_lt
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ

Tactic:
have : {ξ₀}ᶜ ∈ @nhds 𝕜 t 0 := IsOpen.mem_nhds isOpen_compl_singleton <|
      mem_compl_singleton_iff.mpr <| Ne.symm <| norm_ne_zero_iff.mp hξ₀.ne.symm
-- 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 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)

Tactic:
have : balancedCore 𝕜 {ξ₀}ᶜ ∈ @nhds 𝕜 t 0 := balancedCore_mem_nhds_zero this
-- 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 𝕜 {ξ₀}ᶜ)
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)

Tactic:
mem_of_superset this fun ξ hξ => ?_

Premises used: Filter.mem_of_superset
-- 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 𝕜 {ξ₀}ᶜ)
refine_1 :
  ∀ (ξ : 𝕜) (hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ),
    Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)

Tactic:
refine mem_of_superset this fun ξ hξ => ?_

Premises used: Filter.mem_of_superset
-- 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 𝕜 {ξ₀}ᶜ) ξ
pos : ∀ (hξ0 : ξ = 0), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
neg : ∀ (hξ0 : ¬ξ = 0), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ

Tactic:
by_cases hξ0 : ξ = 0
-- 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
pos : Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) 0
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ

Tactic:
rw [hξ0]
-- 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
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) 0

Tactic:
Metric.mem_closedBall_self hε.le

Premises used: Set.Mem, LT.lt.le, Metric.mem_closedBall_self
-- 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
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) 0

Tactic:
exact Metric.mem_closedBall_self hε.le

Premises used: LT.lt.le, Metric.mem_closedBall_self
-- 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
neg : ‖ξ‖ ≤ ε
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ

Tactic:
rw [mem_closedBall_zero_iff]

Premises used: mem_closedBall_zero_iff
-- 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
neg : ∀ (h : ε < ‖ξ‖), False
⊢ ‖ξ‖ ≤ ε

Tactic:
by_contra! h
-- 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_2 : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
this : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)
⊢ Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ₀

Tactic:
rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this

Premises used: mul_assoc, smul_eq_mul, mul_one, inv_mul_cancel₀
-- 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_2 : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
this : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ₀
⊢ False

Tactic:
notMem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this)

Premises used: Iff.mpr, Set.mem_singleton, Set.notMem_compl_iff, balancedCore_subset
-- 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_2 : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
ξ : 𝕜
hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
this : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ₀
⊢ False

Tactic:
exact notMem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this)

Premises used: Iff.mpr, Set.mem_singleton, Set.notMem_compl_iff, balancedCore_subset
-- 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 : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ((ξ₀ * ξ⁻¹) • ξ)
⊢ False

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)