Theorem: localOscillation_of_integer_linear (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
x R : ℝ
R_nonneg : 0 ≤ R
⊢ ∀ (n m : ℤ), localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
intro n m
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
by_cases n_ne_m : n = m
State after:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
. rw [n_ne_m]
  simp
  apply localOscillation_of_same
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
push_neg at n_ne_m
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
have norm_n_sub_m_pos : 0 < |(n : ℝ) - m| := by
  simp
  rwa [sub_eq_zero, Int.cast_inj]
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
have norm_integer_linear_eq {n m : ℤ} {z : ℝ × ℝ} : ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
  rw [←Complex.norm_real, integer_linear, integer_linear]
  congr 1
  simp
  ring
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
have localOscillation_eq : localOscillation (Metric.ball x R) (θ n) (θ m) = ⨆ z ∈ (Metric.ball x R) ×ˢ (Metric.ball x R), ‖(n - m) * (z.1 - x) - (n - m) * (z.2 - x)‖ := by
    rw [localOscillation]
    congr
    ext z
    rw [norm_integer_linear_eq]
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
rw [localOscillation_eq]
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ = 2 * R * |↑n - ↑m|

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ = 2 * R * |↑n - ↑m|
Tactic:
apply le_antisymm
State after:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
. calc ⨆ z ∈ (Metric.ball x R) ×ˢ (Metric.ball x R), ‖(n - m) * (z.1 - x) - (n - m) * (z.2 - x)‖
    _ ≤ 2 * R * |↑n - ↑m| := by
      apply Real.iSup_le
      intro z
      apply Real.iSup_le
      . intro hz
        simp at hz
        rw [Real.dist_eq, Real.dist_eq] at hz
        rw [Real.norm_eq_abs]
        calc |(n - m) * (z.1 - x) - (n - m) * (z.2 - x)|
        _ ≤ |(n - m) * (z.1 - x)| + |(n - m) * (z.2 - x)| := by apply abs_sub
        _ = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| := by congr <;> apply abs_mul
        _ ≤ |↑n - ↑m| * R + |↑n - ↑m| * R := by gcongr; linarith [hz.1]; linarith [hz.2]
        _ = 2 * R * |↑n - ↑m| := by ring
      repeat
        apply mul_nonneg
        linarith
        apply abs_nonneg
State after:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
. apply le_of_forall_lt
  intro c hc
  have := fact_isCompact_ball x R
  by_cases c_nonneg : 0 > c
  . calc c
      _ < 0 := c_nonneg
      _ ≤ @dist (withLocalOscillation (Metric.ball x R)) PseudoMetricSpace.toDist (θ n) (θ m) := dist_nonneg
      _ = localOscillation (Metric.ball x R) (θ n) (θ m) := rfl
      _ = ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
        rw [localOscillation]
        congr
        ext z
        congr
        rw [norm_integer_linear_eq]
  push_neg at c_nonneg
  set R' := (c + 2 * R * |(n : ℝ) - m|) / (4 * |(n : ℝ) - m|) with R'def
  have hR' : 0 ≤ R' ∧ R' < R := by
    rw [R'def]
    constructor
    . positivity
    calc (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
      _ < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) := by
        gcongr
      _ = R := by
        ring_nf
        rw [mul_assoc, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_one]
  let y := (x - R', x + R')
  calc c
    _ = c / 2 + c / 2 := by ring
    _ < c / 2 + (2 * R * |↑n - ↑m|) / 2 := by
      gcongr
    _ = 2 * R' * |↑n - ↑m| := by
      rw [R'def]
      ring_nf
      rw [pow_two, ←mul_assoc, mul_assoc c, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_assoc (R * _), mul_inv_cancel norm_n_sub_m_pos.ne.symm]
      ring
    _ ≤ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ := by
      simp
      rw [sub_eq_add_neg (-((n - m) * R')), ←neg_add, abs_neg, ←two_mul, abs_mul, abs_mul, mul_comm |(n : ℝ) - m|, mul_assoc]
      simp
      gcongr
      apply le_abs_self
    _ ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
      apply ConditionallyCompleteLattice.le_biSup
      . convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
        apply norm_integer_linear_eq.symm
      . use y
        simp
        rw [abs_of_nonneg]
        exact hR'.2
        exact hR'.1
State after:
no goals

State before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
rw [n_ne_m]
State after:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ m) (θ m) = 2 * R * |↑m - ↑m|

State before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ m) (θ m) = 2 * R * |↑m - ↑m|
Tactic:
simp
State after:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ m) (θ m) = 0

State before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ m) (θ m) = 0
Tactic:
apply localOscillation_of_same
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ 0 < |↑n - ↑m|
Tactic:
simp
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ ¬↑n - ↑m = 0

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ ¬↑n - ↑m = 0
Tactic:
rwa [sub_eq_zero, Int.cast_inj]
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
rw [←Complex.norm_real, integer_linear, integer_linear]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ ‖{ toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.1 - { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.1 -
          { toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.2 +
        { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.2‖ =
    ‖↑((↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x))‖

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ ‖{ toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.1 - { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.1 -
          { toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.2 +
        { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.2‖ =
    ‖↑((↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x))‖
Tactic:
congr 1
State after:
case e_a
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ { toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.1 - { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.1 -
        { toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.2 +
      { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.2 =
    ↑((↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x))

State before:
case e_a
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ { toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.1 - { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.1 -
        { toFun := fun x => ↑n * ↑x, continuous_toFun := ⋯ } z.2 +
      { toFun := fun x => ↑m * ↑x, continuous_toFun := ⋯ } z.2 =
    ↑((↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x))
Tactic:
simp
State after:
case e_a
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ ↑n * ↑z.1 - ↑m * ↑z.1 - ↑n * ↑z.2 + ↑m * ↑z.2 = (↑n - ↑m) * (↑z.1 - ↑x) - (↑n - ↑m) * (↑z.2 - ↑x)

State before:
case e_a
x R : ℝ
R_nonneg : 0 ≤ R
n✝ m✝ : ℤ
n_ne_m : n✝ ≠ m✝
norm_n_sub_m_pos : 0 < |↑n✝ - ↑m✝|
n m : ℤ
z : ℝ × ℝ
⊢ ↑n * ↑z.1 - ↑m * ↑z.1 - ↑n * ↑z.2 + ↑m * ↑z.2 = (↑n - ↑m) * (↑z.1 - ↑x) - (↑n - ↑m) * (↑z.2 - ↑x)
Tactic:
ring
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
rw [localOscillation]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
congr
State after:
case e_s
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ (fun z => ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun z =>
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case e_s
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ (fun z => ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun z =>
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
ext z
State after:
case e_s.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case e_s.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
rw [norm_integer_linear_eq]
State after:
no goals

State before:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
calc ⨆ z ∈ (Metric.ball x R) ×ˢ (Metric.ball x R), ‖(n - m) * (z.1 - x) - (n - m) * (z.2 - x)‖
  _ ≤ 2 * R * |↑n - ↑m| := by
    apply Real.iSup_le
    intro z
    apply Real.iSup_le
    . intro hz
      simp at hz
      rw [Real.dist_eq, Real.dist_eq] at hz
      rw [Real.norm_eq_abs]
      calc |(n - m) * (z.1 - x) - (n - m) * (z.2 - x)|
      _ ≤ |(n - m) * (z.1 - x)| + |(n - m) * (z.2 - x)| := by apply abs_sub
      _ = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| := by congr <;> apply abs_mul
      _ ≤ |↑n - ↑m| * R + |↑n - ↑m| * R := by gcongr; linarith [hz.1]; linarith [hz.2]
      _ = 2 * R * |↑n - ↑m| := by ring
    repeat
      apply mul_nonneg
      linarith
      apply abs_nonneg
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
apply Real.iSup_le
State after:
case hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ∀ (i : ℝ × ℝ),
    ⨆ (_ : i ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|

State before:
case hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ∀ (i : ℝ × ℝ),
    ⨆ (_ : i ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|
Tactic:
intro z
State after:
case hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|

State before:
case hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|
Tactic:
apply Real.iSup_le
State after:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ z ∈ Metric.ball x R ×ˢ Metric.ball x R → ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case hS.ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ 0 ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|

State before:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ z ∈ Metric.ball x R ×ˢ Metric.ball x R → ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case hS.ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ 0 ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|
Tactic:
. intro hz
  simp at hz
  rw [Real.dist_eq, Real.dist_eq] at hz
  rw [Real.norm_eq_abs]
  calc |(n - m) * (z.1 - x) - (n - m) * (z.2 - x)|
  _ ≤ |(n - m) * (z.1 - x)| + |(n - m) * (z.2 - x)| := by apply abs_sub
  _ = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| := by congr <;> apply abs_mul
  _ ≤ |↑n - ↑m| * R + |↑n - ↑m| * R := by gcongr; linarith [hz.1]; linarith [hz.2]
  _ = 2 * R * |↑n - ↑m| := by ring
State after:
case hS.ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ 0 ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|

State before:
case hS.ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ 0 ≤ 2 * R * |↑n - ↑m|

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|
Tactic:
repeat
  apply mul_nonneg
  linarith
  apply abs_nonneg
State after:
no goals

State before:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
⊢ z ∈ Metric.ball x R ×ˢ Metric.ball x R → ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
intro hz
State after:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : z ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

State before:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : z ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
simp at hz
State after:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : dist z.1 x < R ∧ dist z.2 x < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

State before:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : dist z.1 x < R ∧ dist z.2 x < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
rw [Real.dist_eq, Real.dist_eq] at hz
State after:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

State before:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
rw [Real.norm_eq_abs]
State after:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)| ≤ 2 * R * |↑n - ↑m|

State before:
case hS.hS
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)| ≤ 2 * R * |↑n - ↑m|
Tactic:
calc |(n - m) * (z.1 - x) - (n - m) * (z.2 - x)|
_ ≤ |(n - m) * (z.1 - x)| + |(n - m) * (z.2 - x)| := by apply abs_sub
_ = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| := by congr <;> apply abs_mul
_ ≤ |↑n - ↑m| * R + |↑n - ↑m| * R := by gcongr; linarith [hz.1]; linarith [hz.2]
_ = 2 * R * |↑n - ↑m| := by ring
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)| ≤ |(↑n - ↑m) * (z.1 - x)| + |(↑n - ↑m) * (z.2 - x)|
Tactic:
apply abs_sub
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x)| + |(↑n - ↑m) * (z.2 - x)| = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x|
Tactic:
congr <;> apply abs_mul
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| ≤ |↑n - ↑m| * R + |↑n - ↑m| * R
Tactic:
gcongr
State after:
case h₁.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.1 - x| ≤ R

case h₂.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R

State before:
case h₁.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.1 - x| ≤ R

case h₂.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R
Tactic:
linarith [hz.1]
State after:
case h₂.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R

State before:
case h₂.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R
Tactic:
linarith [hz.2]
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |↑n - ↑m| * R + |↑n - ↑m| * R = 2 * R * |↑n - ↑m|
Tactic:
ring
State after:
no goals

State before:
case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|
Tactic:
apply mul_nonneg
State after:
case ha.ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R

case ha.hb
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ |↑n - ↑m|

State before:
case ha.ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ 2 * R

case ha.hb
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ |↑n - ↑m|
Tactic:
linarith
State after:
case ha.hb
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ |↑n - ↑m|

State before:
case ha.hb
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 0 ≤ |↑n - ↑m|
Tactic:
apply abs_nonneg
State after:
no goals

State before:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
apply le_of_forall_lt
State after:
case neg.a.H
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ∀ c < 2 * R * |↑n - ↑m|, c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg.a.H
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ∀ c < 2 * R * |↑n - ↑m|, c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
intro c hc
State after:
case neg.a.H
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg.a.H
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
have := fact_isCompact_ball x R
State after:
case neg.a.H
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg.a.H
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
by_cases c_nonneg : 0 > c
State after:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : ¬0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : ¬0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
. calc c
    _ < 0 := c_nonneg
    _ ≤ @dist (withLocalOscillation (Metric.ball x R)) PseudoMetricSpace.toDist (θ n) (θ m) := dist_nonneg
    _ = localOscillation (Metric.ball x R) (θ n) (θ m) := rfl
    _ = ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
      rw [localOscillation]
      congr
      ext z
      congr
      rw [norm_integer_linear_eq]
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : ¬0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : ¬0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
push_neg at c_nonneg
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
set R' := (c + 2 * R * |(n : ℝ) - m|) / (4 * |(n : ℝ) - m|) with R'def
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
have hR' : 0 ≤ R' ∧ R' < R := by
  rw [R'def]
  constructor
  . positivity
  calc (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
    _ < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) := by
      gcongr
    _ = R := by
      ring_nf
      rw [mul_assoc, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_one]
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
let y := (x - R', x + R')
State after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
calc c
  _ = c / 2 + c / 2 := by ring
  _ < c / 2 + (2 * R * |↑n - ↑m|) / 2 := by
    gcongr
  _ = 2 * R' * |↑n - ↑m| := by
    rw [R'def]
    ring_nf
    rw [pow_two, ←mul_assoc, mul_assoc c, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_assoc (R * _), mul_inv_cancel norm_n_sub_m_pos.ne.symm]
    ring
  _ ≤ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ := by
    simp
    rw [sub_eq_add_neg (-((n - m) * R')), ←neg_add, abs_neg, ←two_mul, abs_mul, abs_mul, mul_comm |(n : ℝ) - m|, mul_assoc]
    simp
    gcongr
    apply le_abs_self
  _ ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
    apply ConditionallyCompleteLattice.le_biSup
    . convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
      apply norm_integer_linear_eq.symm
    . use y
      simp
      rw [abs_of_nonneg]
      exact hR'.2
      exact hR'.1
State after:
no goals

State before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
calc c
  _ < 0 := c_nonneg
  _ ≤ @dist (withLocalOscillation (Metric.ball x R)) PseudoMetricSpace.toDist (θ n) (θ m) := dist_nonneg
  _ = localOscillation (Metric.ball x R) (θ n) (θ m) := rfl
  _ = ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
    rw [localOscillation]
    congr
    ext z
    congr
    rw [norm_integer_linear_eq]
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
rw [localOscillation]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
congr
State after:
case e_s
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ (fun z => ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun z =>
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case e_s
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
⊢ (fun z => ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun z =>
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
ext z
State after:
case e_s.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case e_s.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
congr
State after:
case e_s.h.e_s
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
z : ℝ × ℝ
⊢ (fun h => ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun h => ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

State before:
case e_s.h.e_s
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 > c
z : ℝ × ℝ
⊢ (fun h => ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun h => ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
rw [norm_integer_linear_eq]
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ 0 ≤ R' ∧ R' < R
Tactic:
rw [R'def]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) ∧ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) ∧ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Tactic:
constructor
State after:
case left
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)

case right
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R

State before:
case left
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)

case right
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Tactic:
. positivity
State after:
case right
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R

State before:
case right
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Tactic:
calc (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
  _ < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) := by
    gcongr
  _ = R := by
    ring_nf
    rw [mul_assoc, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_one]
State after:
no goals

State before:
case left
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
Tactic:
positivity
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
Tactic:
gcongr
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) = R
Tactic:
ring_nf
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ R * |↑n - ↑m| * |↑n - ↑m|⁻¹ = R

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
⊢ R * |↑n - ↑m| * |↑n - ↑m|⁻¹ = R
Tactic:
rw [mul_assoc, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_one]
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c = c / 2 + c / 2
Tactic:
ring
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c / 2 + c / 2 < c / 2 + 2 * R * |↑n - ↑m| / 2
Tactic:
gcongr
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c / 2 + 2 * R * |↑n - ↑m| / 2 = 2 * R' * |↑n - ↑m|
Tactic:
rw [R'def]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c / 2 + 2 * R * |↑n - ↑m| / 2 = 2 * ((c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)) * |↑n - ↑m|

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c / 2 + 2 * R * |↑n - ↑m| / 2 = 2 * ((c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)) * |↑n - ↑m|
Tactic:
ring_nf
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * |↑n - ↑m| * |↑n - ↑m|⁻¹ * (1 / 2) + R * |↑n - ↑m| ^ 2 * |↑n - ↑m|⁻¹

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * |↑n - ↑m| * |↑n - ↑m|⁻¹ * (1 / 2) + R * |↑n - ↑m| ^ 2 * |↑n - ↑m|⁻¹
Tactic:
rw [pow_two, ←mul_assoc, mul_assoc c, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_assoc (R * _), mul_inv_cancel norm_n_sub_m_pos.ne.symm]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * 1 * (1 / 2) + R * |↑n - ↑m| * 1

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * 1 * (1 / 2) + R * |↑n - ↑m| * 1
Tactic:
ring
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 2 * R' * |↑n - ↑m| ≤ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
simp
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 2 * R' * |↑n - ↑m| ≤ |-((↑n - ↑m) * R') - (↑n - ↑m) * R'|

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 2 * R' * |↑n - ↑m| ≤ |-((↑n - ↑m) * R') - (↑n - ↑m) * R'|
Tactic:
rw [sub_eq_add_neg (-((n - m) * R')), ←neg_add, abs_neg, ←two_mul, abs_mul, abs_mul, mul_comm |(n : ℝ) - m|, mul_assoc]
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 2 * (R' * |↑n - ↑m|) ≤ |2| * (|R'| * |↑n - ↑m|)

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 2 * (R' * |↑n - ↑m|) ≤ |2| * (|R'| * |↑n - ↑m|)
Tactic:
simp
State after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' * |↑n - ↑m| ≤ |R'| * |↑n - ↑m|

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' * |↑n - ↑m| ≤ |R'| * |↑n - ↑m|
Tactic:
gcongr
State after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' ≤ |R'|

State before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' ≤ |R'|
Tactic:
apply le_abs_self
State after:
no goals

State before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ ≤
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
apply ConditionallyCompleteLattice.le_biSup
State after:
case hfs
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ BddAbove ((fun i => ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖) '' Metric.ball x R ×ˢ Metric.ball x R)

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ∃ i ∈ Metric.ball x R ×ˢ Metric.ball x R,
    ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖

State before:
case hfs
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ BddAbove ((fun i => ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖) '' Metric.ball x R ×ˢ Metric.ball x R)

case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ∃ i ∈ Metric.ball x R ×ˢ Metric.ball x R,
    ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
. convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
  apply norm_integer_linear_eq.symm
State after:
case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ∃ i ∈ Metric.ball x R ×ˢ Metric.ball x R,
    ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖

State before:
case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ∃ i ∈ Metric.ball x R ×ˢ Metric.ball x R,
    ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
. use y
  simp
  rw [abs_of_nonneg]
  exact hR'.2
  exact hR'.1
State after:
no goals

State before:
case hfs
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ BddAbove ((fun i => ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖) '' Metric.ball x R ×ˢ Metric.ball x R)
Tactic:
convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
State after:
case h.e'_3.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
a✝¹ : ℝ × ℝ
a✝ : a✝¹ ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (a✝¹.1 - x) - (↑n - ↑m) * (a✝¹.2 - x)‖ = ‖(θ n) a✝¹.1 - (θ m) a✝¹.1 - (θ n) a✝¹.2 + (θ m) a✝¹.2‖

State before:
case h.e'_3.h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
a✝¹ : ℝ × ℝ
a✝ : a✝¹ ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (a✝¹.1 - x) - (↑n - ↑m) * (a✝¹.2 - x)‖ = ‖(θ n) a✝¹.1 - (θ m) a✝¹.1 - (θ n) a✝¹.2 + (θ m) a✝¹.2‖
Tactic:
apply norm_integer_linear_eq.symm
State after:
no goals

State before:
case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ∃ i ∈ Metric.ball x R ×ˢ Metric.ball x R,
    ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
use y
State after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ y ∈ Metric.ball x R ×ˢ Metric.ball x R ∧
    ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖

State before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ y ∈ Metric.ball x R ×ˢ Metric.ball x R ∧
    ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
simp
State after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ |R'| < R

State before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ |R'| < R
Tactic:
rw [abs_of_nonneg]
State after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' < R

case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'

State before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' < R

case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'
Tactic:
exact hR'.2
State after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'

State before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'
Tactic:
exact hR'.1
State after:
no goals