[GOAL]
p x t : ℝ
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖
[PROOFSTEP]
have aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b) := fun {a b c} h =>
  by
  simp only [mem_zmultiples_iff] at h ⊢
  obtain ⟨n, rfl⟩ := h
  exact ⟨n, (mul_smul_comm n c b).symm⟩
[GOAL]
p x t a b c : ℝ
h : a ∈ zmultiples b
⊢ c * a ∈ zmultiples (c * b)
[PROOFSTEP]
simp only [mem_zmultiples_iff] at h ⊢
[GOAL]
p x t a b c : ℝ
h : ∃ k, k • b = a
⊢ ∃ k, k • (c * b) = c * a
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
p x t b c : ℝ
n : ℤ
⊢ ∃ k, k • (c * b) = c * n • b
[PROOFSTEP]
exact ⟨n, (mul_smul_comm n c b).symm⟩
[GOAL]
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖
[PROOFSTEP]
rcases eq_or_ne t 0 with (rfl | ht)
[GOAL]
case inl
p x : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
⊢ ‖↑(0 * x)‖ = |0| * ‖↑x‖
[PROOFSTEP]
simp
[GOAL]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖
[PROOFSTEP]
have ht' : |t| ≠ 0 := (not_congr abs_eq_zero).mpr ht
[GOAL]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖
[PROOFSTEP]
simp only [quotient_norm_eq, Real.norm_eq_abs]
[GOAL]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})
[PROOFSTEP]
conv_rhs => rw [← smul_eq_mul, ← Real.sInf_smul_of_nonneg (abs_nonneg t)]
[GOAL]
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
| |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})
[PROOFSTEP]
rw [← smul_eq_mul, ← Real.sInf_smul_of_nonneg (abs_nonneg t)]
[GOAL]
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
| |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})
[PROOFSTEP]
rw [← smul_eq_mul, ← Real.sInf_smul_of_nonneg (abs_nonneg t)]
[GOAL]
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
| |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})
[PROOFSTEP]
rw [← smul_eq_mul, ← Real.sInf_smul_of_nonneg (abs_nonneg t)]
[GOAL]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = sInf (|t| • (fun a => |a|) '' {m | ↑m = ↑x})
[PROOFSTEP]
simp only [QuotientAddGroup.mk'_apply, QuotientAddGroup.eq_iff_sub_mem]
[GOAL]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ sInf ((fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)}) =
    sInf (|t| • (fun a => |a|) '' {m | m - x ∈ zmultiples p})
[PROOFSTEP]
congr 1
[GOAL]
case inr.e_a
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} = |t| • (fun a => |a|) '' {m | m - x ∈ zmultiples p}
[PROOFSTEP]
ext z
[GOAL]
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ z ∈ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} ↔ z ∈ |t| • (fun a => |a|) '' {m | m - x ∈ zmultiples p}
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ ht']
[GOAL]
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ z ∈ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} ↔ |t|⁻¹ • z ∈ (fun a => |a|) '' {m | m - x ∈ zmultiples p}
[PROOFSTEP]
show (∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ |w| = |t|⁻¹ * z
[GOAL]
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ (∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ |w| = |t|⁻¹ * z
[PROOFSTEP]
constructor
[GOAL]
case inr.e_a.h.mp
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ (∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z) → ∃ w, w - x ∈ zmultiples p ∧ |w| = |t|⁻¹ * z
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
case inr.e_a.h.mp.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ ∃ w, w - x ∈ zmultiples p ∧ |w| = |t|⁻¹ * |y|
[PROOFSTEP]
refine' ⟨t⁻¹ * y, _, by rw [abs_mul, abs_inv]⟩
[GOAL]
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ |t⁻¹ * y| = |t|⁻¹ * |y|
[PROOFSTEP]
rw [abs_mul, abs_inv]
[GOAL]
case inr.e_a.h.mp.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * y - x ∈ zmultiples p
[PROOFSTEP]
rw [← inv_mul_cancel_left₀ ht x, ← inv_mul_cancel_left₀ ht p, ← mul_sub]
[GOAL]
case inr.e_a.h.mp.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * (y - t * x) ∈ zmultiples (t⁻¹ * (t * p))
[PROOFSTEP]
exact aux hy
[GOAL]
case inr.e_a.h.mpr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ (∃ w, w - x ∈ zmultiples p ∧ |w| = |t|⁻¹ * z) → ∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z
[PROOFSTEP]
rintro ⟨w, hw, hw'⟩
[GOAL]
case inr.e_a.h.mpr.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : |w| = |t|⁻¹ * z
⊢ ∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z
[PROOFSTEP]
refine' ⟨t * w, _, by rw [← (eq_inv_mul_iff_mul_eq₀ ht').mp hw', abs_mul]⟩
[GOAL]
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : |w| = |t|⁻¹ * z
⊢ |t * w| = z
[PROOFSTEP]
rw [← (eq_inv_mul_iff_mul_eq₀ ht').mp hw', abs_mul]
[GOAL]
case inr.e_a.h.mpr.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : |w| = |t|⁻¹ * z
⊢ t * w - t * x ∈ zmultiples (t * p)
[PROOFSTEP]
rw [← mul_sub]
[GOAL]
case inr.e_a.h.mpr.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : |w| = |t|⁻¹ * z
⊢ t * (w - x) ∈ zmultiples (t * p)
[PROOFSTEP]
exact aux hw
[GOAL]
p x : ℝ
⊢ ‖↑x‖ = ‖↑x‖
[PROOFSTEP]
suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖
  by
  rw [← this, neg_one_mul]
  simp
[GOAL]
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑x‖
[PROOFSTEP]
rw [← this, neg_one_mul]
[GOAL]
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖
[PROOFSTEP]
simp
[GOAL]
p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖
[PROOFSTEP]
simp only [norm_coe_mul, abs_neg, abs_one, one_mul]
[GOAL]
p x : ℝ
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
suffices {y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ))} = { x } by
  rw [quotient_norm_eq, this, image_singleton, Real.norm_eq_abs, csInf_singleton]
