awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ s ≠ 0

Tactic:
simpa using hs 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ s ≠ 0

Tactic:
have hs0 : s ≠ 0 := by simpa using hs 0
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₄ : (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₅ : Gamma s / (s * Gamma s) + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₆ : s⁻¹ + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₇ : s⁻¹ + deriv Gamma s / Gamma s = deriv Gamma s / Gamma s + s⁻¹
rw₈ rw₉ : deriv Gamma s / Gamma s + s⁻¹ = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹

Tactic:
rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]

Premises used: Complex.Gamma_add_one, Complex.deriv_Gamma_add_one, logDeriv_apply, add_comm, Complex.digamma_def, mul_div_mul_left, div_mul_cancel_right₀, Complex.Gamma_ne_zero, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
⊢ Meromorphic digamma

Tactic:
Meromorphic.Gamma.logDeriv

Premises used: Meromorphic.logDeriv, Meromorphic.Gamma, Complex.digamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
c T : ℝ
rw :
  rexp (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I) * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2).re) =
    rexp
      (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) T 2 - 2 * ((↑b.re : ℂ) + (↑b.im : ℂ) * I).im * c * T -
          ((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) c 2))
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2)‖ =
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
rw [Complex.norm_exp, neg_mul, neg_re, ← re_add_im b]

Premises used: Complex.neg_re, Complex.norm_exp, neg_mul, Complex.re_add_im
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
c T : ℝ
simp :
  rexp
      (-(b.re *
            ((T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) * (T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) -
              (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) * (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0))) -
          b.im *
            ((T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) * (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) +
              (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) * (T + (c * 0 - HMul.hMul (α := ℝ) 0 1))))) =
    rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))
⊢ rexp (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I) * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2).re) =
    rexp
      (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) T 2 - 2 * ((↑b.re : ℂ) + (↑b.im : ℂ) * I).im * c * T -
          ((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) c 2))

Tactic:
simp only [sq, re_add_im, mul_re, mul_im, add_re, add_im, ofReal_re, ofReal_im, I_re, I_im]

Premises used: Complex.mul_im, Complex.add_im, Complex.mul_re, Complex.add_re, sq, Complex.I_re, Complex.I_im, Complex.ofReal_re, Complex.ofReal_im, Complex.re_add_im
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
c T : ℝ
⊢ rexp
      (-(b.re *
            ((T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) * (T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) -
              (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) * (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0))) -
          b.im *
            ((T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) * (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) +
              (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) * (T + (c * 0 - HMul.hMul (α := ℝ) 0 1))))) =
    rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2 =
    b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
      HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2 =
    b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
      HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)

Tactic:
have :
    b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 =
      b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re) := by
    field
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2 =
    b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
      HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)
rw :
  rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2)) =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
rw₁ rw₂ :
  rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re))) =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2)‖ =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))

Tactic:
rw [norm_cexp_neg_mul_sq_add_mul_I, this]

Premises used: GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
rw :
  rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * y * T - b.re * HPow.hPow (β := ℕ) y 2)) ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
rw [norm_cexp_neg_mul_sq_add_mul_I b]

Premises used: GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : 2 * b.im * y ≤ 2 * |b.im| * |c|
a₁ : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) c 2
⊢ rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * y * T - b.re * HPow.hPow (β := ℕ) y 2)) ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
gcongr exp (-(_ - ?_ * _ - _ * ?_))

Premises used: HMul.hMul, HSub.hSub, Real.exp, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
rw : 2 * (b.im * y)
| 2 * b.im * y

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : 2 * (b.im * y) ≤ 2 * |b.im| * |c|
⊢ 2 * b.im * y ≤ 2 * |b.im| * |c|

Tactic:
conv_lhs => rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
rw : 2 * (|b.im| * |c|)
| 2 * |b.im| * |c|

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : 2 * (b.im * y) ≤ 2 * (|b.im| * |c|)
⊢ 2 * (b.im * y) ≤ 2 * |b.im| * |c|

Tactic:
conv_rhs => rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : b.im * y ≤ |b.im| * |c|
⊢ 2 * (b.im * y) ≤ 2 * (|b.im| * |c|)

