p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
p x t : ℝ
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
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⟩
case inl
p x : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
⊢ ‖↑(0 * x)‖ = abs 0 * ‖↑x‖

case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
rcases eq_or_ne t 0 with (rfl | ht)
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
have ht' : |t| ≠ 0 := (not_congr abs_eq_zero).mpr ht
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ sInf ((fun a => abs a) '' {m | ↑m = ↑(t * x)}) = abs t * sInf ((fun a => abs a) '' {m | ↑m = ↑x})
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ ‖↑(t * x)‖ = abs t * ‖↑x‖
simp only [quotient_norm_eq, Real.norm_eq_abs]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ sInf ((fun a => abs a) '' {m | ↑m = ↑(t * x)}) = sInf (abs t • (fun a => abs a) '' {m | ↑m = ↑x})
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ sInf ((fun a => abs a) '' {m | ↑m = ↑(t * x)}) = abs t * sInf ((fun a => abs a) '' {m | ↑m = ↑x})
conv_rhs => rw [← smul_eq_mul, ← Real.sInf_smul_of_nonneg (abs_nonneg t)]
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ sInf ((fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)}) =
    sInf (abs t • (fun a => abs a) '' {m | m - x ∈ zmultiples p})
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ sInf ((fun a => abs a) '' {m | ↑m = ↑(t * x)}) = sInf (abs t • (fun a => abs a) '' {m | ↑m = ↑x})
simp only [QuotientAddGroup.mk'_apply, QuotientAddGroup.eq_iff_sub_mem]
case inr.e_a
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ (fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)} = abs t • (fun a => abs a) '' {m | m - x ∈ zmultiples p}
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ sInf ((fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)}) =
    sInf (abs t • (fun a => abs a) '' {m | m - x ∈ zmultiples p})
congr 1
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z : ℝ
⊢ z ∈ (fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)} ↔
    z ∈ abs t • (fun a => abs a) '' {m | m - x ∈ zmultiples p}
case inr.e_a
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
⊢ (fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)} = abs t • (fun a => abs a) '' {m | m - x ∈ zmultiples p}
ext z
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z : ℝ
⊢ z ∈ (fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)} ↔
    (abs t)⁻¹ • z ∈ (fun a => abs a) '' {m | m - x ∈ zmultiples p}
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z : ℝ
⊢ z ∈ (fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)} ↔
    z ∈ abs t • (fun a => abs a) '' {m | m - x ∈ zmultiples p}
rw [mem_smul_set_iff_inv_smul_mem₀ ht']
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z : ℝ
⊢ (∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * z
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z : ℝ
⊢ z ∈ (fun a => abs a) '' {m | m - t * x ∈ zmultiples (t * p)} ↔
    (abs t)⁻¹ • z ∈ (fun a => abs a) '' {m | m - x ∈ zmultiples p}
show
  (∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ |w| = (|t|)⁻¹ * z
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' : abs t ≠ 0
z : ℝ
⊢ (∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z) → ∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * z

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' : abs t ≠ 0
z : ℝ
⊢ (∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * z) → ∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z : ℝ
⊢ (∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * z
constructor
p x t a b c : ℝ
h : ∃ k, k • b = a
⊢ ∃ k, k • (c * b) = c * a
p x t a b c : ℝ
h : a ∈ zmultiples b
⊢ c * a ∈ zmultiples (c * b)
simp only [mem_zmultiples_iff] at h⊢
case intro
p x t b c : ℝ
n : ℤ
⊢ ∃ k, k • (c * b) = c * n • b
p x t a b c : ℝ
h : ∃ k, k • b = a
⊢ ∃ k, k • (c * b) = c * a
obtain ⟨n, rfl⟩ := h
no goals
case intro
p x t b c : ℝ
n : ℤ
⊢ ∃ k, k • (c * b) = c * n • b
exact ⟨n, (mul_smul_comm n c b).symm⟩
no goals
case inl
p x : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
⊢ ‖↑(0 * x)‖ = abs 0 * ‖↑x‖
simp
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' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ ∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * abs y
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' : abs t ≠ 0
z : ℝ
⊢ (∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z) → ∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * z
rintro ⟨y, hy, rfl⟩
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' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * y - x ∈ zmultiples p
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' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ ∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * abs y
refine' ⟨t⁻¹ * y, _, by rw [abs_mul, abs_inv]⟩
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' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * (y - t * x) ∈ zmultiples (t⁻¹ * (t * p))
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' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * y - x ∈ zmultiples p
rw [← inv_mul_cancel_left₀ ht x, ← inv_mul_cancel_left₀ ht p, ← mul_sub]
no goals
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' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * (y - t * x) ∈ zmultiples (t⁻¹ * (t * p))
exact aux hy
no goals
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ abs (t⁻¹ * y) = (abs t)⁻¹ * abs y
rw [abs_mul, abs_inv]
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' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ ∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z
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' : abs t ≠ 0
z : ℝ
⊢ (∃ w, w - x ∈ zmultiples p ∧ abs w = (abs t)⁻¹ * z) → ∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z
rintro ⟨w, hw, hw'⟩
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' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ t * w - t * x ∈ zmultiples (t * p)
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' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ ∃ y, y - t * x ∈ zmultiples (t * p) ∧ abs y = z
refine' ⟨t * w, _, by rw [← (eq_inv_mul_iff_mul_eq₀ ht').mp hw', abs_mul]⟩
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' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ t * (w - x) ∈ zmultiples (t * p)
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' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ t * w - t * x ∈ zmultiples (t * p)
rw [← mul_sub]
no goals
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' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ t * (w - x) ∈ zmultiples (t * p)
exact aux hw
no goals
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : abs t ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : abs w = (abs t)⁻¹ * z
⊢ abs (t * w) = z
rw [← (eq_inv_mul_iff_mul_eq₀ ht').mp hw', abs_mul]