awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
inst_7 : FiniteDimensional.{u_1, u_2} 𝕜 (E ⧸ s)
s_closed : IsClosed[inst_3] (↑s : Set E)
s_le_t : s ≤ t
⊢ IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)

Tactic:
exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

Premises used: Submodule.closed_of_finiteDimensional, continuous_quot_mk, IsClosed.preimage, Submodule.mkQ, Submodule.map
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
hs : IsClosed[inst_3] (↑s : Set E)
ht : FiniteDimensional.{u_1, u_2} 𝕜 ↥t
rw : IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)
⊢ IsClosed[inst_3] (↑(s ⊔ t) : Set E)

Tactic:
rw [← comap_map_mkQ]

Premises used: Submodule.comap_map_mkQ
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
hs : IsClosed[inst_3] (↑s : Set E)
ht : FiniteDimensional.{u_1, u_2} 𝕜 ↥t
⊢ IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)

Tactic:
(map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

Premises used: Set.Mem, Submodule.Quotient.mk, setOf, Submodule.closed_of_finiteDimensional, Set.preimage, continuous_quot_mk, IsClosed.preimage, Submodule.mkQ, Set.image, Submodule.map
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
hs : IsClosed[inst_3] (↑s : Set E)
ht : FiniteDimensional.{u_1, u_2} 𝕜 ↥t
⊢ IsClosed[inst_3] (↑(comap s.mkQ (map s.mkQ t)) : Set E)

Tactic:
exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

Premises used: Submodule.closed_of_finiteDimensional, continuous_quot_mk, IsClosed.preimage, Submodule.mkQ, Submodule.map
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module 𝕜 F
inst_11 : ContinuousSMul 𝕜 F
inst_12 : T2Space E
inst_13 : FiniteDimensional 𝕜 E
inst_14 : T2Space F
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
g : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) E ↥f.range := LinearEquiv.ofInjective f ⋯
⊢ IsClosed[inst_8] (Set.range.{u_3, u_2 + 1} (ι := E) (⇑f : (a : E) → F))

Tactic:
simpa [LinearMap.coe_range f] using (LinearMap.range f).closed_of_finiteDimensional

Premises used: Submodule.closed_of_finiteDimensional, LinearMap.range, LinearMap.coe_range
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
hc : c ≠ 0
⊢ IsClosedEmbedding.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c

Tactic:
LinearMap.isClosedEmbedding_of_injective (LinearMap.ker_toSpanSingleton 𝕜 hc)

Premises used: LinearMap.isClosedEmbedding_of_injective, LinearMap.ker_toSpanSingleton
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
pos : ∀ (hc : c = 0), IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
neg : ∀ (hc : ¬c = 0), IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
hc : c = 0
pos : IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ 0
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c