[GOAL]
p x : ℝ
this : {y | ↑y = ↑x} = {x}
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
rw [quotient_norm_eq, this, image_singleton, Real.norm_eq_abs, csInf_singleton]
[GOAL]
p x : ℝ
⊢ {y | ↑y = ↑x} = {x}
[PROOFSTEP]
ext y
[GOAL]
case h
p x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}
[PROOFSTEP]
simp [QuotientAddGroup.eq_iff_sub_mem, mem_zmultiples_iff, sub_eq_zero]
[GOAL]
p x : ℝ
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
[PROOFSTEP]
suffices ∀ x : ℝ, ‖(x : AddCircle (1 : ℝ))‖ = |x - round x|
  by
  rcases eq_or_ne p 0 with (rfl | hp)
  · simp
  intros
  have hx := norm_coe_mul p x p⁻¹
  rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
  rw [← hx, inv_mul_cancel hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
[GOAL]
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
[PROOFSTEP]
rcases eq_or_ne p 0 with (rfl | hp)
[GOAL]
case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (0⁻¹ * x)) * 0|
[PROOFSTEP]
simp
[GOAL]
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
[PROOFSTEP]
intros
[GOAL]
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
[PROOFSTEP]
have hx := norm_coe_mul p x p⁻¹
[GOAL]
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p⁻¹| * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
[PROOFSTEP]
rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
[GOAL]
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
[PROOFSTEP]
rw [← hx, inv_mul_cancel hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
[GOAL]
p x : ℝ
⊢ ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
[PROOFSTEP]
clear! x p
[GOAL]
⊢ ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
[PROOFSTEP]
intros x
[GOAL]
x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|
[PROOFSTEP]
rw [quotient_norm_eq, abs_sub_round_eq_min]
[GOAL]
x : ℝ
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
[PROOFSTEP]
have h₁ : BddBelow (abs '' {m : ℝ | (m : AddCircle (1 : ℝ)) = x}) := ⟨0, by simp [mem_lowerBounds]⟩
[GOAL]
x : ℝ
⊢ 0 ∈ lowerBounds (abs '' {m | ↑m = ↑x})
[PROOFSTEP]
simp [mem_lowerBounds]
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
[PROOFSTEP]
have h₂ : (abs '' {m : ℝ | (m : AddCircle (1 : ℝ)) = x}).Nonempty := ⟨|x|, ⟨x, rfl, rfl⟩⟩
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) ≤ min (fract x) (1 - fract x)
[PROOFSTEP]
simp_rw [Real.norm_eq_abs, csInf_le_iff h₁ h₂, le_min_iff]
[GOAL]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ ∀ (b : ℝ), b ∈ lowerBounds (abs '' {m | ↑m = ↑x}) → b ≤ fract x ∧ b ≤ 1 - fract x
[PROOFSTEP]
intro b h
[GOAL]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ b ≤ fract x ∧ b ≤ 1 - fract x
[PROOFSTEP]
refine'
  ⟨mem_lowerBounds.1 h _ ⟨fract x, _, abs_fract⟩,
    mem_lowerBounds.1 h _ ⟨fract x - 1, _, by rw [abs_sub_comm, abs_one_sub_fract]⟩⟩
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ |fract x - 1| = 1 - fract x
[PROOFSTEP]
rw [abs_sub_comm, abs_one_sub_fract]
[GOAL]
case a.refine'_1
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x ∈ {m | ↑m = ↑x}
[PROOFSTEP]
simp only [mem_setOf, fract, sub_eq_self, QuotientAddGroup.mk_sub, QuotientAddGroup.eq_zero_iff,
  int_cast_mem_zmultiples_one]
