[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ 𝔠 ≤ #𝕜
[PROOFSTEP]
suffices ∃ f : (ℕ → Bool) → 𝕜, range f ⊆ univ ∧ Continuous f ∧ Injective f
  by
  rcases this with ⟨f, -, -, f_inj⟩
  simpa using lift_mk_le_lift_mk_of_injective f_inj
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
this : ∃ f, range f ⊆ Set.univ ∧ Continuous f ∧ Injective f
⊢ 𝔠 ≤ #𝕜
[PROOFSTEP]
rcases this with ⟨f, -, -, f_inj⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : (ℕ → Bool) → 𝕜
f_inj : Injective f
⊢ 𝔠 ≤ #𝕜
[PROOFSTEP]
simpa using lift_mk_le_lift_mk_of_injective f_inj
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ ∃ f, range f ⊆ Set.univ ∧ Continuous f ∧ Injective f
[PROOFSTEP]
apply Perfect.exists_nat_bool_injection _ univ_nonempty
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ Perfect Set.univ
[PROOFSTEP]
refine ⟨isClosed_univ, preperfect_iff_nhds.2 (fun x _ U hU ↦ ?_)⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
⊢ ∃ y, y ∈ U ∩ Set.univ ∧ y ≠ x
[PROOFSTEP]
rcases NormedField.exists_norm_lt_one 𝕜 with ⟨c, c_pos, hc⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
⊢ ∃ y, y ∈ U ∩ Set.univ ∧ y ≠ x
[PROOFSTEP]
have A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 (x + 0)) :=
  tendsto_const_nhds.add (tendsto_pow_atTop_nhds_0_of_norm_lt_1 hc)
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 (x + 0))
⊢ ∃ y, y ∈ U ∩ Set.univ ∧ y ≠ x
[PROOFSTEP]
rw [add_zero] at A
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
⊢ ∃ y, y ∈ U ∩ Set.univ ∧ y ≠ x
[PROOFSTEP]
have B : ∀ᶠ n in atTop, x + c ^ n ∈ U := tendsto_def.1 A U hU
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
⊢ ∃ y, y ∈ U ∩ Set.univ ∧ y ≠ x
[PROOFSTEP]
rcases B.exists with ⟨n, hn⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ ∃ y, y ∈ U ∩ Set.univ ∧ y ≠ x
[PROOFSTEP]
refine ⟨x + c ^ n, by simpa using hn, ?_⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ∈ U ∩ Set.univ
[PROOFSTEP]
simpa using hn
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ≠ x
[PROOFSTEP]
simp only [ne_eq, add_right_eq_self]
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ ¬c ^ n = 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case intro.intro.intro.h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ c ≠ 0
[PROOFSTEP]
simpa using c_pos
[GOAL]
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ 𝔠 ≤ #E
[PROOFSTEP]
have A : lift.{v} (𝔠 : Cardinal.{u}) ≤ lift.{v} (#𝕜) := by
  simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜
[GOAL]
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ lift 𝔠 ≤ lift #𝕜
[PROOFSTEP]
simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜
[GOAL]
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
A : lift 𝔠 ≤ lift #𝕜
⊢ 𝔠 ≤ #E
[PROOFSTEP]
simpa using A.trans (Cardinal.mk_le_of_module 𝕜 E)
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
⊢ #↑s = #E
[PROOFSTEP]
obtain ⟨c, hc⟩ : ∃ x : 𝕜, 1 < ‖x‖ := NormedField.exists_lt_norm 𝕜 1
[GOAL]
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
⊢ #↑s = #E
[PROOFSTEP]
have cn_ne : ∀ n, c ^ n ≠ 0 := by
  intro n
  apply pow_ne_zero
  rintro rfl
  simp only [norm_zero] at hc
  exact lt_irrefl _ (hc.trans zero_lt_one)
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ (n : ℕ), c ^ n ≠ 0
[PROOFSTEP]
intro n
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ c ^ n ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ c ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
n : ℕ
hc : 1 < ‖0‖
⊢ False
[PROOFSTEP]
simp only [norm_zero] at hc
[GOAL]
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
n : ℕ
hc : 1 < 0
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (hc.trans zero_lt_one)
[GOAL]
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
⊢ #↑s = #E
[PROOFSTEP]
have A : ∀ (x : E), ∀ᶠ n in (atTop : Filter ℕ), x ∈ c ^ n • s :=
  by
  intro x
  have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) :=
    by
    have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) :=
      by
      simp_rw [← inv_pow]
      apply tendsto_pow_atTop_nhds_0_of_norm_lt_1
      rw [norm_inv]
      exact inv_lt_one hc
    exact Tendsto.smul_const this x
  rw [zero_smul] at this
  filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
  exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
