awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
⊢ (↑(finrank ℝ V) : ℝ) = (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume

Tactic:
hf
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume

Tactic:
exact hf
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ ContinuousAt f v

Tactic:
h'f
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ ContinuousAt f v

Tactic:
exact h'f
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))

Tactic:
have A : Tendsto (fun (c : ℝ) ↦ ∫ w : V, (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
      atTop (𝓝 (f v)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable'
    · exact fun x ↦ by positivity
    · rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]
      nth_rewrite 2 [← pow_one π]
      rw [← rpow_natCast, ← rpow_natCast, ← rpow_sub pi_pos, ← rpow_mul pi_nonneg,
        ← rpow_add pi_pos]
      ring_nf
      exact rpow_zero _
    · have A : Tendsto (fun (w : V) ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop := by
        rw [tendsto_const_mul_atTop_of_pos (by positivity)]
        apply (tendsto_pow_atTop two_ne_zero).comp tendsto_norm_cobounded_atTop
      have B := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (finrank ℝ V / 2) 1
        zero_lt_one |>.comp A |>.const_mul (π ^ (-finrank ℝ V / 2 : ℝ))
      rw [mul_zero] at B
      convert! B using 2 with x
      simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]
      congr 1
      rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg,
        ← rpow_mul (norm_nonneg _), ← mul_assoc, ← rpow_add pi_pos, mul_comm]
      congr <;> ring
    · exact hf
    · exact h'f
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))

Tactic:
have B : Tendsto
      (fun (c : ℝ) ↦
        ∫ w : V, ((c ^ (1 / 2 : ℝ)) ^ finrank ℝ V * φ ((c ^ (1 / 2 : ℝ)) • (v - w))) • f w)
      atTop (𝓝 (f v)) :=
    A.comp (tendsto_rpow_atTop (by simp))
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
apply :
  EventuallyEq.{0, u_2} (β := E) atTop
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
    atTop (𝓝 (f v))

Tactic:
apply B.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
h :
  ∀ (hc : 0 < c),
    Eq.{u_2 + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) c →
    Eq.{u_2 + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)

Tactic:
(hc : 0 < c)
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
h :
  ∀ (c : ℝ) (hc : 0 < c),
    Eq.{u_2 + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
⊢ EventuallyEq.{0, u_2} (β := E) atTop
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w

Tactic:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
h :
  ∀ (w : V),
    ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w =
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w)

Tactic:
congr with w
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) • f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
⊢ ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w

Tactic:
rw [← coe_smul]

Premises used: Complex.coe_smul
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) • f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) *
      cexp (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)

Tactic:
rw [ofReal_mul, ofReal_mul, ofReal_exp, ← mul_assoc]

Premises used: mul_assoc, Complex.ofReal_exp, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2
h₁ :
  (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) *
      cexp (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  (↑π : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) * (↑c : ℂ) ^ (↑(1 / 2 * (↑(finrank ℝ V) : ℝ)) : ℂ) =
    (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 * (↑c : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2

Tactic:
rw [mul_cpow_ofReal_nonneg pi_nonneg hc.le, ← rpow_natCast, ← rpow_mul hc.le, mul_comm,
      ofReal_cpow pi_nonneg, ofReal_cpow hc.le]

Premises used: Real.pi_nonneg, Complex.ofReal_cpow, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, mul_comm, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ (↑π : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) * (↑c : ℂ) ^ (↑(1 / 2 * (↑(finrank ℝ V) : ℝ)) : ℂ) =
    (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 * (↑c : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2

Tactic:
simp [div_eq_inv_mul]

Premises used: div_eq_inv_mul