Tactic:
gcongr _ * ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ b.im * y ≤ |b.im| * |c|

Tactic:
(le_abs_self _).trans ?_

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : |b.im * y| ≤ |b.im| * |c|
⊢ b.im * y ≤ |b.im| * |c|

Tactic:
refine (le_abs_self _).trans ?_

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : |b.im| * |y| ≤ |b.im| * |c|
⊢ |b.im * y| ≤ |b.im| * |c|

Tactic:
rw [abs_mul]

Premises used: abs_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : 0 ≤ |b.im|
⊢ |b.im| * |y| ≤ |b.im| * |c|

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a a₁ a₂ a₃ : |y| ≤ |c|
⊢ HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) c 2

Tactic:
rwa [sq_le_sq]

Premises used: sq_le_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
⊢ ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
have vert_norm_bound :
    ∀ {T : ℝ},
      0 ≤ T →
        ∀ {c y : ℝ},
          |y| ≤ |c| →
            ‖cexp (-b * (T + y * I) ^ 2)‖ ≤
              exp (-(b.re * T ^ 2 - (2 : ℝ) * |b.im| * |c| * T - b.re * c ^ 2)) := by
    intro T hT c y hy
    rw [norm_cexp_neg_mul_sq_add_mul_I b]
    gcongr exp (-(_ - ?_ * _ - _ * ?_))
    · (conv_lhs => rw [mul_assoc]); (conv_rhs => rw [mul_assoc])
      gcongr _ * ?_
      refine (le_abs_self _).trans ?_
      rw [abs_mul]
      gcongr
    · rwa [sq_le_sq]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
apply :
  2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c - 0| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
apply₁ : ℝ
apply₂ :
  ∀ x ∈ uIoc 0 c,
    ‖I *
          (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2) -
            cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))‖ ≤
      2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ ‖verticalIntegral b c T‖ ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
apply (intervalIntegral.norm_integral_le_of_norm_le_const _).trans

Premises used: intervalIntegral.norm_integral_le_of_norm_le_const, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
rw :
  2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c - 0| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
simp : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
| 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c|

Tactic:
simp only [mul_comm _ |c|]

Premises used: abs, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
conv_lhs :
  |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
conv_lhs => simp only [mul_comm _ |c|]

Premises used: abs, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
a : 2 * |c|
a₁ : rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
a : |c| * 2
| 2 * |c|

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
a : |c| * 2
a₁ : rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
congr
        rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
conv : |c| * 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
conv =>
        congr
        rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
rw : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
| |c| * 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
conv : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
conv =>
        congr
        rw [mul_comm]
      rw [mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
conv_rhs :
  |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
conv_rhs₁ :
  |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
⊢ |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
conv_rhs =>
      conv =>
        congr
        rw [mul_comm]
      rw [mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
⊢ |y| ≤ |c|

Tactic:
simpa using abs_sub_left_of_mem_uIcc (uIoc_subset_uIcc hy)

Premises used: Set.uIoc_subset_uIcc, Set.abs_sub_left_of_mem_uIcc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
⊢ |y| ≤ |c|

Tactic:
have absy : |y| ≤ |c| := by
      simpa using abs_sub_left_of_mem_uIcc (uIoc_subset_uIcc hy)
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
rw :
  ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
        cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2)‖ ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) +
      rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ ‖I *
        (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
          cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))‖ ≤
    2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
rw [norm_mul, norm_I, one_mul, two_mul]

Premises used: two_mul, norm_mul, Complex.norm_I, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
        cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2)‖ ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) +
      rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
(norm_sub_le _ _).trans (add_le_add (vert_norm_bound hT absy) ?_)

Premises used: norm_sub_le, add_le_add, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
refine :
  ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2)‖ ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
        cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2)‖ ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) +
      rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
refine (norm_sub_le _ _).trans (add_le_add (vert_norm_bound hT absy) ?_)

Premises used: norm_sub_le, add_le_add, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
⊢ |(-y)| ≤ |c|

Tactic:
rw [← abs_neg y] at absy

Premises used: abs_neg