⊢ ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
[PROOFSTEP]
intro x
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
[PROOFSTEP]
have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) :=
  by
  have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) :=
    by
    simp_rw [← inv_pow]
    apply tendsto_pow_atTop_nhds_0_of_norm_lt_1
    rw [norm_inv]
    exact inv_lt_one hc
  exact Tendsto.smul_const this x
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun n => (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))
[PROOFSTEP]
have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
  simp_rw [← inv_pow]
  apply tendsto_pow_atTop_nhds_0_of_norm_lt_1
  rw [norm_inv]
  exact inv_lt_one hc
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun n => (c ^ n)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
simp_rw [← inv_pow]
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun n => c⁻¹ ^ n) atTop (𝓝 0)
[PROOFSTEP]
apply tendsto_pow_atTop_nhds_0_of_norm_lt_1
[GOAL]
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ‖c⁻¹‖ < 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ‖c‖⁻¹ < 1
[PROOFSTEP]
exact inv_lt_one hc
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n => (c ^ n)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun n => (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))
[PROOFSTEP]
exact Tendsto.smul_const this x
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n => (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
[PROOFSTEP]
rw [zero_smul] at this
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n => (c ^ n)⁻¹ • x) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
[PROOFSTEP]
filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
[GOAL]
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n => (c ^ n)⁻¹ • x) atTop (𝓝 0)
n : ℕ
hn : (c ^ n)⁻¹ • x ∈ s
⊢ x ∈ c ^ n • s
[PROOFSTEP]
exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn
[GOAL]
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
⊢ #↑s = #E
[PROOFSTEP]
have B : ∀ n, #(c ^ n • s) = #s := by
  intro n
  have : c ^ n • s ≃ s :=
    { toFun := fun x ↦ ⟨(c ^ n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩
      invFun := fun x ↦ ⟨(c ^ n) • x.1, smul_mem_smul_set x.2⟩
      left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel (cn_ne n)]
      right_inv := fun x ↦ by simp [smul_smul, inv_mul_cancel (cn_ne n)] }
  exact Cardinal.mk_congr this
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
⊢ ∀ (n : ℕ), #↑(c ^ n • s) = #↑s
[PROOFSTEP]
intro n
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
n : ℕ
⊢ #↑(c ^ n • s) = #↑s
[PROOFSTEP]
have : c ^ n • s ≃ s :=
  { toFun := fun x ↦ ⟨(c ^ n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩
    invFun := fun x ↦ ⟨(c ^ n) • x.1, smul_mem_smul_set x.2⟩
    left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel (cn_ne n)]
    right_inv := fun x ↦ by simp [smul_smul, inv_mul_cancel (cn_ne n)] }
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
n : ℕ
x : ↑(c ^ n • s)
⊢ (fun x => { val := c ^ n • ↑x, property := (_ : c ^ n • ↑x ∈ c ^ n • s) })
      ((fun x => { val := (c ^ n)⁻¹ • ↑x, property := (_ : (c ^ n)⁻¹ • ↑x ∈ s) }) x) =
    x
[PROOFSTEP]
simp [smul_smul, mul_inv_cancel (cn_ne n)]
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
n : ℕ
x : ↑s
⊢ (fun x => { val := (c ^ n)⁻¹ • ↑x, property := (_ : (c ^ n)⁻¹ • ↑x ∈ s) })
      ((fun x => { val := c ^ n • ↑x, property := (_ : c ^ n • ↑x ∈ c ^ n • s) }) x) =
    x
