Theorem: CarlesonOperatorReal'_mul (Carleson/Theorem1_1/CarlesonOperatorReal.lean)

State before:
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ T' f x = ↑a.toNNReal * T' (fun x => 1 / ↑a * f x) x
Tactic:
rw [CarlesonOperatorReal', CarlesonOperatorReal', ENNReal.mul_iSup]
State after:
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊

State before:
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊
Tactic:
congr
State after:
case e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ (fun n =>
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊

State before:
case e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ (fun n =>
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊
Tactic:
ext n
State after:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
rw [ENNReal.mul_iSup]
State after:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ (_ : 0 < i),
          ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ (_ : 0 < i),
          ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
congr
State after:
case e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ (fun r =>
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ (fun r =>
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
ext r
State after:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
rw [ENNReal.mul_iSup]
State after:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ (_ : 0 < r),
      ↑a.toNNReal *
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ (_ : 0 < r),
      ↑a.toNNReal *
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
congr
State after:
case e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ (fun x_1 => ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ (fun x_1 => ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
ext rpos
State after:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
rw [ENNReal.mul_iSup]
State after:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ (_ : r < 1),
      ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ (_ : r < 1),
      ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
congr
State after:
case e_s.h.e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ (fun x_1 => ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) = fun i =>
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ (fun x_1 => ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) = fun i =>
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
ext rle1
State after:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
norm_cast
State after:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply NNReal.eq
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑(a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊)

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑(a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊)
Tactic:
simp only [coe_nnnorm, NNReal.coe_mul]
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ↑a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ↑a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖
Tactic:
rw [← Real.norm_of_nonneg (@NNReal.zero_le_coe a.toNNReal), ← Complex.norm_real, ← norm_mul]
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ‖↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ‖↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖
Tactic:
congr
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp
Tactic:
rw [← MeasureTheory.integral_mul_left, Real.coe_toNNReal a ha.le]
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ∫ (a_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ∫ (a_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)
Tactic:
congr
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun a_1 =>
    ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun a_1 =>
    ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)
Tactic:
ext y
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp)

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp)
Tactic:
field_simp
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (f y * K x y * (Complex.I * ↑n * ↑y).exp) / ↑a

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (f y * K x y * (Complex.I * ↑n * ↑y).exp) / ↑a
Tactic:
rw [mul_div_cancel_left₀]
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ↑a ≠ 0

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ↑a ≠ 0
Tactic:
norm_cast
State after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ¬a = 0

State before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ¬a = 0
Tactic:
exact ha.ne.symm
State after:
no goals