[GOAL]
case a.refine'_2
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x - 1 ∈ {m | ↑m = ↑x}
[PROOFSTEP]
simp only [mem_setOf, fract, sub_eq_self, QuotientAddGroup.mk_sub, QuotientAddGroup.eq_zero_iff,
  int_cast_mem_zmultiples_one, sub_sub, (by norm_cast : (⌊x⌋ : ℝ) + 1 = (↑(⌊x⌋ + 1) : ℝ))]
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ ↑⌊x⌋ + 1 = ↑(⌊x⌋ + 1)
[PROOFSTEP]
norm_cast
[GOAL]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ min (fract x) (1 - fract x) ≤ sInf (norm '' {m | ↑m = ↑x})
[PROOFSTEP]
simp only [QuotientAddGroup.mk'_apply, Real.norm_eq_abs, le_csInf_iff h₁ h₂]
[GOAL]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ ∀ (b : ℝ), b ∈ abs '' {m | ↑m = ↑x} → min (fract x) (1 - fract x) ≤ b
[PROOFSTEP]
rintro b' ⟨b, hb, rfl⟩
[GOAL]
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
hb : b ∈ {m | ↑m = ↑x}
⊢ min (fract x) (1 - fract x) ≤ |b|
[PROOFSTEP]
simp only [mem_setOf, QuotientAddGroup.eq_iff_sub_mem, mem_zmultiples_iff, smul_one_eq_coe] at hb
[GOAL]
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
hb : ∃ k, ↑k = b - x
⊢ min (fract x) (1 - fract x) ≤ |b|
[PROOFSTEP]
obtain ⟨z, hz⟩ := hb
[GOAL]
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ min (fract x) (1 - fract x) ≤ |b|
[PROOFSTEP]
rw [(by rw [hz]; abel : x = b - z), fract_sub_int, ← abs_sub_round_eq_min]
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - ↑z
[PROOFSTEP]
rw [hz]
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - (b - x)
[PROOFSTEP]
abel
[GOAL]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - (b - x)
[PROOFSTEP]
abel
[GOAL]
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ |b - ↑(round b)| ≤ |b|
[PROOFSTEP]
convert round_le b 0
[GOAL]
case h.e'_4.h.e'_3
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ b = b - ↑0
[PROOFSTEP]
simp
[GOAL]
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
[PROOFSTEP]
conv_rhs =>
  congr
  rw [← abs_eq_self.mpr hp.le]
[GOAL]
p : ℝ
hp : 0 < p
x : ℝ
| p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
[PROOFSTEP]
  congr
  rw [← abs_eq_self.mpr hp.le]
[GOAL]
p : ℝ
hp : 0 < p
x : ℝ
| p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
[PROOFSTEP]
  congr
  rw [← abs_eq_self.mpr hp.le]
[GOAL]
p : ℝ
hp : 0 < p
x : ℝ
| p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
[PROOFSTEP]
congr
[GOAL]
case a
p : ℝ
hp : 0 < p
x : ℝ
| p
case a p : ℝ hp : 0 < p x : ℝ | |p⁻¹ * x - ↑(round (p⁻¹ * x))|
[PROOFSTEP]
rw [← abs_eq_self.mpr hp.le]
[GOAL]
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |p| * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
[PROOFSTEP]
rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]
[GOAL]
p : ℝ
x : AddCircle p
hp : p ≠ 0
⊢ ‖x‖ ≤ |p| / 2
[PROOFSTEP]
obtain ⟨x⟩ := x
[GOAL]
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖Quot.mk Setoid.r x‖ ≤ |p| / 2
[PROOFSTEP]
change ‖(x : AddCircle p)‖ ≤ |p| / 2
[GOAL]
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖↑x‖ ≤ |p| / 2
[PROOFSTEP]
rw [norm_eq, ← mul_le_mul_left (abs_pos.mpr (inv_ne_zero hp)), ← abs_mul, mul_sub, mul_left_comm, ← mul_div_assoc, ←
  abs_mul, inv_mul_cancel hp, mul_one, abs_one]
[GOAL]
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ 1 / 2
[PROOFSTEP]
exact abs_sub_round (p⁻¹ * x)
[GOAL]
p : ℝ
⊢ ‖↑(p / 2)‖ = |p| / 2
[PROOFSTEP]
rcases eq_or_ne p 0 with (rfl | hp)
[GOAL]
case inl
⊢ ‖↑(0 / 2)‖ = |0| / 2
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2
[PROOFSTEP]
rw [norm_eq, ← mul_div_assoc, inv_mul_cancel hp, one_div, round_two_inv, Int.cast_one, one_mul,
  (by linarith : p / 2 - p = -(p / 2)), abs_neg, abs_div, abs_two]
[GOAL]
p : ℝ
hp : p ≠ 0
⊢ p / 2 - p = -(p / 2)
[PROOFSTEP]
linarith
[GOAL]
p x : ℝ
hp : p ≠ 0
⊢ ‖↑x‖ = |x| ↔ |x| ≤ |p| / 2
[PROOFSTEP]
refine' ⟨fun hx => hx ▸ norm_le_half_period p hp, fun hx => _⟩
[GOAL]
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
suffices ∀ p : ℝ, 0 < p → |x| ≤ p / 2 → ‖(x : AddCircle p)‖ = |x| by
  -- Porting note: replaced `lt_trichotomy` which had trouble substituting `p = 0`.
  rcases hp.symm.lt_or_lt with (hp | hp)
  · rw [abs_eq_self.mpr hp.le] at hx
    exact this p hp hx
  · rw [← norm_neg_period]
    rw [abs_eq_neg_self.mpr hp.le] at hx
    exact this (-p) (neg_pos.mpr hp) hx