[PROOFSTEP]
simp [smul_smul, inv_mul_cancel (cn_ne n)]
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
n : ℕ
this : ↑(c ^ n • s) ≃ ↑s
⊢ #↑(c ^ n • s) = #↑s
[PROOFSTEP]
exact Cardinal.mk_congr this
[GOAL]
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
B : ∀ (n : ℕ), #↑(c ^ n • s) = #↑s
⊢ #↑s = #E
[PROOFSTEP]
apply (Cardinal.mk_of_countable_eventually_mem A B).symm
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
⊢ #↑s = #E
[PROOFSTEP]
let g := Homeomorph.addLeft x
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
⊢ #↑s = #E
[PROOFSTEP]
let t := g ⁻¹' s
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ↑g ⁻¹' s
⊢ #↑s = #E
[PROOFSTEP]
have : t ∈ 𝓝 0 := g.continuous.continuousAt.preimage_mem_nhds (by simpa using hs)
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ↑g ⁻¹' s
⊢ s ∈ 𝓝 (↑g 0)
[PROOFSTEP]
simpa using hs
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ↑g ⁻¹' s
this : t ∈ 𝓝 0
⊢ #↑s = #E
[PROOFSTEP]
have A : #t = #E := cardinal_eq_of_mem_nhds_zero 𝕜 this
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ↑g ⁻¹' s
this : t ∈ 𝓝 0
A : #↑t = #E
⊢ #↑s = #E
[PROOFSTEP]
have B : #t = #s := Cardinal.mk_subtype_of_equiv s g.toEquiv
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ↑g ⁻¹' s
this : t ∈ 𝓝 0
A : #↑t = #E
B : #↑t = #↑s
⊢ #↑s = #E
[PROOFSTEP]
rwa [B] at A
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
h's : Set.Nonempty s
⊢ #↑s = #E
[PROOFSTEP]
rcases h's with ⟨x, hx⟩
[GOAL]
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
x : E
hx : x ∈ s
⊢ #↑s = #E
[PROOFSTEP]
exact cardinal_eq_of_mem_nhds 𝕜 (hs.mem_nhds hx)
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
h's : Set.Nonempty s
⊢ 𝔠 ≤ #↑s
[PROOFSTEP]
simpa [cardinal_eq_of_is_open 𝕜 hs h's] using continuum_le_cardinal_of_module 𝕜 E
[GOAL]
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Set.Countable s
⊢ Dense sᶜ
[PROOFSTEP]
rw [← interior_eq_empty_iff_dense_compl]
[GOAL]
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Set.Countable s
⊢ interior s = ∅
[PROOFSTEP]
by_contra H
[GOAL]
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Set.Countable s
H : ¬interior s = ∅
⊢ False
[PROOFSTEP]
apply lt_irrefl (ℵ₀ : Cardinal.{u})
[GOAL]
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Set.Countable s
H : ¬interior s = ∅
⊢ ℵ₀ < ℵ₀
[PROOFSTEP]
calc
  (ℵ₀ : Cardinal.{u}) < 𝔠 := aleph0_lt_continuum
  _ ≤ #(interior s) := (continuum_le_cardinal_of_is_open 𝕜 isOpen_interior (nmem_singleton_empty.1 H))
  _ ≤ #s := (mk_le_mk_of_subset interior_subset)
  _ ≤ ℵ₀ := le_aleph0 hs


[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
⊢ LocallyCompactSpace G
[PROOFSTEP]
refine' locally_compact_of_compact_nhds fun x => _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x : G
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
[PROOFSTEP]
obtain ⟨y, hy⟩ := K.interior_nonempty
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
[PROOFSTEP]
let F := Homeomorph.mulLeft (x * y⁻¹)
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
[PROOFSTEP]
refine' ⟨F '' K, _, K.isCompact.image F.continuous⟩
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑F '' ↑K ∈ 𝓝 x
[PROOFSTEP]
suffices F.symm ⁻¹' K ∈ 𝓝 x by
  convert this using 1
  apply Equiv.image_eq_preimage
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K ∈ 𝓝 x
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K = ↑(Homeomorph.symm F) ⁻¹' ↑K
[PROOFSTEP]
apply Equiv.image_eq_preimage
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
[PROOFSTEP]
apply ContinuousAt.preimage_mem_nhds F.symm.continuous.continuousAt
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
[PROOFSTEP]
have : F.symm x = y := by
  simp only [Homeomorph.mulLeft_symm, mul_inv_rev, inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) x = y
[PROOFSTEP]
simp only [Homeomorph.mulLeft_symm, mul_inv_rev, inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
[PROOFSTEP]
rw [this]
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 y
[PROOFSTEP]
exact mem_interior_iff_mem_nhds.1 hy
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
let F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.1 • p.2
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
change Continuous F
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous F
[PROOFSTEP]
have H : Continuous (F ∘ fun p : G × G => (p.1, QuotientGroup.mk p.2)) :=
  by
  change Continuous fun p : G × G => QuotientGroup.mk (p.1 * p.2)
  refine' continuous_coinduced_rng.comp continuous_mul
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous (F ∘ fun p => (p.fst, ↑p.snd))
[PROOFSTEP]
change Continuous fun p : G × G => QuotientGroup.mk (p.1 * p.2)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous fun p => ↑(p.fst * p.snd)
[PROOFSTEP]
refine' continuous_coinduced_rng.comp continuous_mul
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
H : Continuous (F ∘ fun p => (p.fst, ↑p.snd))
⊢ Continuous F
[PROOFSTEP]
exact QuotientMap.continuous_lift_prod_right quotientMap_quotient_mk' H


[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hf : IsClosable f
hfg : g ≤ f
⊢ IsClosable g
[PROOFSTEP]
cases' hf with f' hf
[GOAL]
case intro
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
⊢ IsClosable g
[PROOFSTEP]
have : g.graph.topologicalClosure ≤ f'.graph := by
  rw [← hf]
  exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
⊢ Submodule.topologicalClosure (graph g) ≤ graph f'
[PROOFSTEP]
rw [← hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
⊢ Submodule.topologicalClosure (graph g) ≤ Submodule.topologicalClosure (graph f)
[PROOFSTEP]
exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
[GOAL]
case intro
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
this : Submodule.topologicalClosure (graph g) ≤ graph f'
⊢ IsClosable g
[PROOFSTEP]
use g.graph.topologicalClosure.toLinearPMap
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
this : Submodule.topologicalClosure (graph g) ≤ graph f'
⊢ Submodule.topologicalClosure (graph g) = graph (Submodule.toLinearPMap (Submodule.topologicalClosure (graph g)))
[PROOFSTEP]
rw [Submodule.toLinearPMap_graph_eq]
[GOAL]
case h.hg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
this : Submodule.topologicalClosure (graph g) ≤ graph f'
⊢ ∀ (x : E × F), x ∈ Submodule.topologicalClosure (graph g) → x.fst = 0 → x.snd = 0
[PROOFSTEP]
exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ ∃! f', Submodule.topologicalClosure (graph f) = graph f'
[PROOFSTEP]
refine' exists_unique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph _
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
x✝¹ x✝ : E →ₗ.[R] F
hy₁ : Submodule.topologicalClosure (graph f) = graph x✝¹
hy₂ : Submodule.topologicalClosure (graph f) = graph x✝
⊢ graph x✝¹ = graph x✝
[PROOFSTEP]
rw [← hy₁, ← hy₂]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ closure f = Exists.choose hf
[PROOFSTEP]
simp [closure, hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬IsClosable f
⊢ closure f = f
[PROOFSTEP]
simp [closure, hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ Submodule.topologicalClosure (graph f) = graph (closure f)
[PROOFSTEP]
rw [closure_def hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ Submodule.topologicalClosure (graph f) = graph (Exists.choose hf)
[PROOFSTEP]
exact hf.choose_spec
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f ≤ closure f
[PROOFSTEP]
by_cases hf : f.IsClosable
[GOAL]
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ f ≤ closure f
[PROOFSTEP]
refine' le_of_le_graph _
[GOAL]
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ graph f ≤ graph (closure f)
[PROOFSTEP]
rw [← hf.graph_closure_eq_closure_graph]
[GOAL]
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ graph f ≤ Submodule.topologicalClosure (graph f)
[PROOFSTEP]
exact (graph f).le_topologicalClosure
[GOAL]
case neg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬IsClosable f
⊢ f ≤ closure f
[PROOFSTEP]
rw [closure_def' hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ closure f ≤ closure g
[PROOFSTEP]
refine' le_of_le_graph _
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ graph (closure f) ≤ graph (closure g)
[PROOFSTEP]
rw [← (hg.leIsClosable h).graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ Submodule.topologicalClosure (graph f) ≤ graph (closure g)
[PROOFSTEP]
rw [← hg.graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ Submodule.topologicalClosure (graph f) ≤ Submodule.topologicalClosure (graph g)
[PROOFSTEP]
exact Submodule.topologicalClosure_mono (le_graph_of_le h)
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ IsClosed (closure f)
[PROOFSTEP]
rw [IsClosed, ← hf.graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ _root_.IsClosed ↑(Submodule.topologicalClosure (graph f))
[PROOFSTEP]
exact f.graph.isClosed_topologicalClosure
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ HasCore (closure f) f.domain
[PROOFSTEP]
refine' ⟨f.le_closure.1, _⟩
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ closure (domRestrict (closure f) f.domain) = closure f
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ domRestrict (closure f) f.domain = f
[PROOFSTEP]
ext x y hxy
[GOAL]
case e_f.h.h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
⊢ x ∈ (domRestrict (closure f) f.domain).domain ↔ x ∈ f.domain
[PROOFSTEP]
simp only [domRestrict_domain, Submodule.mem_inf, and_iff_left_iff_imp]
[GOAL]
case e_f.h.h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
⊢ x ∈ f.domain → x ∈ (closure f).domain
[PROOFSTEP]
intro hx
[GOAL]
case e_f.h.h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
hx : x ∈ f.domain
⊢ x ∈ (closure f).domain
[PROOFSTEP]
exact f.le_closure.1 hx
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
⊢ ↑(domRestrict (closure f) f.domain) x = ↑f y
[PROOFSTEP]
let z : f.closure.domain := ⟨y.1, f.le_closure.1 y.2⟩
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
⊢ ↑(domRestrict (closure f) f.domain) x = ↑f y
[PROOFSTEP]
have hyz : (y : E) = z := by simp
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
⊢ ↑y = ↑z
[PROOFSTEP]
simp
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
hyz : ↑y = ↑z
⊢ ↑(domRestrict (closure f) f.domain) x = ↑f y
[PROOFSTEP]
rw [f.le_closure.2 hyz]
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
hyz : ↑y = ↑z
⊢ ↑(domRestrict (closure f) f.domain) x = ↑(closure f) z
[PROOFSTEP]
exact domRestrict_apply (hxy.trans hyz)
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ graph (inverse (closure f)) = Submodule.topologicalClosure (graph (inverse f))
[PROOFSTEP]
rw [inverse_graph hf, inverse_graph hcf, ← hf'.graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ Submodule.map (LinearEquiv.prodComm R E F) (Submodule.topologicalClosure (graph f)) =
    Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f))
[PROOFSTEP]
apply SetLike.ext'
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ ↑(Submodule.map (LinearEquiv.prodComm R E F) (Submodule.topologicalClosure (graph f))) =
    ↑(Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f)))
[PROOFSTEP]
simp only [Submodule.topologicalClosure_coe, Submodule.map_coe, LinearEquiv.prodComm_apply]
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ (fun a => Prod.swap a) '' _root_.closure ↑(graph f) = _root_.closure ((fun a => Prod.swap a) '' ↑(graph f))
[PROOFSTEP]
apply (image_closure_subset_closure_image continuous_swap).antisymm
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
have h1 := Set.image_equiv_eq_preimage_symm f.graph (LinearEquiv.prodComm R E F).toEquiv
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 :
  ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)) '' ↑(graph f) =
    ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)).symm ⁻¹' ↑(graph f)
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
have h2 := Set.image_equiv_eq_preimage_symm (_root_.closure f.graph) (LinearEquiv.prodComm R E F).toEquiv
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 :
  ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)) '' ↑(graph f) =
    ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)).symm ⁻¹' ↑(graph f)
h2 :
  ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)) '' _root_.closure ↑(graph f) =
    ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)).symm ⁻¹' _root_.closure ↑(graph f)
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply, LinearEquiv.coe_toEquiv_symm] at h1 h2
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 : (fun a => Prod.swap a) '' ↑(graph f) = ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' ↑(graph f)
h2 :
  (fun a => Prod.swap a) '' _root_.closure ↑(graph f) =
    ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' _root_.closure ↑(graph f)
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
rw [h1, h2]
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 : (fun a => Prod.swap a) '' ↑(graph f) = ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' ↑(graph f)
h2 :
  (fun a => Prod.swap a) '' _root_.closure ↑(graph f) =
    ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' _root_.closure ↑(graph f)
