Theorem: Hilbert_kernel_regularity (Carleson/Theorem1_1/Hilbert_kernel.lean)

State before:
x y y' : ℝ
⊢ 2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
rw [K, K]
State after:
x y y' : ℝ
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
x y y' : ℝ
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
wlog x_eq_zero : x = 0 generalizing x y y'
State after:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
. intro h
  set x_ := (0 : ℝ) with x_def
  set y_ := y - x with y_def
  set y'_ := y' - x with y'_def
  have h_ : 2 * |y_ - y'_| ≤ |x_ - y_| := by
    rw [x_def, y_def, y'_def]
    simpa
  have := this x_def h_
  rw [x_def, y_def, y'_def] at this
  simpa
State after:
x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
rw [x_eq_zero]
State after:
x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |0 - y| → ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)

State before:
x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |0 - y| → ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Tactic:
intro h
State after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |0 - y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)

State before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |0 - y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Tactic:
simp at h
State after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)

State before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Tactic:
simp only [zero_sub, abs_neg]
State after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
wlog yy'nonneg : 0 ≤ y ∧ 0 ≤ y' generalizing y y'
State after:
case inr
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case inr
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. by_cases yge0 : 0 ≤ y
  . push_neg at yy'nonneg
    exfalso
    rw [abs_of_nonneg yge0, abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]
  . push_neg at yge0
    by_cases y'ge0 : 0 ≤ y'
    . exfalso
      rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
    . push_neg at y'ge0
      set! y_ := -y with y_def
      set! y'_ := -y' with y'_def
      have h_ : 2 * |y_ - y'_| ≤ |y_| := by
        rw [y_def, y'_def, ← abs_neg]
        simpa [neg_add_eq_sub]
      have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
      have := this h_ y_y'_nonneg
      rw [y_def, y'_def] at this
      simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
      rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
      simpa
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
by_cases ypos : y ≤ 0
State after:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. have y_eq_zero : y = 0 := by
    exact le_antisymm ypos yy'nonneg.1
  have y'_eq_zero : y' = 0 := by
    rw [y_eq_zero] at h
    simp at h
    rw [abs_of_nonneg yy'nonneg.2] at h
    linarith
  rw [y_eq_zero, y'_eq_zero]
  simp
State after:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at ypos
State after:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have y2ley' : y / 2 ≤ y' := by
  rw [div_le_iff two_pos]
  calc y
    _ = 2 * (y - y') - y + 2 * y' := by ring
    _ ≤ 2 * |y - y'| - y + 2 * y' := by
      gcongr
      apply le_abs_self
    _ ≤ y - y + 2 * y' := by
      gcongr
      rw [abs_eq_self.mpr yy'nonneg.1] at h
      exact h
    _ = y' * 2 := by ring
State after:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rcases le_or_gt y 1, le_or_gt y' 1 with ⟨hy | hy, hy' | hy'⟩
State after:
case neg.inl.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg.inl.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy')
  gcongr <;> norm_num
State after:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. rw [@k_of_one_le_abs (-y')]
  . calc ‖k (-y) - 0‖
      _ = ‖k (-y) - k (-1)‖ := by
        congr
        apply (k_of_one_le_abs _).symm
        simp
      _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by
        apply Hilbert_kernel_regularity_main_part
        constructor
        all_goals linarith
      _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
        gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
        rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
      _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
        gcongr <;> norm_num
  . rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. rw [@k_of_one_le_abs (-y)]
  . calc ‖0 - k (-y')‖
      _ = ‖k (-1) - k (-y')‖ := by
        congr
        apply (k_of_one_le_abs _).symm
        simp
      _ = ‖k (-y') - k (-1)‖ := by
        rw [norm_sub_rev]
      _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by
        apply Hilbert_kernel_regularity_main_part
        constructor
        all_goals linarith
      _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by
        congr
        . rw [abs_of_nonneg]
          exact yy'nonneg.2
        . rw [abs_of_nonpos]
          simp
          linarith
        . rw [abs_of_nonneg]
          exact yy'nonneg.2
      _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by
        gcongr
        . apply div_nonneg <;> linarith
        . linarith
      _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by
        ring
      _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by
        gcongr
        apply div_nonneg <;> linarith
        rw [abs_of_nonneg yy'nonneg.1]
        rw [abs_of_nonneg] <;> linarith
        rw [abs_of_nonneg yy'nonneg.1]
      _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
        gcongr
        norm_num
  . rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. calc ‖k (-y) - k (-y')‖
    _ = 0 := by
      simp
      rw [k_of_one_le_abs, k_of_one_le_abs] <;> (rw [abs_neg, abs_of_nonneg] <;> linarith)
    _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
      apply mul_nonneg
      apply mul_nonneg
      . norm_num
      . simp
      . apply div_nonneg <;> simp
State after:
no goals

State before:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
intro h
State after:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
h : 2 * |y - y'| ≤ |x - y|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
h : 2 * |y - y'| ≤ |x - y|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
set x_ := (0 : ℝ) with x_def
State after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
set y_ := y - x with y_def
State after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
set y'_ := y' - x with y'_def
State after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
have h_ : 2 * |y_ - y'_| ≤ |x_ - y_| := by
  rw [x_def, y_def, y'_def]
  simpa
State after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
have := this x_def h_
State after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (x_ - y_) - k (x_ - y'_)‖ ≤ 2 ^ 8 * (1 / |x_ - y_|) * (|y_ - y'_| / |x_ - y_|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (x_ - y_) - k (x_ - y'_)‖ ≤ 2 ^ 8 * (1 / |x_ - y_|) * (|y_ - y'_| / |x_ - y_|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
rw [x_def, y_def, y'_def] at this
State after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (0 - (y - x)) - k (0 - (y' - x))‖ ≤ 2 ^ 8 * (1 / |0 - (y - x)|) * (|y - x - (y' - x)| / |0 - (y - x)|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)

State before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (0 - (y - x)) - k (0 - (y' - x))‖ ≤ 2 ^ 8 * (1 / |0 - (y - x)|) * (|y - x - (y' - x)| / |0 - (y - x)|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
simpa
State after:
no goals

State before:
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ 2 * |y_ - y'_| ≤ |x_ - y_|
Tactic:
rw [x_def, y_def, y'_def]
State after:
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ 2 * |y - x - (y' - x)| ≤ |0 - (y - x)|

State before:
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ 2 * |y - x - (y' - x)| ≤ |0 - (y - x)|
Tactic:
simpa
State after:
no goals

State before:
case inr
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
by_cases yge0 : 0 ≤ y
State after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : 0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : 0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. push_neg at yy'nonneg
  exfalso
  rw [abs_of_nonneg yge0, abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. push_neg at yge0
  by_cases y'ge0 : 0 ≤ y'
  . exfalso
    rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
  . push_neg at y'ge0
    set! y_ := -y with y_def
    set! y'_ := -y' with y'_def
    have h_ : 2 * |y_ - y'_| ≤ |y_| := by
      rw [y_def, y'_def, ← abs_neg]
      simpa [neg_add_eq_sub]
    have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
    have := this h_ y_y'_nonneg
    rw [y_def, y'_def] at this
    simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
    rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
    simpa
State after:
no goals

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : 0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at yy'nonneg
State after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
exfalso
State after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ False

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ False
Tactic:
rw [abs_of_nonneg yge0, abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]
State after:
no goals

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at yge0
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
by_cases y'ge0 : 0 ≤ y'
State after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. exfalso
  rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. push_neg at y'ge0
  set! y_ := -y with y_def
  set! y'_ := -y' with y'_def
  have h_ : 2 * |y_ - y'_| ≤ |y_| := by
    rw [y_def, y'_def, ← abs_neg]
    simpa [neg_add_eq_sub]
  have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
  have := this h_ y_y'_nonneg
  rw [y_def, y'_def] at this
  simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
  rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
  simpa
State after:
no goals

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
exfalso
State after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : 0 ≤ y'
⊢ False

State before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : 0 ≤ y'
⊢ False
Tactic:
rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
State after:
no goals

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at y'ge0
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
set! y_ := -y with y_def
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
set! y'_ := -y' with y'_def
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have h_ : 2 * |y_ - y'_| ≤ |y_| := by
  rw [y_def, y'_def, ← abs_neg]
  simpa [neg_add_eq_sub]
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have := this h_ y_y'_nonneg
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y_) - k (-y'_)‖ ≤ 2 ^ 8 * (1 / |y_|) * (|y_ - y'_| / |y_|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y_) - k (-y'_)‖ ≤ 2 ^ 8 * (1 / |y_|) * (|y_ - y'_| / |y_|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [y_def, y'_def] at this
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (- -y) - k (- -y')‖ ≤ 2 ^ 8 * (1 / |(-y)|) * (|-y - -y'| / |(-y)|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (- -y) - k (- -y')‖ ≤ 2 ^ 8 * (1 / |(-y)|) * (|-y - -y'| / |(-y)|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k y - k y'‖ ≤ 2 ^ 8 * (1 / |y|) * (|y' - y| / |y|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k y - k y'‖ ≤ 2 ^ 8 * (1 / |y|) * (|y' - y| / |y|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
State after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|(-(y' - y))| / |y|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this✝ : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|(-(y' - y))| / |y|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
simpa
State after:
no goals

State before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ 2 * |y_ - y'_| ≤ |y_|
Tactic:
rw [y_def, y'_def, ← abs_neg]
State after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ 2 * |(-(-y - -y'))| ≤ |(-y)|

State before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ 2 * |(-(-y - -y'))| ≤ |(-y)|
Tactic:
simpa [neg_add_eq_sub]
State after:
no goals

State before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
⊢ 0 ≤ y_ ∧ 0 ≤ y'_
Tactic:
constructor <;> linarith
State after:
no goals

State before:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have y_eq_zero : y = 0 := by
  exact le_antisymm ypos yy'nonneg.1
State after:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have y'_eq_zero : y' = 0 := by
  rw [y_eq_zero] at h
  simp at h
  rw [abs_of_nonneg yy'nonneg.2] at h
  linarith
State after:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [y_eq_zero, y'_eq_zero]
State after:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-0) - k (-0)‖ ≤ 2 ^ 8 * (1 / |0|) * (|0 - 0| / |0|)

State before:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-0) - k (-0)‖ ≤ 2 ^ 8 * (1 / |0|) * (|0 - 0| / |0|)
Tactic:
simp
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
⊢ y = 0
Tactic:
exact le_antisymm ypos yy'nonneg.1
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ y' = 0
Tactic:
rw [y_eq_zero] at h
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |0 - y'| ≤ |0|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ y' = 0

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |0 - y'| ≤ |0|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ y' = 0
Tactic:
simp at h
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * |y'| ≤ 0
⊢ y' = 0

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * |y'| ≤ 0
⊢ y' = 0
Tactic:
rw [abs_of_nonneg yy'nonneg.2] at h
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * y' ≤ 0
⊢ y' = 0

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * y' ≤ 0
⊢ y' = 0
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y / 2 ≤ y'
Tactic:
rw [div_le_iff two_pos]
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y ≤ y' * 2

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y ≤ y' * 2
Tactic:
calc y
  _ = 2 * (y - y') - y + 2 * y' := by ring
  _ ≤ 2 * |y - y'| - y + 2 * y' := by
    gcongr
    apply le_abs_self
  _ ≤ y - y + 2 * y' := by
    gcongr
    rw [abs_eq_self.mpr yy'nonneg.1] at h
    exact h
  _ = y' * 2 := by ring
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y = 2 * (y - y') - y + 2 * y'
Tactic:
ring
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * (y - y') - y + 2 * y' ≤ 2 * |y - y'| - y + 2 * y'
Tactic:
gcongr
State after:
case bc.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y - y' ≤ |y - y'|

State before:
case bc.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y - y' ≤ |y - y'|
Tactic:
apply le_abs_self
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| - y + 2 * y' ≤ y - y + 2 * y'
Tactic:
gcongr
State after:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y

State before:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y
Tactic:
rw [abs_eq_self.mpr yy'nonneg.1] at h
State after:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ y
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y

State before:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ y
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y
Tactic:
exact h
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y - y + 2 * y' = y' * 2
Tactic:
ring
State after:
no goals

State before:
case neg.inl.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy')
State after:
case neg.inl.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

State before:
case neg.inl.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr <;> norm_num
State after:
no goals

State before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [@k_of_one_le_abs (-y')]
State after:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|

State before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Tactic:
. calc ‖k (-y) - 0‖
    _ = ‖k (-y) - k (-1)‖ := by
      congr
      apply (k_of_one_le_abs _).symm
      simp
    _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by
      apply Hilbert_kernel_regularity_main_part
      constructor
      all_goals linarith
    _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
      rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
    _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr <;> norm_num
State after:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|

State before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Tactic:
. rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
no goals

State before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
calc ‖k (-y) - 0‖
  _ = ‖k (-y) - k (-1)‖ := by
    congr
    apply (k_of_one_le_abs _).symm
    simp
  _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by
    apply Hilbert_kernel_regularity_main_part
    constructor
    all_goals linarith
  _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
    rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
  _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr <;> norm_num
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ = ‖k (-y) - k (-1)‖
Tactic:
congr
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 = k (-1)

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 = k (-1)
Tactic:
apply (k_of_one_le_abs _).symm
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-1)|

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-1)|
Tactic:
simp
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-1)‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|)
Tactic:
apply Hilbert_kernel_regularity_main_part
State after:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1

State before:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Tactic:
constructor
State after:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1

State before:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Tactic:
all_goals linarith
State after:
no goals

State before:
case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
State after:
case h.hab
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ |y - 1| ≤ |y - y'|

State before:
case h.hab
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ |y - 1| ≤ |y - y'|
Tactic:
rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr <;> norm_num
State after:
no goals

State before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Tactic:
rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
no goals

State before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [@k_of_one_le_abs (-y)]
State after:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|

State before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Tactic:
. calc ‖0 - k (-y')‖
    _ = ‖k (-1) - k (-y')‖ := by
      congr
      apply (k_of_one_le_abs _).symm
      simp
    _ = ‖k (-y') - k (-1)‖ := by
      rw [norm_sub_rev]
    _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by
      apply Hilbert_kernel_regularity_main_part
      constructor
      all_goals linarith
    _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by
      congr
      . rw [abs_of_nonneg]
        exact yy'nonneg.2
      . rw [abs_of_nonpos]
        simp
        linarith
      . rw [abs_of_nonneg]
        exact yy'nonneg.2
    _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by
      gcongr
      . apply div_nonneg <;> linarith
      . linarith
    _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by
      ring
    _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr
      apply div_nonneg <;> linarith
      rw [abs_of_nonneg yy'nonneg.1]
      rw [abs_of_nonneg] <;> linarith
      rw [abs_of_nonneg yy'nonneg.1]
    _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr
      norm_num
State after:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|

State before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Tactic:
. rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
no goals

State before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
calc ‖0 - k (-y')‖
  _ = ‖k (-1) - k (-y')‖ := by
    congr
    apply (k_of_one_le_abs _).symm
    simp
  _ = ‖k (-y') - k (-1)‖ := by
    rw [norm_sub_rev]
  _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by
    apply Hilbert_kernel_regularity_main_part
    constructor
    all_goals linarith
  _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by
    congr
    . rw [abs_of_nonneg]
      exact yy'nonneg.2
    . rw [abs_of_nonpos]
      simp
      linarith
    . rw [abs_of_nonneg]
      exact yy'nonneg.2
  _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by
    gcongr
    . apply div_nonneg <;> linarith
    . linarith
  _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by
    ring
  _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr
    apply div_nonneg <;> linarith
    rw [abs_of_nonneg yy'nonneg.1]
    rw [abs_of_nonneg] <;> linarith
    rw [abs_of_nonneg yy'nonneg.1]
  _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr
    norm_num
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ = ‖k (-1) - k (-y')‖
Tactic:
congr
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 = k (-1)

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 = k (-1)
Tactic:
apply (k_of_one_le_abs _).symm
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-1)|

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-1)|
Tactic:
simp
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-1) - k (-y')‖ = ‖k (-y') - k (-1)‖
Tactic:
rw [norm_sub_rev]
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y') - k (-1)‖ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|)
Tactic:
apply Hilbert_kernel_regularity_main_part
State after:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y' ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1

State before:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y' ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Tactic:
constructor
State after:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1

State before:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Tactic:
all_goals linarith
State after:
no goals

State before:
case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) = 2 ^ 6 * (1 / y') * ((1 - y') / y')
Tactic:
congr
State after:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

State before:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
. rw [abs_of_nonneg]
  exact yy'nonneg.2
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
. rw [abs_of_nonpos]
  simp
  linarith
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
. rw [abs_of_nonneg]
  exact yy'nonneg.2
State after:
no goals

State before:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
rw [abs_of_nonneg]
State after:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'

State before:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'
Tactic:
exact yy'nonneg.2
State after:
no goals

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'
Tactic:
rw [abs_of_nonpos]
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ -(y' - 1) = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ -(y' - 1) = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0
Tactic:
simp
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0
Tactic:
linarith
State after:
no goals

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
rw [abs_of_nonneg]
State after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'

State before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'
Tactic:
exact yy'nonneg.2
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * (1 / y') * ((1 - y') / y') ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2))
Tactic:
gcongr
State after:
case c0
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ (1 - y') / y'

case h₂.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1 - y'

State before:
case c0
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ (1 - y') / y'

case h₂.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1 - y'
Tactic:
. apply div_nonneg <;> linarith
State after:
case h₂.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1 - y'

State before:
case h₂.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1 - y'
Tactic:
. linarith
State after:
no goals

State before:
case c0
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ (1 - y') / y'
Tactic:
apply div_nonneg <;> linarith
State after:
no goals

State before:
case h₂.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1 - y'
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) = 2 ^ 6 * 2 * 2 * (1 / y) * ((1 - y') / y)
Tactic:
ring
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * 2 * 2 * (1 / y) * ((1 - y') / y) ≤ 2 ^ 6 * 2 * 2 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr
State after:
case c0
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ (1 - y') / y

case h₁.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

case h₂.hac
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 - y' ≤ |y - y'|

case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

State before:
case c0
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ (1 - y') / y

case h₁.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

case h₂.hac
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 - y' ≤ |y - y'|

case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y
Tactic:
apply div_nonneg <;> linarith
State after:
case h₁.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

case h₂.hac
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 - y' ≤ |y - y'|

case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

State before:
case h₁.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

case h₂.hac
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 - y' ≤ |y - y'|

case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y
Tactic:
rw [abs_of_nonneg yy'nonneg.1]
State after:
case h₂.hac
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 - y' ≤ |y - y'|

case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

State before:
case h₂.hac
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 - y' ≤ |y - y'|

case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y
Tactic:
rw [abs_of_nonneg] <;> linarith
State after:
case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y

State before:
case h₂.hbd
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y| ≤ y
Tactic:
rw [abs_of_nonneg yy'nonneg.1]
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * 2 * 2 * (1 / |y|) * (|y - y'| / |y|) ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr
State after:
case h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * 2 * 2 ≤ 2 ^ 8

State before:
case h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * 2 * 2 ≤ 2 ^ 8
Tactic:
norm_num
State after:
no goals

State before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Tactic:
rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
no goals

State before:
case neg.inr.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
calc ‖k (-y) - k (-y')‖
  _ = 0 := by
    simp
    rw [k_of_one_le_abs, k_of_one_le_abs] <;> (rw [abs_neg, abs_of_nonneg] <;> linarith)
  _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
    apply mul_nonneg
    apply mul_nonneg
    . norm_num
    . simp
    . apply div_nonneg <;> simp
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ ‖k (-y) - k (-y')‖ = 0
Tactic:
simp
State after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ k (-y) = k (-y')

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ k (-y) = k (-y')
Tactic:
rw [k_of_one_le_abs, k_of_one_le_abs] <;> (rw [abs_neg, abs_of_nonneg] <;> linarith)
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 1 ≤ |(-y)|
Tactic:
rw [abs_neg, abs_of_nonneg] <;> linarith
State after:
no goals

State before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
apply mul_nonneg
State after:
case ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 2 ^ 8 * (1 / |y|)

case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|

State before:
case ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 2 ^ 8 * (1 / |y|)

case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|
Tactic:
apply mul_nonneg
State after:
case ha.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 2 ^ 8

case ha.hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 1 / |y|

case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|

State before:
case ha.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 2 ^ 8

case ha.hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 1 / |y|

case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|
Tactic:
. norm_num
State after:
case ha.hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 1 / |y|

case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|

State before:
case ha.hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 1 / |y|

case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|
Tactic:
. simp
State after:
case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|

State before:
case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|
Tactic:
. apply div_nonneg <;> simp
State after:
no goals

State before:
case ha.ha
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 2 ^ 8
Tactic:
norm_num
State after:
no goals

State before:
case ha.hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ 1 / |y|
Tactic:
simp
State after:
no goals

State before:
case hb
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ 0 ≤ |y - y'| / |y|
Tactic:
apply div_nonneg <;> simp
State after:
no goals