[GOAL]
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
rcases hp.symm.lt_or_lt with (hp | hp)
[GOAL]
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : 0 < p
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
rw [abs_eq_self.mpr hp.le] at hx
[GOAL]
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ p / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : 0 < p
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
exact this p hp hx
[GOAL]
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
rw [← norm_neg_period]
[GOAL]
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
rw [abs_eq_neg_self.mpr hp.le] at hx
[GOAL]
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ -p / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
exact this (-p) (neg_pos.mpr hp) hx
[GOAL]
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
⊢ ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
[PROOFSTEP]
clear hx
[GOAL]
p x : ℝ
hp : p ≠ 0
⊢ ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
[PROOFSTEP]
intro p hp hx
[GOAL]
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')
[GOAL]
case inl
p✝ : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |p / 2| ≤ p / 2
⊢ ‖↑(p / 2)‖ = |p / 2|
[PROOFSTEP]
simp [abs_div, abs_two]
[GOAL]
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
suffices round (p⁻¹ * x) = 0 by simp [norm_eq, this]
[GOAL]
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
this : round (p⁻¹ * x) = 0
⊢ ‖↑x‖ = |x|
[PROOFSTEP]
simp [norm_eq, this]
[GOAL]
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ round (p⁻¹ * x) = 0
[PROOFSTEP]
rw [round_eq_zero_iff]
[GOAL]
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
[PROOFSTEP]
obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx
[GOAL]
case inr.intro
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x ≤ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
[PROOFSTEP]
replace hx₂ := Ne.lt_of_le hx' hx₂
[GOAL]
case inr.intro
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
[PROOFSTEP]
constructor
[GOAL]
case inr.intro.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x
[PROOFSTEP]
rwa [← mul_le_mul_left hp, ← mul_assoc, mul_inv_cancel hp.ne.symm, one_mul, mul_neg, ← mul_div_assoc, mul_one]
[GOAL]
case inr.intro.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2
[PROOFSTEP]
rwa [← mul_lt_mul_left hp, ← mul_assoc, mul_inv_cancel hp.ne.symm, one_mul, ← mul_div_assoc, mul_one]
[GOAL]
p : ℝ
hp : p ≠ 0
x✝ : AddCircle p
ε : ℝ
hε : |p| / 2 ≤ ε
x : AddCircle p
⊢ x ∈ closedBall x✝ ε
[PROOFSTEP]
simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε
[GOAL]
p x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = closedBall x ε
[PROOFSTEP]
ext y
[GOAL]
case h
p x ε y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε
[PROOFSTEP]
simp only [Set.mem_preimage, dist_eq_norm, AddCircle.norm_eq_of_zero, iff_self, ← QuotientAddGroup.mk_sub,
  Metric.mem_closedBall, Real.norm_eq_abs]
[GOAL]
p x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • p) ε
[PROOFSTEP]
rcases eq_or_ne p 0 with (rfl | hp)
[GOAL]
case inl
x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • 0) ε
[PROOFSTEP]
simp [iUnion_const]
[GOAL]
case inr
p x ε : ℝ
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • p) ε
[PROOFSTEP]
ext y
[GOAL]
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ (z : ℤ), closedBall (x + z • p) ε
[PROOFSTEP]
simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs, ←
  QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]
[GOAL]
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε ↔ ∃ i, |y - x - ↑i * p| ≤ ε
[PROOFSTEP]
refine' ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, _⟩
[GOAL]
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ (∃ i, |y - x - ↑i * p| ≤ ε) → |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |y - x - ↑n * p| ≤ ε
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε
[PROOFSTEP]
rw [← mul_le_mul_left (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p, inv_mul_cancel_left₀ hp] at hn
  ⊢
[GOAL]
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - ↑n| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - ↑(round (p⁻¹ * (y - x)))| ≤ |p⁻¹| * ε
[PROOFSTEP]
exact (round_le (p⁻¹ * (y - x)) n).trans hn
[GOAL]
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
cases' le_or_lt (|p| / 2) ε with hε hε
[GOAL]
case inl
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
rcases eq_or_ne p 0 with (rfl | hp)
[GOAL]
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : |0| / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |0| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
simp only [abs_zero, zero_div] at hε
[GOAL]
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |0| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div, if_false,
  inter_eq_right_iff_subset]
[GOAL]
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ s ⊆ closedBall x ε
[PROOFSTEP]
exact
  hs.trans
    (closedBall_subset_closedBall <| by simp [hε])
      -- Porting note: was
          -- simp [closedBall_eq_univ_of_half_period_le p hp (↑x) hε, not_lt.mpr hε]
[GOAL]
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ |0| / 2 ≤ ε
[PROOFSTEP]
simp [hε]
[GOAL]
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
simp only [not_lt.mpr hε, ite_false, inter_eq_right_iff_subset]
[GOAL]
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
hp : p ≠ 0
⊢ s ⊆ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε
[PROOFSTEP]
rw [closedBall_eq_univ_of_half_period_le p hp (↑x : ℝ ⧸ zmultiples p) hε, preimage_univ]
[GOAL]
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
hp : p ≠ 0
⊢ s ⊆ univ
[PROOFSTEP]
apply subset_univ
[GOAL]
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
suffices ∀ z : ℤ, closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅ by
  simp [-zsmul_eq_mul, ← QuotientAddGroup.mk_zero, coe_real_preimage_closedBall_eq_iUnion, iUnion_inter, iUnion_ite,
    this, hε]