⊢ _root_.closure (↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' ↑(graph f)) ⊆
    ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' _root_.closure ↑(graph f)
[PROOFSTEP]
apply continuous_swap.closure_preimage_subset
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
⊢ IsClosable (inverse f) ↔ LinearMap.ker (closure f).toFun = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
⊢ IsClosable (inverse f) → LinearMap.ker (closure f).toFun = ⊥
[PROOFSTEP]
intro ⟨f', h⟩
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
⊢ LinearMap.ker (closure f).toFun = ⊥
[PROOFSTEP]
rw [LinearMap.ker_eq_bot']
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
⊢ ∀ (m : { x // x ∈ (closure f).domain }), ↑(closure f).toFun m = 0 → m = 0
[PROOFSTEP]
intro ⟨x, hx⟩ hx'
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : ↑(closure f).toFun { val := x, property := hx } = 0
⊢ { val := x, property := hx } = 0
[PROOFSTEP]
simp only [Submodule.mk_eq_zero]
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : ↑(closure f).toFun { val := x, property := hx } = 0
⊢ x = 0
[PROOFSTEP]
rw [toFun_eq_coe, eq_comm, image_iff] at hx'
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
⊢ x = 0
[PROOFSTEP]
have : (0, x) ∈ graph f'
[GOAL]
case this
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
⊢ (0, x) ∈ graph f'
[PROOFSTEP]
rw [← h, inverse_graph hf]
[GOAL]
case this
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
⊢ (0, x) ∈ Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f))
[PROOFSTEP]
rw [← hf'.graph_closure_eq_closure_graph, ← SetLike.mem_coe, Submodule.topologicalClosure_coe] at hx'
[GOAL]
case this
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ _root_.closure ↑(graph f)
⊢ (0, x) ∈ Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f))
[PROOFSTEP]
apply image_closure_subset_closure_image continuous_swap
[GOAL]
case this.a
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ _root_.closure ↑(graph f)
⊢ (0, x) ∈ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
[GOAL]
case this.a
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ _root_.closure ↑(graph f)
⊢ ∃ a b, (a, b) ∈ _root_.closure ↑(graph f) ∧ b = 0 ∧ a = x
[PROOFSTEP]
exact ⟨x, 0, hx', rfl, rfl⟩
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
this : (0, x) ∈ graph f'
⊢ x = 0
[PROOFSTEP]
exact graph_fst_eq_zero_snd f' this rfl
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
⊢ LinearMap.ker (closure f).toFun = ⊥ → IsClosable (inverse f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
h : LinearMap.ker (closure f).toFun = ⊥
⊢ IsClosable (inverse f)
[PROOFSTEP]
use f.closure.inverse
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
h : LinearMap.ker (closure f).toFun = ⊥
⊢ Submodule.topologicalClosure (graph (inverse f)) = graph (inverse (closure f))
[PROOFSTEP]
exact (closure_inverse_graph hf hf' h).symm
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ closure (inverse f) = inverse (closure f)
[PROOFSTEP]
apply eq_of_eq_graph
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ graph (closure (inverse f)) = graph (inverse (closure f))
[PROOFSTEP]
rw [closure_inverse_graph hf hf' hcf, ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]


[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LE α
inst✝¹ : TopologicalSpace β
inst✝ : LE β
s t : ClopenUpperSet α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LE α
inst✝¹ : TopologicalSpace β
inst✝ : LE β
t : ClopenUpperSet α
carrier✝ : Set α
clopen'✝ : IsClopen carrier✝
upper'✝ : IsUpperSet { carrier := carrier✝, clopen' := clopen'✝ }.carrier
h :
  (fun s => s.carrier) { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ } =
    (fun s => s.carrier) t
⊢ { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LE α
inst✝¹ : TopologicalSpace β
inst✝ : LE β
carrier✝¹ : Set α
clopen'✝¹ : IsClopen carrier✝¹
upper'✝¹ : IsUpperSet { carrier := carrier✝¹, clopen' := clopen'✝¹ }.carrier
carrier✝ : Set α
clopen'✝ : IsClopen carrier✝
upper'✝ : IsUpperSet { carrier := carrier✝, clopen' := clopen'✝ }.carrier
h :
  (fun s => s.carrier) { toClopens := { carrier := carrier✝¹, clopen' := clopen'✝¹ }, upper' := upper'✝¹ } =
    (fun s => s.carrier) { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ }
⊢ { toClopens := { carrier := carrier✝¹, clopen' := clopen'✝¹ }, upper' := upper'✝¹ } =
    { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ }
[PROOFSTEP]
congr


[GOAL]
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TrivialStar R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : StarAddMonoid A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousStar A
src✝ : A ≃+ A := AddEquiv.refl A
r : R
a : A
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : A), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • a) =
    ↑(starRingEnd R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : A), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        a
[PROOFSTEP]
simp [starRingEnd_apply]


[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤
[PROOFSTEP]
suffices ∀ i j : ℕ, ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j by
  simpa only [smul_eq_mul, mul_top, Algebra.id.map_eq_id, map_id, le_inf_iff] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤
[PROOFSTEP]
simpa only [smul_eq_mul, mul_top, Algebra.id.map_eq_id, map_id, le_inf_iff] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
[PROOFSTEP]
intro i j
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
[PROOFSTEP]
exact ⟨max i j, pow_le_pow (le_max_left i j), pow_le_pow (le_max_right i j)⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤
[PROOFSTEP]
suffices ∀ (a : R) (i : ℕ), ∃ j : ℕ, a • I ^ j ≤ I ^ i by
  simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤
[PROOFSTEP]
simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
[PROOFSTEP]
intro r n
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ ∃ j, r • I ^ j ≤ I ^ n
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ r • I ^ n ≤ I ^ n
[PROOFSTEP]
rintro a ⟨x, hx, rfl⟩
[GOAL]
case h.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
x : R
hx : x ∈ ↑(I ^ n)
⊢ ↑(DistribMulAction.toLinearMap R R r) x ∈ I ^ n
[PROOFSTEP]
exact (I ^ n).smul_mem r hx
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)
[PROOFSTEP]
suffices ∀ i : ℕ, ∃ j : ℕ, (I ^ j : Set R) * (I ^ j : Set R) ⊆ (I ^ i : Set R) by
  simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)
[PROOFSTEP]
simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ n)
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ↑(I ^ n) * ↑(I ^ n) ⊆ ↑(I ^ n)
[PROOFSTEP]
rintro a ⟨x, b, _hx, hb, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x b : R
_hx : x ∈ ↑(I ^ n)
hb : b ∈ ↑(I ^ n)
⊢ (fun x x_1 => x * x_1) x b ∈ ↑(I ^ n)
[PROOFSTEP]
exact (I ^ n).smul_mem x hb
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t
[PROOFSTEP]
intro U
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
[PROOFSTEP]
rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U) → ∃ i, True ∧ ↑(I ^ i) ⊆ U
[PROOFSTEP]
rintro ⟨-, ⟨i, rfl⟩, h⟩
[GOAL]
case mp.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ∃ i, True ∧ ↑(I ^ i) ⊆ U
[PROOFSTEP]
replace h : ↑(I ^ i) ⊆ U := by simpa using h
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ↑(I ^ i) ⊆ U
[PROOFSTEP]
simpa using h
[GOAL]
case mp.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i, True ∧ ↑(I ^ i) ⊆ U
[PROOFSTEP]
exact ⟨i, trivial, h⟩
[GOAL]
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U
[PROOFSTEP]
rintro ⟨i, -, h⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U
[PROOFSTEP]
exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ↑(I ^ i) = ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
⊢ HasBasis (𝓝 x) (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
[PROOFSTEP]
letI := I.adicTopology
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this : TopologicalSpace R := adicTopology I
⊢ HasBasis (𝓝 x) (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
[PROOFSTEP]
have := I.hasBasis_nhds_zero_adic.map fun y => x + y
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := adicTopology I
this : HasBasis (Filter.map (fun y => x + y) (𝓝 0)) (fun _n => True) fun i => (fun y => x + y) '' ↑(I ^ i)
⊢ HasBasis (𝓝 x) (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
[PROOFSTEP]
rwa [map_add_left_nhds_zero x] at this
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
⊢ ↑(I ^ i • ⊤) = ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
[PROOFSTEP]
replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ I ^ i
[PROOFSTEP]
simpa [(I ^ i).mul_top] using a_in
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
[PROOFSTEP]
exact smul_mem_smul a_in mem_top
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ OpenAddSubgroup R
[PROOFSTEP]
letI := I.adicTopology
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ OpenAddSubgroup R
[PROOFSTEP]
refine ⟨(I ^ n).toAddSubgroup, ?_⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ IsOpen (toAddSubgroup (I ^ n)).toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
convert (I.adic_basis.toRing_subgroups_basis.openAddSubgroup n).isOpen
[GOAL]
case h.e'_3
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ (toAddSubgroup (I ^ n)).toAddSubmonoid.toAddSubsemigroup.carrier =
    ↑(RingSubgroupsBasis.openAddSubgroup (_ : RingSubgroupsBasis fun i => toAddSubgroup (I ^ i • ⊤)) n)
[PROOFSTEP]
change (I ^ n : Set R) = (I ^ n • (⊤ : Ideal R) : Set R)
[GOAL]
case h.e'_3
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ ↑(I ^ n) = ↑(I ^ n • ⊤)
[PROOFSTEP]
simp [smul_top_eq_map, Algebra.id.map_eq_id, map_id, restrictScalars_self]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
⊢ IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
⊢ IsAdic J → (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : IsAdic J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
change _ = _ at H
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
rw [H]
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
letI := J.adicTopology
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
⊢ ∀ (n : ℕ), IsOpen ↑(J ^ n)
[PROOFSTEP]
intro n
[GOAL]
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
n : ℕ
⊢ IsOpen ↑(J ^ n)
[PROOFSTEP]
exact (J.openAddSubgroup n).isOpen'
[GOAL]
case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
⊢ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
intro s hs
[GOAL]
case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
s : Set R
hs : s ∈ 𝓝 0
⊢ ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
simpa using J.hasBasis_nhds_zero_adic.mem_iff.mp hs
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J
[PROOFSTEP]
rintro ⟨H₁, H₂⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ IsAdic J
[PROOFSTEP]
apply TopologicalAddGroup.ext
[GOAL]
case mpr.intro.tg
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ TopologicalAddGroup R
[PROOFSTEP]
apply @TopologicalRing.to_topologicalAddGroup
[GOAL]
case mpr.intro.tg'
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ TopologicalAddGroup R
[PROOFSTEP]
apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup
[GOAL]
case mpr.intro.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ 𝓝 0 = 𝓝 0
[PROOFSTEP]
ext s
[GOAL]
case mpr.intro.h.a
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
[PROOFSTEP]
letI := Ideal.adic_basis J
[GOAL]
case mpr.intro.h.a
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
[PROOFSTEP]
rw [J.hasBasis_nhds_zero_adic.mem_iff]
[GOAL]
case mpr.intro.h.a
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(J ^ i) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.h.a.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 → ∃ i, True ∧ ↑(J ^ i) ⊆ s
[PROOFSTEP]
intro H
[GOAL]
case mpr.intro.h.a.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ (∃ i, True ∧ ↑(J ^ i) ⊆ s) → s ∈ 𝓝 0
[PROOFSTEP]
intro H
[GOAL]
case mpr.intro.h.a.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s
[PROOFSTEP]
rcases H₂ s H with ⟨n, h⟩
[GOAL]
case mpr.intro.h.a.mp.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
n : ℕ
h : ↑(J ^ n) ⊆ s
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s
[PROOFSTEP]
exact ⟨n, trivial, h⟩
[GOAL]
case mpr.intro.h.a.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0
[PROOFSTEP]
rcases H with ⟨n, -, hn⟩
[GOAL]
case mpr.intro.h.a.mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ s ∈ 𝓝 0
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case mpr.intro.h.a.mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ ∃ t, t ⊆ s ∧ IsOpen t ∧ 0 ∈ t
[PROOFSTEP]
refine' ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : IsAdic J
n : ℕ
hn : 0 < n
⊢ IsAdic (J ^ n)
[PROOFSTEP]
rw [isAdic_iff] at h ⊢
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ (∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)
[PROOFSTEP]
intro m
[GOAL]
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen ↑((J ^ n) ^ m)
[PROOFSTEP]
rw [← pow_mul]
[GOAL]
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen ↑(J ^ (n * m))
[PROOFSTEP]
apply h.left
[GOAL]
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
[PROOFSTEP]
intro V hV
[GOAL]
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
[PROOFSTEP]
cases' h.right V hV with m hm
[GOAL]
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
[PROOFSTEP]
use m
[GOAL]
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ V
[PROOFSTEP]
refine' Set.Subset.trans _ hm
[GOAL]
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ ↑(J ^ m)
[PROOFSTEP]
cases n
[GOAL]
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < Nat.zero
⊢ ↑((J ^ Nat.zero) ^ m) ⊆ ↑(J ^ m)
[PROOFSTEP]
exfalso
[GOAL]
case h.zero.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < Nat.zero
⊢ False
[PROOFSTEP]
exact Nat.not_succ_le_zero 0 hn
[GOAL]
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ ↑((J ^ Nat.succ n✝) ^ m) ⊆ ↑(J ^ m)
[PROOFSTEP]
rw [← pow_mul, Nat.succ_mul]
[GOAL]
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ ↑(J ^ (n✝ * m + m)) ⊆ ↑(J ^ m)
[PROOFSTEP]
apply Ideal.pow_le_pow
[GOAL]
case h.succ.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ m ≤ n✝ * m + m
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ IsAdic ⊥ ↔ DiscreteTopology A
[PROOFSTEP]
rw [isAdic_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) ↔ DiscreteTopology A
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) → DiscreteTopology A
[PROOFSTEP]
rintro ⟨h, _h'⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ DiscreteTopology A
[PROOFSTEP]
rw [discreteTopology_iff_open_singleton_zero]
[GOAL]
case mp.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen {0}
[PROOFSTEP]
simpa using h 1
[GOAL]
case mpr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
[PROOFSTEP]
intros
[GOAL]
case mpr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mpr.left
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
[PROOFSTEP]
simp
[GOAL]
case mpr.right
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
[PROOFSTEP]
intro U U_nhds
[GOAL]
case mpr.right
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ∃ n, ↑(⊥ ^ n) ⊆ U
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ↑(⊥ ^ 1) ⊆ U
[PROOFSTEP]
simp [mem_of_mem_nhds U_nhds]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
⊢ NonarchimedeanRing R
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
⊢ TopologicalRing (UniformSpace.Completion R)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ TopologicalAddGroup M
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ContinuousSMul R M
[PROOFSTEP]
infer_instance


[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
φ : M →SL[σ] M₂
x : M
hf : HasSum f x
⊢ HasSum (fun b => ↑φ (f b)) (↑φ x)
[PROOFSTEP]
simpa only using hf.map φ.toLinearMap.toAddMonoidHom φ.continuous
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun b => ↑e (f b)) y
⊢ HasSum f (↑(ContinuousLinearEquiv.symm e) y)
[PROOFSTEP]
simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M)
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (↑(ContinuousLinearEquiv.symm e) y)
⊢ HasSum (fun b => ↑e (f b)) y
[PROOFSTEP]
simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum (fun b => ↑e (f b)) (↑e x) ↔ HasSum f x
[PROOFSTEP]
rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
exact
  ⟨fun h => (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h =>
    (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
have hf' : ¬Summable fun z => e (f z) := fun h => hf (e.summable.mp h)
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y ↔ 0 = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
refine ⟨?_, fun H => ?_⟩
[GOAL]
case neg.refine_1
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y → 0 = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.refine_1
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = ↑(ContinuousLinearEquiv.symm e) 0
[PROOFSTEP]
simp
[GOAL]
case neg.refine_2
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
H : 0 = ↑(ContinuousLinearEquiv.symm e) y
⊢ 0 = y
[PROOFSTEP]
simpa using congr_arg (fun z => e z) H
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ↑e (∑' (z : ι), f z) = ∑' (z : ι), ↑e (f z)
[PROOFSTEP]
refine' symm (e.tsum_eq_iff.mpr _)
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) (↑e (∑' (z : ι), f z))
[PROOFSTEP]
rw [e.symm_apply_apply _]