Tactic:
simp_rw [hc, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ 0

Tactic:
isClosedMap_const

Premises used: isClosedMap_const
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ 0

Tactic:
exact isClosedMap_const

Premises used: isClosedMap_const
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
hc : ¬c = 0
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c

Tactic:
(isClosedEmbedding_smul_left hc).isClosedMap

Premises used: Topology.IsClosedEmbedding.isClosedMap, isClosedEmbedding_smul_left
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : T2Space E
c : E
hc : ¬c = 0
⊢ IsClosedMap.{u_1, u_2} (Y := E) fun (x : 𝕜) ↦ x • c

Tactic:
exact (isClosedEmbedding_smul_left hc).isClosedMap

Premises used: Topology.IsClosedEmbedding.isClosedMap, isClosedEmbedding_smul_left
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module 𝕜 F
inst_11 : ContinuousSMul 𝕜 F
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 F
f : E →L[𝕜] F
hf : (↑f : E →ₗ[𝕜] F).range = ⊤
⊢ ∃ (g : F →L[𝕜] E), f ∘SL g = ContinuousLinearMap.id 𝕜 F

Tactic:
let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_rightInverse_of_surjective hf
  ⟨LinearMap.toContinuousLinearMap g, ContinuousLinearMap.coe_inj.1 hg⟩

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.coe_inj, LinearMap.exists_rightInverse_of_surjective, Exists, ContinuousLinearMap.toLinearMap, ContinuousLinearMap.id, Exists.intro, Iff.mp, _private.0.ContinuousLinearMap.exists_rightInverse_of_surjective.match_1, Eq, DFunLike.coe, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module 𝕜 F
inst_11 : ContinuousSMul 𝕜 F
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 F
f : E →L[𝕜] F
hf : (↑f : E →ₗ[𝕜] F).range = ⊤
⊢ IsQuotientMap.{u_2, u_3} (X := E) (Y := F) (⇑f : (a : E) → F)

Tactic:
let ⟨g, hg⟩ := f.exists_rightInverse_of_surjective hf
  .of_inverse g.continuous f.continuous (fun _ ↦ congr($hg _))

Premises used: congrArg, id, ContinuousLinearMap.continuous, _private.0.ContinuousLinearMap.isQuotientMap_of_finiteDimensional.match_1, Topology.IsQuotientMap, Topology.IsQuotientMap.of_inverse, DFunLike.coe, ContinuousLinearMap.exists_rightInverse_of_surjective
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module 𝕜 F
inst_11 : ContinuousSMul 𝕜 F
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 F
f : E →L[𝕜] F
⊢ Eq (α := Submodule 𝕜 ↥(↑f : E →ₗ[𝕜] F).range) (LinearMap.range (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range)) ⊤

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : Module 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module 𝕜 F
inst_11 : ContinuousSMul 𝕜 F
inst_12 : T2Space F
inst_13 : FiniteDimensional 𝕜 F
f : E →L[𝕜] F
⊢ IsQuotientMap.{u_2, u_3} (X := E) (Y := (↑(range.{u_3, u_2 + 1} (ι := E) (⇑f : (a : E) → F)) : Type u_3))
    (rangeFactorization (⇑f : (a : E) → F))

Tactic:
exact f.rangeRestrict.isQuotientMap_of_finiteDimensional (by simp)

Premises used: ContinuousLinearMap.rangeRestrict, ContinuousLinearMap.isQuotientMap_of_finiteDimensional
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
K : Type u_4
V : Type u_5
inst : NontriviallyNormedField K
inst_1 : CompleteSpace K
inst_2 : LocallyCompactSpace K
inst_3 : AddCommGroup V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : Module K V
inst_7 : ContinuousSMul K V
inst_8 : FiniteDimensional K V
⊢ LocallyCompactSpace V

Tactic:
suffices LocallyCompactSpace (SeparationQuotient V) from
    SeparationQuotient.isInducing_mk.locallyCompactSpace <|
      SeparationQuotient.range_mk (X := V) ▸ isClosed_univ.isLocallyClosed
  let ⟨_, ⟨b⟩⟩ := Basis.exists_basis K (SeparationQuotient V)
  have := FiniteDimensional.fintypeBasisIndex b
  b.equivFun.toContinuousLinearEquiv.toHomeomorph.isOpenEmbedding.locallyCompactSpace

Premises used: isClosed_univ, SeparationQuotient.isInducing_mk, SeparationQuotient.range_mk, Eq.rec, FiniteDimensional.fintypeBasisIndex, Topology.IsOpenEmbedding.locallyCompactSpace, _private.0.LocallyCompactSpace.of_finiteDimensional_of_complete.match_1, SeparationQuotient, IsClosed.isLocallyClosed, Module.Basis.exists_basis, ContinuousLinearEquiv.toHomeomorph, Homeomorph.isOpenEmbedding, LinearEquiv.toContinuousLinearEquiv, Topology.IsInducing.locallyCompactSpace, Eq.symm, LocallyCompactSpace, Module.Basis.equivFun
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
⊢ ∃ (c : 𝕜), 0 < ‖c‖ ∧ ‖c‖ < 1

Tactic:
NormedField.exists_norm_lt 𝕜 zero_lt_one

Premises used: zero_lt_one, NormedField.exists_norm_lt
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
obtain : ∀ (c : 𝕜) (hc0 : 0 < ‖c‖) (hc1 : ‖c‖ < 1), FiniteDimensional 𝕜 Eᵤ
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
obtain ⟨c, hc0, hc1⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < 1 := NormedField.exists_norm_lt 𝕜 zero_lt_one

Premises used: zero_lt_one, NormedField.exists_norm_lt
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
⊢ c ≠ 0

Tactic:
have hc_ne : c ≠ 0 := norm_pos_iff.mp hc0
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
obtain : ∀ (F : Set Eᵤ) (hF_finite : F.Finite) (hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U), FiniteDimensional 𝕜 Eᵤ
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
obtain ⟨F, hF_finite, hF_cover⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hU_tb
    (c • U) ((set_smul_mem_nhds_zero_iff hc_ne).mpr hU_nhds)

Premises used: Iff.mpr, set_smul_mem_nhds_zero_iff, Iff.mp, HSMul.hSMul, totallyBounded_iff_subset_finite_iUnion_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
x : Eᵤ
hx : x ∈ U
obtain :
  ∀ (f : Eᵤ) (hf : f ∈ F) (y : Eᵤ) (hy : y ∈ c • U) (hx : (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ U),
    (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ (↑M : Set Eᵤ) + c • U
⊢ x ∈ (↑M : Set Eᵤ) + c • U

Tactic:
obtain ⟨f, hf, y, hy, rfl⟩ := Set.mem_iUnion₂.mp <| hF_cover hx

Premises used: Set.mem_iUnion₂, Iff.mp, rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
f : Eᵤ
hf : f ∈ F
y : Eᵤ
hy : y ∈ c • U
hx : (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ U
⊢ (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ (↑M : Set Eᵤ) + c • U

Tactic:
⟨f, Submodule.subset_span hf, y, hy, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
f : Eᵤ
hf : f ∈ F
y : Eᵤ
hy : y ∈ c • U
hx : (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ U
⊢ (fun (x : Eᵤ) ↦ f +ᵥ x) y ∈ (↑M : Set Eᵤ) + c • U

Tactic:
exact ⟨f, Submodule.subset_span hf, y, hy, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
⊢ U ⊆ (↑M : Set Eᵤ) + c • U

Tactic:
have h_cover : U ⊆ M + c • U := fun x hx ↦ by
    obtain ⟨f, hf, y, hy, rfl⟩ := Set.mem_iUnion₂.mp <| hF_cover hx
    exact ⟨f, Submodule.subset_span hf, y, hy, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
⊢ U ⊆ (↑M : Set Eᵤ) + HPow.hPow (β := ℕ) c 0 • U

Tactic:
simpa using fun x hx ↦ ⟨0, M.zero_mem, x, hx, zero_add x⟩
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
⊢ U ⊆ (↑M : Set Eᵤ) + c ^ n • U

Tactic:
ih
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
⊢ (↑M : Set Eᵤ) + c ^ n • U ⊆ (↑M : Set Eᵤ) + c ^ n • ((↑M : Set Eᵤ) + c • U)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
rw : (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) + (c ^ n * c) • U ⊆ (↑M : Set Eᵤ) + (c ^ n * c) • U
⊢ (↑M : Set Eᵤ) + c ^ n • ((↑M : Set Eᵤ) + c • U) ⊆ (↑M : Set Eᵤ) + c ^ (n + 1) • U

Tactic:
rw [smul_add, smul_smul, pow_succ, ← add_assoc]

Premises used: pow_succ, add_assoc, smul_smul, smul_add
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
hxy : (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)
⊢ (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) + (c ^ n * c) • U ⊆ (↑M : Set Eᵤ) + (c ^ n * c) • U

Tactic:
congr!
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
⊢ IsUnit c

Tactic:
isUnit_iff_ne_zero.mpr hc_ne

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
h_cover : U ⊆ (↑M : Set Eᵤ) + c • U
n : ℕ
ih : U ⊆ (↑M : Set Eᵤ) + c ^ n • U
hxy :
  ∀ (c : 𝕜ˣ) (hc0 : 0 < ‖(↑c : 𝕜)‖) (hc1 : ‖(↑c : 𝕜)‖ < 1) (hc_ne : (↑c : 𝕜) ≠ 0)
    (hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ (↑c : 𝕜) • U) (h_cover : U ⊆ (↑M : Set Eᵤ) + (↑c : 𝕜) • U)
    (ih : U ⊆ (↑M : Set Eᵤ) + (↑c : 𝕜) ^ n • U), (↑M : Set Eᵤ) + (↑c : 𝕜) ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)
⊢ (↑M : Set Eᵤ) + c ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)

Tactic:
lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
Eᵤ : Type u_6
inst_2 : AddCommGroup Eᵤ
inst_3 : Module 𝕜 Eᵤ
inst_4 : UniformSpace Eᵤ
inst_5 : T2Space Eᵤ
inst_6 : IsUniformAddGroup Eᵤ
inst_7 : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : Membership.mem (γ := Filter Eᵤ) (𝓝 0) U
hU_tb : TotallyBounded U
F : Set Eᵤ
hF_finite : F.Finite
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional.{u_4, u_6} 𝕜 ↥M := ⋯
n : ℕ
c : 𝕜ˣ
hc0 : 0 < ‖(↑c : 𝕜)‖
hc1 : ‖(↑c : 𝕜)‖ < 1
hc_ne : (↑c : 𝕜) ≠ 0
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ (↑c : 𝕜) • U
h_cover : U ⊆ (↑M : Set Eᵤ) + (↑c : 𝕜) • U
ih : U ⊆ (↑M : Set Eᵤ) + (↑c : 𝕜) ^ n • U
⊢ (↑M : Set Eᵤ) + (↑c : 𝕜) ^ n • (↑M : Set Eᵤ) = (↑M : Set Eᵤ)

Tactic:
simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]

Premises used: Units.smul_def, Units.val_pow_eq_pow_val