[GOAL]
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
this : ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
[PROOFSTEP]
simp [-zsmul_eq_mul, ← QuotientAddGroup.mk_zero, coe_real_preimage_closedBall_eq_iUnion, iUnion_inter, iUnion_ite, this,
  hε]
[GOAL]
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
⊢ ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
[PROOFSTEP]
intro z
[GOAL]
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
[PROOFSTEP]
simp only [Real.closedBall_eq_Icc, zero_sub, zero_add] at hs ⊢
[GOAL]
case inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz)
[GOAL]
case inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + 0 • p - ε) (x + 0 • p + ε) ∩ s = if 0 = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
[PROOFSTEP]
simp
[GOAL]
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
[PROOFSTEP]
simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_not_mem]
[GOAL]
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
⊢ ∀ (x_1 : ℝ), ¬x_1 ∈ Icc (x + ↑z * p - ε) (x + ↑z * p + ε) ∩ s
[PROOFSTEP]
rintro y ⟨⟨hy₁, hy₂⟩, hy₀⟩
[GOAL]
case inr.inr.intro.intro
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
⊢ False
[PROOFSTEP]
obtain ⟨hy₃, hy₄⟩ := hs hy₀
[GOAL]
case inr.inr.intro.intro.intro
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
⊢ False
[PROOFSTEP]
rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)
[GOAL]
case inr.inr.intro.intro.intro.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
⊢ False
[PROOFSTEP]
cases' Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' hz'
[GOAL]
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ False
[PROOFSTEP]
have : ↑z * p ≤ -p
[GOAL]
case this
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ ↑z * p ≤ -p
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
this : ↑z * p ≤ -p
⊢ False
[PROOFSTEP]
nlinarith
[GOAL]
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
this : ↑z * p ≤ -p
⊢ False
[PROOFSTEP]
linarith [abs_eq_self.mpr hp.le]
[GOAL]
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False
[PROOFSTEP]
have : p ≤ ↑z * p
[GOAL]
case this
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ p ≤ ↑z * p
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
[PROOFSTEP]
nlinarith
[GOAL]
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
[PROOFSTEP]
linarith [abs_eq_self.mpr hp.le]
[GOAL]
case inr.inr.intro.intro.intro.inr.inl
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hε : ε < |0| / 2
hs : s ⊆ Icc (x - |0| / 2) (x + |0| / 2)
hy₁ : x + ↑z * 0 - ε ≤ y
hy₂ : y ≤ x + ↑z * 0 + ε
hy₃ : x - |0| / 2 ≤ y
hy₄ : y ≤ x + |0| / 2
⊢ False
[PROOFSTEP]
simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
[GOAL]
case inr.inr.intro.intro.intro.inr.inl
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hs : s ⊆ Icc (x - |0| / 2) (x + |0| / 2)
hy₃ : x - |0| / 2 ≤ y
hy₄ : y ≤ x + |0| / 2
hy₁ : x - ε ≤ y
hy₂ : y ≤ x + ε
hε : ε < 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case inr.inr.intro.intro.intro.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
⊢ False
[PROOFSTEP]
cases' Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' hz'
[GOAL]
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ False
[PROOFSTEP]
have : -p ≤ ↑z * p
[GOAL]
case this
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ -p ≤ ↑z * p
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
[PROOFSTEP]
nlinarith
[GOAL]
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
[PROOFSTEP]
linarith [abs_eq_neg_self.mpr hp.le]
[GOAL]
case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ False
[PROOFSTEP]
have : ↑z * p ≤ p
[GOAL]
case this
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ ↑z * p ≤ p
case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
[PROOFSTEP]
nlinarith
[GOAL]
case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
[PROOFSTEP]
linarith [abs_eq_neg_self.mpr hp.le]
[GOAL]
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
[PROOFSTEP]
have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
[GOAL]
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
[PROOFSTEP]
rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
[GOAL]
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
[PROOFSTEP]
rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
[PROOFSTEP]
let n := addOrderOf u
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
[PROOFSTEP]
change ∃ k : ℕ, ‖u‖ = p * (k / n)
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
[PROOFSTEP]
obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu
[GOAL]
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
[PROOFSTEP]
refine' ⟨min (m % n) (n - m % n), _⟩
[GOAL]
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
[PROOFSTEP]
rw [← hm, norm_div_nat_cast]
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu
[GOAL]
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ p ≤ addOrderOf u • ‖u‖
[PROOFSTEP]
replace hu : (addOrderOf u : ℝ) ≠ 0
[GOAL]
case hu
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ ↑(addOrderOf u) ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case hu
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ ¬addOrderOf u = 0
[PROOFSTEP]
exact (addOrderOf_pos_iff.mpr hu).ne'
[GOAL]
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖
[PROOFSTEP]
conv_lhs => rw [← mul_one p]
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
| p
[PROOFSTEP]
rw [← mul_one p]
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
| p
[PROOFSTEP]
rw [← mul_one p]
[GOAL]
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
| p
[PROOFSTEP]
rw [← mul_one p]
[GOAL]
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ addOrderOf u • ‖u‖
[PROOFSTEP]
rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel' _ hu, mul_le_mul_left hp.out,
  Nat.one_le_cast, Nat.one_le_iff_ne_zero]
[GOAL]
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
contrapose! hu'
[GOAL]
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
hu' : n = 0
⊢ u = 0
[PROOFSTEP]
simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn
[GOAL]
x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|
[PROOFSTEP]
simp [AddCircle.norm_eq]


[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
h : ∃ V x, IsVonNBounded 𝕜 (↑f '' V)
⊢ Continuous f.toFun
[PROOFSTEP]
refine' continuous_of_continuousAt_zero f _
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
h : ∃ V x, IsVonNBounded 𝕜 (↑f '' V)
⊢ ContinuousAt (↑f) 0
[PROOFSTEP]
rw [continuousAt_def, f.map_zero]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
h : ∃ V x, IsVonNBounded 𝕜 (↑f '' V)
⊢ ∀ (A : Set F), A ∈ 𝓝 0 → ↑f ⁻¹' A ∈ 𝓝 0
[PROOFSTEP]
intro U hU
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
h : ∃ V x, IsVonNBounded 𝕜 (↑f '' V)
U : Set F
hU : U ∈ 𝓝 0
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
rcases h with ⟨V, hV, h⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h : IsVonNBounded 𝕜 (↑f '' V)
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
rcases h hU with ⟨r, hr, h⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑f '' V ⊆ a • U
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
rcases NormedField.exists_lt_norm 𝕜 r with ⟨x, hx⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑f '' V ⊆ a • U
x : 𝕜
hx : r < ‖x‖
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
specialize h x hx.le
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
have x_ne := norm_pos_iff.mp (hr.trans hx)
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
have : x⁻¹ • V ⊆ f ⁻¹' U :=
  calc
    x⁻¹ • V ⊆ x⁻¹ • f ⁻¹' (f '' V) := Set.smul_set_mono (Set.subset_preimage_image (⇑f) V)
    _ ⊆ x⁻¹ • f ⁻¹' (x • U) := (Set.smul_set_mono (Set.preimage_mono h))
    _ = f ⁻¹' (x⁻¹ • x • U) := by
      ext
      simp only [Set.mem_inv_smul_set_iff₀ x_ne, Set.mem_preimage, LinearMap.map_smul]
    _ ⊆ f ⁻¹' U := by
      rw [inv_smul_smul₀ x_ne _]
        -- Using this inclusion, it suffices to show that `x⁻¹ • V` is in `𝓝 0`, which is trivial.
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
⊢ x⁻¹ • ↑f ⁻¹' (x • U) = ↑f ⁻¹' (x⁻¹ • x • U)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
x✝ : E
⊢ x✝ ∈ x⁻¹ • ↑f ⁻¹' (x • U) ↔ x✝ ∈ ↑f ⁻¹' (x⁻¹ • x • U)
[PROOFSTEP]
simp only [Set.mem_inv_smul_set_iff₀ x_ne, Set.mem_preimage, LinearMap.map_smul]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
⊢ ↑f ⁻¹' (x⁻¹ • x • U) ⊆ ↑f ⁻¹' U
[PROOFSTEP]
rw [inv_smul_smul₀ x_ne _]
  -- Using this inclusion, it suffices to show that `x⁻¹ • V` is in `𝓝 0`, which is trivial.
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ ↑f ⁻¹' U
⊢ ↑f ⁻¹' U ∈ 𝓝 0
[PROOFSTEP]
refine' mem_of_superset _ this
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ ↑f ⁻¹' U
⊢ x⁻¹ • V ∈ 𝓝 0
[PROOFSTEP]
convert set_smul_mem_nhds_smul hV (inv_ne_zero x_ne)
[GOAL]
case h.e'_5.h.e'_3
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : UniformSpace E
inst✝⁷ : UniformAddGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
f : E →ₗ[𝕜] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜 (↑f '' V)
r : ℝ
hr : 0 < r
x : 𝕜
hx : r < ‖x‖
h : ↑f '' V ⊆ x • U
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ ↑f ⁻¹' U
⊢ 0 = x⁻¹ • 0
[PROOFSTEP]
exact (smul_zero _).symm
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
⊢ ContinuousAt (↑f) 0
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
⊢ False
[PROOFSTEP]
rcases(nhds_basis_balanced 𝕜 E).exists_antitone_subbasis with ⟨b, bE1, bE⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => _root_.id (b i)
⊢ False
[PROOFSTEP]
simp only [id.def] at bE
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ False
[PROOFSTEP]
have bE' : (𝓝 (0 : E)).HasBasis (fun x : ℕ => x ≠ 0) fun n : ℕ => (n : 𝕜)⁻¹ • b n :=
  by
  refine' bE.1.to_hasBasis _ _
  · intro n _
    use n + 1
    simp only [Ne.def, Nat.succ_ne_zero, not_false_iff, Nat.cast_add, Nat.cast_one, true_and_iff]
      -- `b (n + 1) ⊆ b n` follows from `Antitone`.
    have h : b (n + 1) ⊆ b n := bE.2 (by simp)
    refine' _root_.trans _ h
    rintro y
      ⟨x, hx, hy⟩
          -- Since `b (n + 1)` is balanced `(n+1)⁻¹ b (n + 1) ⊆ b (n + 1)`
    rw [← hy]
    refine' (bE1 (n + 1)).2.smul_mem _ hx
    have h' : 0 < (n : ℝ) + 1 := n.cast_add_one_pos
    rw [norm_inv, ← Nat.cast_one, ← Nat.cast_add, IsROrC.norm_natCast, Nat.cast_add, Nat.cast_one,
      inv_le h' zero_lt_one]
    simp
  intro n hn
  have hcont : ContinuousAt (fun x : E => (n : 𝕜) • x) 0 := (continuous_const_smul (n : 𝕜)).continuousAt
  simp only [ContinuousAt, map_zero, smul_zero] at hcont
  rw [bE.1.tendsto_left_iff] at hcont
  rcases hcont (b n) (bE1 n).1 with ⟨i, _, hi⟩
  refine' ⟨i, trivial, fun x hx => ⟨(n : 𝕜) • x, hi hx, _⟩⟩
  simp [← mul_smul, hn]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
[PROOFSTEP]
refine' bE.1.to_hasBasis _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ ∀ (i : ℕ), True → ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b i
[PROOFSTEP]
intro n _
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b n
[PROOFSTEP]
use n + 1
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ n + 1 ≠ 0 ∧ (↑(n + 1))⁻¹ • b (n + 1) ⊆ b n
[PROOFSTEP]
simp only [Ne.def, Nat.succ_ne_zero, not_false_iff, Nat.cast_add, Nat.cast_one, true_and_iff]
  -- `b (n + 1) ⊆ b n` follows from `Antitone`.
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b n
[PROOFSTEP]
have h : b (n + 1) ⊆ b n := bE.2 (by simp)
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ n ≤ n + 1
[PROOFSTEP]
simp
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b n
[PROOFSTEP]
refine' _root_.trans _ h
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b (n + 1)
[PROOFSTEP]
rintro y
  ⟨x, hx, hy⟩
      -- Since `b (n + 1)` is balanced `(n+1)⁻¹ b (n + 1) ⊆ b (n + 1)`
[GOAL]
case h.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ y ∈ b (n + 1)
[PROOFSTEP]
rw [← hy]
[GOAL]
case h.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ (fun x => (↑n + 1)⁻¹ • x) x ∈ b (n + 1)
[PROOFSTEP]
refine' (bE1 (n + 1)).2.smul_mem _ hx
[GOAL]
case h.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ ‖(↑n + 1)⁻¹‖ ≤ 1
[PROOFSTEP]
have h' : 0 < (n : ℝ) + 1 := n.cast_add_one_pos
[GOAL]
case h.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
h' : 0 < ↑n + 1
⊢ ‖(↑n + 1)⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv, ← Nat.cast_one, ← Nat.cast_add, IsROrC.norm_natCast, Nat.cast_add, Nat.cast_one, inv_le h' zero_lt_one]
[GOAL]
case h.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
h' : 0 < ↑n + 1
⊢ 1⁻¹ ≤ ↑n + 1
[PROOFSTEP]
simp
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ ∀ (i' : ℕ), i' ≠ 0 → ∃ i, True ∧ b i ⊆ (↑i')⁻¹ • b i'
[PROOFSTEP]
intro n hn
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
[PROOFSTEP]
have hcont : ContinuousAt (fun x : E => (n : 𝕜) • x) 0 := (continuous_const_smul (n : 𝕜)).continuousAt
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ContinuousAt (fun x => ↑n • x) 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
[PROOFSTEP]
simp only [ContinuousAt, map_zero, smul_zero] at hcont
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : Tendsto (fun x => ↑n • x) (𝓝 0) (𝓝 0)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
[PROOFSTEP]
rw [bE.1.tendsto_left_iff] at hcont
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
[PROOFSTEP]
rcases hcont (b n) (bE1 n).1 with ⟨i, _, hi⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
[PROOFSTEP]
refine' ⟨i, trivial, fun x hx => ⟨(n : 𝕜) • x, hi hx, _⟩⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
x : E
hx : x ∈ b i
⊢ (fun x => (↑n)⁻¹ • x) (↑n • x) = x
[PROOFSTEP]
simp [← mul_smul, hn]
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
⊢ False
[PROOFSTEP]
rw [ContinuousAt, map_zero, bE'.tendsto_iff (nhds_basis_balanced 𝕜' F)] at h
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
h : ¬∀ (ib : Set F), ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib → ∃ ia, ia ≠ 0 ∧ ∀ (x : E), x ∈ (↑ia)⁻¹ • b ia → ↑f x ∈ _root_.id ib
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
⊢ False
[PROOFSTEP]
push_neg at h
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
h : ∃ ib, (ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib) ∧ ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ _root_.id ib
⊢ False
[PROOFSTEP]
rcases h with ⟨V, ⟨hV, -⟩, h⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ _root_.id V
hV : V ∈ 𝓝 0
⊢ False
[PROOFSTEP]
simp only [id.def, forall_true_left] at h
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ V
hV : V ∈ 𝓝 0
⊢ False
[PROOFSTEP]
choose! u hu hu' using h
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ False
[PROOFSTEP]
have h_tendsto : Tendsto (fun n : ℕ => (n : 𝕜) • u n) atTop (𝓝 (0 : E)) :=
  by
  apply bE.tendsto
  intro n
  by_cases h : n = 0
  · rw [h, Nat.cast_zero, zero_smul]
    refine' mem_of_mem_nhds (bE.1.mem_of_mem <| by triv)
  rcases hu n h with ⟨y, hy, hu1⟩
  convert hy
  rw [← hu1, ← mul_smul]
  simp only [h, mul_inv_cancel, Ne.def, Nat.cast_eq_zero, not_false_iff, one_smul]
    -- The image `(fun n ↦ n • u n)` is von Neumann bounded:
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
[PROOFSTEP]
apply bE.tendsto
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ ∀ (i : ℕ), ↑i • u i ∈ b i
[PROOFSTEP]
intro n
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
⊢ ↑n • u n ∈ b n
[PROOFSTEP]
by_cases h : n = 0
[GOAL]
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ ↑n • u n ∈ b n
[PROOFSTEP]
rw [h, Nat.cast_zero, zero_smul]
[GOAL]
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ 0 ∈ b 0
[PROOFSTEP]
refine' mem_of_mem_nhds (bE.1.mem_of_mem <| by triv)
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ True
[PROOFSTEP]
triv
[GOAL]
case neg
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
⊢ ↑n • u n ∈ b n
[PROOFSTEP]
rcases hu n h with ⟨y, hy, hu1⟩
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ ↑n • u n ∈ b n
[PROOFSTEP]
convert hy
[GOAL]
case h.e'_4
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ ↑n • u n = y
[PROOFSTEP]
rw [← hu1, ← mul_smul]
[GOAL]
case h.e'_4
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ (↑n * (↑n)⁻¹) • y = y
[PROOFSTEP]
simp only [h, mul_inv_cancel, Ne.def, Nat.cast_eq_zero, not_false_iff, one_smul]
  -- The image `(fun n ↦ n • u n)` is von Neumann bounded:
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
⊢ False
[PROOFSTEP]
have h_bounded : IsVonNBounded 𝕜 (Set.range fun n : ℕ => (n : 𝕜) • u n) :=
  h_tendsto.cauchySeq.totallyBounded_range.isVonNBounded 𝕜
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
⊢ False
[PROOFSTEP]
rcases hf _ h_bounded hV with ⟨r, hr, h'⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
⊢ False
[PROOFSTEP]
cases' exists_nat_gt r with n hn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ False
[PROOFSTEP]
have h1 : r ≤ ‖(n : 𝕜')‖ := by
  rw [IsROrC.norm_natCast]
  exact hn.le
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ‖↑n‖
[PROOFSTEP]
rw [IsROrC.norm_natCast]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ↑n
[PROOFSTEP]
exact hn.le
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
⊢ False
[PROOFSTEP]
have hn' : 0 < ‖(n : 𝕜')‖ := lt_of_lt_of_le hr h1
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : 0 < ‖↑n‖
⊢ False
[PROOFSTEP]
rw [norm_pos_iff, Ne.def, Nat.cast_eq_zero] at hn'
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
⊢ False
[PROOFSTEP]
have h'' : f (u n) ∈ V := by
  simp only [Set.image_subset_iff] at h'
  specialize h' (n : 𝕜') h1 (Set.mem_range_self n)
  simp only [Set.mem_preimage, LinearMap.map_smulₛₗ, map_natCast] at h'
  rcases h' with ⟨y, hy, h'⟩
  apply_fun fun y : F => (n : 𝕜')⁻¹ • y at h'
  simp only [hn', inv_smul_smul₀, Ne.def, Nat.cast_eq_zero, not_false_iff] at h'
  rwa [← h']
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
simp only [Set.image_subset_iff] at h'
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (Set.range fun n => ↑n • u n) ⊆ (fun a => ↑f a) ⁻¹' (a • V)
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
specialize h' (n : 𝕜') h1 (Set.mem_range_self n)
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • u n ∈ (fun a => ↑f a) ⁻¹' (↑n • V)
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
simp only [Set.mem_preimage, LinearMap.map_smulₛₗ, map_natCast] at h'
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • ↑f (u n) ∈ ↑n • V
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
rcases h' with ⟨y, hy, h'⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : (fun x => ↑n • x) y = ↑n • ↑f (u n)
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
apply_fun fun y : F => (n : 𝕜')⁻¹ • y at h'
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : (↑n)⁻¹ • (fun x => ↑n • x) y = (↑n)⁻¹ • ↑n • ↑f (u n)
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
simp only [hn', inv_smul_smul₀, Ne.def, Nat.cast_eq_zero, not_false_iff] at h'
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : y = ↑f (u n)
⊢ ↑f (u n) ∈ V
[PROOFSTEP]
rwa [← h']
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h'' : ↑f (u n) ∈ V
⊢ False
[PROOFSTEP]
exact hu' n hn' h''