[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
let e : C(ℝ, ℂ) := (fourier (-m)).comp ⟨((↑) : ℝ → UnitAddCircle), continuous_quotient_mk'⟩
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ :=
  by
  have : ∀ x : ℝ, ‖e x‖ = 1 := fun x => abs_coe_circle (AddCircle.toCircle (-m • x))
  intro K g
  simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
[PROOFSTEP]
have : ∀ x : ℝ, ‖e x‖ = 1 := fun x => abs_coe_circle (AddCircle.toCircle (-m • x))
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
this : ∀ (x : ℝ), ‖↑e x‖ = 1
⊢ ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
[PROOFSTEP]
intro K g
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
this : ∀ (x : ℝ), ‖↑e x‖ = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
[PROOFSTEP]
simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight n) = e :=
  by
  intro n; ext1 x
  have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
  simpa only [mul_one] using this.int_mul n x
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
⊢ ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
[PROOFSTEP]
intro n
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
n : ℤ
⊢ ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
[PROOFSTEP]
ext1 x
[GOAL]
case h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
n : ℤ
x : ℝ
⊢ ↑(ContinuousMap.comp e (ContinuousMap.addRight ↑n)) x = ↑e x
[PROOFSTEP]
have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
[GOAL]
case h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
n : ℤ
x : ℝ
this : Periodic (↑e) 1
⊢ ↑(ContinuousMap.comp e (ContinuousMap.addRight ↑n)) x = ↑e x
[PROOFSTEP]
simpa only [mul_one] using this.int_mul n x
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
calc
  fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
      ∫ x in (0 : ℝ)..1, e x * (∑' n : ℤ, f.comp (ContinuousMap.addRight n)) x :=
    by
    simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, comp_apply, coe_mk, Periodic.lift_coe,
      zsmul_one, smul_eq_mul]
      -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
  _ = ∫ x in (0 : ℝ)..1, ∑' n : ℤ, (e * f.comp (ContinuousMap.addRight n)) x := by
    simp_rw [coe_mul, Pi.mul_apply, ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
      -- Swap sum and integral.
  _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f.comp (ContinuousMap.addRight n)) x :=
    by
    refine' (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm _).symm
    convert hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
    exact funext fun n => neK _ _
  _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f).comp (ContinuousMap.addRight n) x :=
    by
    simp only [ContinuousMap.comp_apply, mul_comp] at eadd ⊢
    simp_rw [eadd]
      -- Rearrange sum of interval integrals into an integral over `ℝ`.
  _ = ∫ x, e x * f x :=
    by
    suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
    apply integrable_of_summable_norm_Icc
    convert hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
    simp_rw [mul_comp] at eadd ⊢
    simp_rw [eadd]
    exact
      funext fun n =>
        neK ⟨Icc 0 1, isCompact_Icc⟩
          _
            -- Minor tidying to finish
  _ = 𝓕 f m := by
    rw [fourierIntegral_eq_integral_exp_smul]
    congr 1 with x : 1
    rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
    congr 2
    push_cast
    ring
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    ∫ (x : ℝ) in 0 ..1, ↑e x * ↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, comp_apply, coe_mk, Periodic.lift_coe,
  zsmul_one, smul_eq_mul]
  -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0 ..1, ↑e x * ↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x =
    ∫ (x : ℝ) in 0 ..1, ∑' (n : ℤ), ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
simp_rw [coe_mul, Pi.mul_apply, ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
  -- Swap sum and integral.
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0 ..1, ∑' (n : ℤ), ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
refine' (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm _).symm
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ Summable fun i =>
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := (_ : IsCompact (uIcc 0 1)) })
        (e * ContinuousMap.comp f (ContinuousMap.addRight ↑i))‖
[PROOFSTEP]
convert hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ (fun i =>
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := (_ : IsCompact (uIcc 0 1)) })
          (e * ContinuousMap.comp f (ContinuousMap.addRight ↑i))‖) =
    fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := (_ : IsCompact (uIcc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
exact funext fun n => neK _ _
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
simp only [ContinuousMap.comp_apply, mul_comp] at eadd ⊢
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd :
  ∀ (n : ℤ),
    ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
        (ContinuousMap.addRight ↑n) =
      ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ ∑' (n : ℤ),
      ∫ (x : ℝ) in 0 ..1,
        ↑(ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk) *
              ContinuousMap.comp f (ContinuousMap.addRight ↑n))
          x =
    ∑' (n : ℤ),
      ∫ (x : ℝ) in 0 ..1,
        ↑(ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
                (ContinuousMap.addRight ↑n) *
              ContinuousMap.comp f (ContinuousMap.addRight ↑n))
          x
[PROOFSTEP]
simp_rw [eadd]
  -- Rearrange sum of interval integrals into an integral over `ℝ`.
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n)) x = ∫ (x : ℝ), ↑e x * ↑f x
[PROOFSTEP]
suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ Integrable ↑(e * f)
[PROOFSTEP]
apply integrable_of_summable_norm_Icc
[GOAL]
case hf
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
convert hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ (fun n => ‖ContinuousMap.restrict (Icc 0 1) (ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n))‖) = fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := (_ : IsCompact (Icc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
simp_rw [mul_comp] at eadd ⊢
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd :
  ∀ (n : ℤ),
    ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
        (ContinuousMap.addRight ↑n) =
      ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ (fun n =>
      ‖ContinuousMap.restrict (Icc 0 1)
          (ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
              (ContinuousMap.addRight ↑n) *
            ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖) =
    fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := (_ : IsCompact (Icc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
simp_rw [eadd]
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd :
  ∀ (n : ℤ),
    ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
        (ContinuousMap.addRight ↑n) =
      ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ (fun n =>
      ‖ContinuousMap.restrict (Icc 0 1)
          (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk) *
            ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖) =
    fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := (_ : IsCompact (Icc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
exact
  funext fun n =>
    neK ⟨Icc 0 1, isCompact_Icc⟩
      _
        -- Minor tidying to finish
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), ↑e x * ↑f x = 𝓕 ↑f ↑m
[PROOFSTEP]
rw [fourierIntegral_eq_integral_exp_smul]
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), ↑e x * ↑f x = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * ↑m) * I) • ↑f v
[PROOFSTEP]
congr 1 with x : 1
[GOAL]
case e_f.h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ ↑e x * ↑f x = Complex.exp (↑(-2 * π * x * ↑m) * I) • ↑f x
[PROOFSTEP]
rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
[GOAL]
case e_f.h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ Complex.exp (2 * ↑π * I * ↑(-m) * ↑x / ↑1) * ↑f x = Complex.exp (↑(-2 * π * x * ↑m) * I) * ↑f x
[PROOFSTEP]
congr 2
[GOAL]
case e_f.h.e_a.e_z
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ 2 * ↑π * I * ↑(-m) * ↑x / ↑1 = ↑(-2 * π * x * ↑m) * I
[PROOFSTEP]
push_cast
[GOAL]
case e_f.h.e_a.e_z
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ 2 * ↑π * I * -↑m * ↑x / 1 = -2 * ↑π * ↑x * ↑m * I
[PROOFSTEP]
ring
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
let F : C(UnitAddCircle, ℂ) :=
  ⟨(f.periodic_tsum_comp_add_zsmul 1).lift, continuous_coinduced_dom.mpr (map_continuous _)⟩
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
have : Summable (fourierCoeff F) := by
  convert h_sum
  exact Real.fourierCoeff_tsum_comp_add h_norm _
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
⊢ Summable (fourierCoeff ↑F)
[PROOFSTEP]
convert h_sum
[GOAL]
case h.e'_5.h
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
x✝ : ℤ
⊢ fourierCoeff (↑F) x✝ = 𝓕 ↑f ↑x✝
[PROOFSTEP]
exact Real.fourierCoeff_tsum_comp_add h_norm _
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
convert (has_pointwise_sum_fourier_series_of_summable this 0).tsum_eq.symm using 1
[GOAL]
case h.e'_2
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
⊢ ∑' (n : ℤ), ↑f ↑n = ↑F 0
[PROOFSTEP]
have := (hasSum_apply (summable_of_locally_summable_norm h_norm).hasSum 0).tsum_eq
[GOAL]
case h.e'_2
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this✝ : Summable (fourierCoeff ↑F)
this :
  ∑' (b : ℤ), ↑(ContinuousMap.comp f (ContinuousMap.addRight ↑b)) 0 =
    ↑(∑' (b : ℤ), ContinuousMap.comp f (ContinuousMap.addRight ↑b)) 0
⊢ ∑' (n : ℤ), ↑f ↑n = ↑F 0
[PROOFSTEP]
simpa only [coe_mk, ← QuotientAddGroup.mk_zero, Periodic.lift_coe, zsmul_one, comp_apply, coe_addRight, zero_add] using
  this
[GOAL]
case h.e'_3
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
⊢ ∑' (n : ℤ), 𝓕 ↑f ↑n = ∑' (b : ℤ), fourierCoeff (↑F) b • ↑(fourier b) 0
[PROOFSTEP]
congr 1 with n : 1
[GOAL]
case h.e'_3.e_f.h
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
n : ℤ
⊢ 𝓕 ↑f ↑n = fourierCoeff (↑F) n • ↑(fourier n) 0
[PROOFSTEP]
rw [← Real.fourierCoeff_tsum_comp_add h_norm n, fourier_eval_zero, smul_eq_mul, mul_one]
[GOAL]
case h.e'_3.e_f.h
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
n : ℤ
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      n =
    fourierCoeff (↑F) n
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
have claim : ∀ x : ℝ, max 0 (-2 * R) < x → ∀ y : ℝ, x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b) :=
  by
  intro x hx y hy
  rw [max_lt_iff] at hx
  have hxR : 0 < x + R := by
    rcases le_or_lt 0 R with (h | h)
    · exact add_pos_of_pos_of_nonneg hx.1 h
    · rw [← sub_lt_iff_lt_add, zero_sub]
      refine' lt_trans _ hx.2
      rwa [neg_mul, neg_lt_neg_iff, two_mul, add_lt_iff_neg_left]
  have hy' : 0 < y := hxR.trans_le hy
  have : y ^ (-b) ≤ (x + R) ^ (-b) :=
    by
    rw [rpow_neg hy'.le, rpow_neg hxR.le, inv_le_inv (rpow_pos_of_pos hy' _) (rpow_pos_of_pos hxR _)]
    exact rpow_le_rpow hxR.le hy hb.le
  refine' this.trans _
  rw [← mul_rpow one_half_pos.le hx.1.le, rpow_neg (mul_pos one_half_pos hx.1).le, rpow_neg hxR.le]
  refine' inv_le_inv_of_le (rpow_pos_of_pos (mul_pos one_half_pos hx.1) _) _
  exact rpow_le_rpow (mul_pos one_half_pos hx.1).le (by linarith) hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
⊢ ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
intro x hx y hy
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : max 0 (-2 * R) < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
rw [max_lt_iff] at hx
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
have hxR : 0 < x + R := by
  rcases le_or_lt 0 R with (h | h)
  · exact add_pos_of_pos_of_nonneg hx.1 h
  · rw [← sub_lt_iff_lt_add, zero_sub]
    refine' lt_trans _ hx.2
    rwa [neg_mul, neg_lt_neg_iff, two_mul, add_lt_iff_neg_left]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ 0 < x + R
[PROOFSTEP]
rcases le_or_lt 0 R with (h | h)
[GOAL]
case inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : 0 ≤ R
⊢ 0 < x + R
[PROOFSTEP]
exact add_pos_of_pos_of_nonneg hx.1 h
[GOAL]
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : R < 0
⊢ 0 < x + R
[PROOFSTEP]
rw [← sub_lt_iff_lt_add, zero_sub]
[GOAL]
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : R < 0
⊢ -R < x
[PROOFSTEP]
refine' lt_trans _ hx.2
[GOAL]
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : R < 0
⊢ -R < -2 * R
[PROOFSTEP]
rwa [neg_mul, neg_lt_neg_iff, two_mul, add_lt_iff_neg_left]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
have hy' : 0 < y := hxR.trans_le hy
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
have : y ^ (-b) ≤ (x + R) ^ (-b) :=
  by
  rw [rpow_neg hy'.le, rpow_neg hxR.le, inv_le_inv (rpow_pos_of_pos hy' _) (rpow_pos_of_pos hxR _)]
  exact rpow_le_rpow hxR.le hy hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
⊢ y ^ (-b) ≤ (x + R) ^ (-b)
[PROOFSTEP]
rw [rpow_neg hy'.le, rpow_neg hxR.le, inv_le_inv (rpow_pos_of_pos hy' _) (rpow_pos_of_pos hxR _)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
⊢ (x + R) ^ b ≤ y ^ b
[PROOFSTEP]
exact rpow_le_rpow hxR.le hy hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
refine' this.trans _
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ (x + R) ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
rw [← mul_rpow one_half_pos.le hx.1.le, rpow_neg (mul_pos one_half_pos hx.1).le, rpow_neg hxR.le]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ ((x + R) ^ b)⁻¹ ≤ ((1 / 2 * x) ^ b)⁻¹
[PROOFSTEP]
refine' inv_le_inv_of_le (rpow_pos_of_pos (mul_pos one_half_pos hx.1) _) _
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ (1 / 2 * x) ^ b ≤ (x + R) ^ b
[PROOFSTEP]
exact rpow_le_rpow (mul_pos one_half_pos hx.1).le (by linarith) hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ 1 / 2 * x ≤ x + R
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
obtain ⟨c, hc, hc'⟩ := hf.exists_pos
[GOAL]
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
hc' : IsBigOWith c atTop ↑f fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
simp only [IsBigO, IsBigOWith, eventually_atTop] at hc' ⊢
[GOAL]
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
hc' : ∃ a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ ∃ c a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
[PROOFSTEP]
obtain ⟨d, hd⟩ := hc'
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ ∃ c a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
[PROOFSTEP]
refine' ⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => _⟩⟩
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : x ≥ max (1 + max 0 (-2 * R)) (d - R)
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [ge_iff_le, max_le_iff] at hx
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
have hx' : max 0 (-2 * R) < x := by linarith
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
⊢ max 0 (-2 * R) < x
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : max 0 (-2 * R) < x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [max_lt_iff] at hx'
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [norm_norm,
  ContinuousMap.norm_le _ (mul_nonneg (mul_nonneg hc.le <| rpow_nonneg_of_nonneg one_half_pos.le _) (norm_nonneg _))]
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖↑(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
refine' fun y => (hd y.1 (by linarith [hx.1, y.2.1])).trans _
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
⊢ ↑y ≥ d
[PROOFSTEP]
linarith [hx.1, y.2.1]
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
⊢ c * ‖|↑y| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
have A : ∀ x : ℝ, 0 ≤ |x| ^ (-b) := fun x => by positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x✝ : ℝ
hx : 1 + max 0 (-2 * R) ≤ x✝ ∧ d - R ≤ x✝
hx' : 0 < x✝ ∧ -2 * R < x✝
y : ↑(Icc (x✝ + R) (x✝ + S))
x : ℝ
⊢ 0 ≤ |x| ^ (-b)
[PROOFSTEP]
positivity
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ c * ‖|↑y| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [mul_assoc, mul_le_mul_left hc, norm_of_nonneg (A _), norm_of_nonneg (A _)]
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
[PROOFSTEP]
convert claim x (by linarith only [hx.1]) y.1 y.2.1
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ max 0 (-2 * R) < x
[PROOFSTEP]
linarith only [hx.1]
[GOAL]
case h.e'_3.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| = ↑y
[PROOFSTEP]
apply abs_of_nonneg
[GOAL]
case h.e'_3.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ 0 ≤ ↑y
[PROOFSTEP]
linarith [y.2.1]
[GOAL]
case h.e'_4.h.e'_6.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx'.1
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
have h1 : IsBigO atTop (f.comp (ContinuousMap.mk _ continuous_neg)) fun x : ℝ => |x| ^ (-b) :=
  by
  convert hf.comp_tendsto tendsto_neg_atTop_atBot using 1
  ext1 x; simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
⊢ ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
convert hf.comp_tendsto tendsto_neg_atTop_atBot using 1
[GOAL]
case h.e'_8
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => |x| ^ (-b)) = (fun x => |x| ^ (-b)) ∘ Neg.neg
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_8.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S x : ℝ
⊢ |x| ^ (-b) = ((fun x => |x| ^ (-b)) ∘ Neg.neg) x
[PROOFSTEP]
simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
have h2 := (isBigO_norm_Icc_restrict_atTop hb h1 (-S) (-R)).comp_tendsto tendsto_neg_atBot_atTop
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
have : (fun x : ℝ => |x| ^ (-b)) ∘ Neg.neg = fun x : ℝ => |x| ^ (-b) := by ext1 x;
  simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
⊢ (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
[PROOFSTEP]
ext1 x
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
x : ℝ
⊢ ((fun x => |x| ^ (-b)) ∘ Neg.neg) x = |x| ^ (-b)
[PROOFSTEP]
simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
rw [this] at h2
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
refine' (isBigO_of_le _ fun x => _).trans h2
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤
    ‖((fun x =>
            ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
          Neg.neg)
        x‖
[PROOFSTEP]
rw [norm_norm, Function.comp_apply, norm_norm, ContinuousMap.norm_le _ (norm_nonneg _)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖↑(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖↑(ContinuousMap.restrict (Icc (x✝ + R) (x✝ + S)) f) { val := x, property := hx }‖ ≤
    ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖
[PROOFSTEP]
rw [ContinuousMap.restrict_apply_mk]
[GOAL]
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖↑f x‖ ≤ ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖
[PROOFSTEP]
refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, _⟩)
[GOAL]
case mk.refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖↑f x‖ =
    ‖↑(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a)))
        { val := -x, property := ?mk.refine'_2 }‖
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
[PROOFSTEP]
rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, neg_neg]
[GOAL]
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
[PROOFSTEP]
exact ⟨by linarith [hx.2], by linarith [hx.1]⟩
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x✝ + -S ≤ -x
[PROOFSTEP]
linarith [hx.2]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ≤ -x✝ + -R
[PROOFSTEP]
linarith [hx.1]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
obtain ⟨r, hr⟩ := K.isCompact.bounded.subset_ball 0
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Metric.closedBall 0 r
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
rw [closedBall_eq_Icc, zero_add, zero_sub] at hr
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
have : ∀ x : ℝ, ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ :=
  by
  intro x
  rw [ContinuousMap.norm_le _ (norm_nonneg _)]
  rintro ⟨y, hy⟩
  refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, _⟩)
  · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
  · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
intro x
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x : ℝ
⊢ ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
rw [ContinuousMap.norm_le _ (norm_nonneg _)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x : ℝ
⊢ ∀ (x_1 : ↑↑K),
    ‖↑(ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖↑(ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))) { val := y, property := hy }‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, _⟩)
[GOAL]
case mk.refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖↑(ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))) { val := y, property := hy }‖ =
    ‖↑(ContinuousMap.restrict (Icc (x - r) (x + r)) f) { val := y + x, property := ?mk.refine'_2 }‖
[PROOFSTEP]
simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
[GOAL]
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ y + x ∈ Icc (x - r) (x + r)
[PROOFSTEP]
exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ x - r ≤ y + x
[PROOFSTEP]
linarith [(hr hy).1]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ y + x ≤ x + r
[PROOFSTEP]
linarith [(hr hy).2]
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
simp_rw [cocompact_eq, isBigO_sup] at hf ⊢
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ((fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atBot] fun x =>
      |x| ^ (-b)) ∧
    (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atTop] fun x =>
      |x| ^ (-b)
[PROOFSTEP]
constructor
[GOAL]
case intro.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atBot] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
refine' (isBigO_of_le atBot _).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
[GOAL]
case intro.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
[PROOFSTEP]
simp_rw [norm_norm]
[GOAL]
case intro.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
[PROOFSTEP]
exact this
[GOAL]
case intro.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atTop] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
refine' (isBigO_of_le atTop _).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)
[GOAL]
case intro.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
[PROOFSTEP]
simp_rw [norm_norm]
[GOAL]
case intro.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
[PROOFSTEP]
exact this
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), ↑g ↑n
[PROOFSTEP]
simp_rw [← hfg]
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
rw [Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay f.continuous one_lt_two (f.isBigO_cocompact_rpow (-2))]
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ 𝓕 ↑f =O[cocompact ℝ] fun x => |x| ^ (-2)
[PROOFSTEP]
rw [hfg]
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ ↑g =O[cocompact ℝ] fun x => |x| ^ (-2)
[PROOFSTEP]
exact g.isBigO_cocompact_rpow (-2)


[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ Comp.mk (tfst f' <$> tfst f x) = tfst (Comp.mk ∘ map f' ∘ f) x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ bitraverse (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (Comp.mk ∘ map f' ∘ f) x
[PROOFSTEP]
simp only [Function.comp, tfst, map_pure, Pure.pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tfst f <$> tsnd f' x) = bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
    bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
[PROOFSTEP]
simp only [Function.comp, map_pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tsnd f' <$> tfst f x) = bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
    bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
[PROOFSTEP]
simp only [Function.comp, map_pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Comp.mk ∘ map g' ∘ g) x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (Comp.mk ∘ map g' ∘ g) x
[PROOFSTEP]
simp only [Function.comp, map_pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (fun x => Comp.mk (pure (pure x))) (fun x => Comp.mk (g' <$> g x)) x =
    tsnd (fun x => Comp.mk (g' <$> g x)) x
[PROOFSTEP]
rfl
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α α' β : Type u
f : α → α'
x : t α β
⊢ tfst (pure ∘ f) x = pure (fst f x)
[PROOFSTEP]
apply bitraverse_eq_bimap_id
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β β' : Type u
f : β → β'
x : t α β
⊢ tsnd (pure ∘ f) x = pure (snd f x)
[PROOFSTEP]
apply bitraverse_eq_bimap_id


[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : (fun {α} => app η α) = fun {α} => app η' α
⊢ η = η'
[PROOFSTEP]
cases η
[GOAL]
case mk
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η' : ApplicativeTransformation F G
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ :
  ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (Seq.seq x fun x => y) = Seq.seq (app✝ (α → β) x) fun x => app✝ α y
h :
  (fun {α} => app { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } α) =
    fun {α} => app η' α
⊢ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } = η'
[PROOFSTEP]
cases η'
[GOAL]
case mk.mk
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
app✝¹ : (α : Type u) → F α → G α
preserves_pure'✝¹ : ∀ {α : Type u} (x : α), app✝¹ α (pure x) = pure x
preserves_seq'✝¹ :
  ∀ {α β : Type u} (x : F (α → β)) (y : F α),
    app✝¹ β (Seq.seq x fun x => y) = Seq.seq (app✝¹ (α → β) x) fun x => app✝¹ α y
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ :
  ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (Seq.seq x fun x => y) = Seq.seq (app✝ (α → β) x) fun x => app✝ α y
h :
  (fun {α} => app { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } α) =
    fun {α} => app { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } α
⊢ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } =
    { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ η = η'
[PROOFSTEP]
apply coe_inj
[GOAL]
case h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ (fun {α} => app η α) = fun {α} => app η' α
[PROOFSTEP]
ext1 α
[GOAL]
case h.h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
α : Type u
⊢ app η α = app η' α
[PROOFSTEP]
exact funext (h α)
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ (fun {α} => app η α) (x <$> y) = x <$> (fun {α} => app η α) y
[PROOFSTEP]
rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
⊢ (fun {α} => app η α) ∘ Functor.map x = Functor.map x ∘ fun {α} => app η α
[PROOFSTEP]
ext y
[GOAL]
case h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} => app η α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => app η α) y
[PROOFSTEP]
exact preserves_map η x y
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
⊢ ∀ {α : Type u} (x : α), (fun α => id) α (pure x) = pure x
[PROOFSTEP]
simp
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ (fun α => id) β✝ (Seq.seq x fun x => y) = Seq.seq ((fun α => id) (α✝ → β✝) x) fun x => (fun α => id) α✝ y
[PROOFSTEP]
simp
[GOAL]
F : Type u → Type v
inst✝⁵ : Applicative F
inst✝⁴ : LawfulApplicative F
G : Type u → Type w
inst✝³ : Applicative G
inst✝² : LawfulApplicative G
H : Type u → Type s
inst✝¹ : Applicative H
inst✝ : LawfulApplicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ : Type u
x : α✝
⊢ (fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) α✝ (pure x) = pure x
[PROOFSTEP]
simp only [preserves_pure]
[GOAL]
F : Type u → Type v
inst✝⁵ : Applicative F
inst✝⁴ : LawfulApplicative F
G : Type u → Type w
inst✝³ : Applicative G
inst✝² : LawfulApplicative G
H : Type u → Type s
inst✝¹ : Applicative H
inst✝ : LawfulApplicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ (fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) β✝ (Seq.seq x fun x => y) =
    Seq.seq ((fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) (α✝ → β✝) x) fun x =>
      (fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) α✝ y
[PROOFSTEP]
simp only [preserves_seq]
[GOAL]
⊢ LawfulTraversable Id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
⊢ ∀ {α β : Type ?u.11560}, mapConst = map ∘ const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
⊢ ∀ {α : Type ?u.11560} (x : Id α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
⊢ ∀ {α β γ : Type ?u.11560} (g : α → β) (h : β → γ) (x : Id α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_4
⊢ ∀ {α : Type ?u.11560} (x : Id α), traverse pure x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_5
⊢ ∀ {F G : Type ?u.11560 → Type ?u.11560} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α β γ : Type ?u.11560} (f : β → F γ) (g : α → G β) (x : Id α),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)
[PROOFSTEP]
intros
[GOAL]
case refine'_6
⊢ ∀ {α β : Type ?u.11560} (f : α → β) (x : Id α), traverse (pure ∘ f) x = id.mk (f <$> x)
[PROOFSTEP]
intros
[GOAL]
case refine'_7
⊢ ∀ {F G : Type ?u.11560 → Type ?u.11560} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type ?u.11560} (f : α → F β) (x : Id α),
    (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =
      traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.11560
⊢ mapConst = map ∘ const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α✝ : Type ?u.11560
x✝ : Id α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.11560
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Id α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α✝ : Type ?u.11560
x✝ : Id α✝
⊢ traverse pure x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
F✝ G✝ : Type ?u.11560 → Type ?u.11560
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type ?u.11560
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : Id α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α✝ β✝ : Type ?u.11560
f✝ : α✝ → β✝
x✝ : Id α✝
⊢ traverse (pure ∘ f✝) x✝ = id.mk (f✝ <$> x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
F✝ G✝ : Type ?u.11560 → Type ?u.11560
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type ?u.11560
f✝ : α✝ → F✝ β✝
x✝ : Id α✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (traverse f✝ x✝) =
    traverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝) x✝
[PROOFSTEP]
rfl


[GOAL]
α : Type ?u.3
⊢ (fun {α β} e => ↑(uniqueCongr e)) (Equiv.refl α) = id
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {α β γ : Type ?u.3} (k : α ≃ β) (h : β ≃ γ),
    (fun {α β} e => ↑(uniqueCongr e)) (k.trans h) =
      (fun {α β} e => ↑(uniqueCongr e)) h ∘ (fun {α β} e => ↑(uniqueCongr e)) k
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.3738
⊢ (fun {α β} e p => (e.symm.trans p).trans e) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h.H
α : Type ?u.3738
x✝¹ : Perm α
x✝ : α
⊢ ↑((fun {α β} e p => (e.symm.trans p).trans e) (Equiv.refl α) x✝¹) x✝ = ↑(id x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
α✝ β✝ γ✝ : Type ?u.3738
x✝¹ : α✝ ≃ β✝
x✝ : β✝ ≃ γ✝
⊢ (fun {α β} e p => (e.symm.trans p).trans e) (x✝¹.trans x✝) =
    (fun {α β} e p => (e.symm.trans p).trans e) x✝ ∘ (fun {α β} e p => (e.symm.trans p).trans e) x✝¹
[PROOFSTEP]
ext
[GOAL]
case h.H
α✝ β✝ γ✝ : Type ?u.3738
x✝³ : α✝ ≃ β✝
x✝² : β✝ ≃ γ✝
x✝¹ : Perm α✝
x✝ : γ✝
⊢ ↑((fun {α β} e p => (e.symm.trans p).trans e) (x✝³.trans x✝²) x✝¹) x✝ =
    ↑(((fun {α β} e p => (e.symm.trans p).trans e) x✝² ∘ (fun {α β} e p => (e.symm.trans p).trans e) x✝³) x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.6374
⊢ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type ?u.6374
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (Equiv.refl α) x✝ ↔ a✝ ∈ id x✝
[PROOFSTEP]
simp
[GOAL]
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
⊢ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (k.trans h) =
    (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) h ∘ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) k
[PROOFSTEP]
ext _ a
[GOAL]
case h.a
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ a ∈ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (k.trans h) x✝ ↔
    a ∈
      ((fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) h ∘
          (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) k)
        x✝
[PROOFSTEP]
simp
[GOAL]
case h.a
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ (∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a) ↔ ↑k.symm (↑h.symm a) ∈ x✝
[PROOFSTEP]
constructor
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ (∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a) → ↑k.symm (↑h.symm a) ∈ x✝
[PROOFSTEP]
intro h'
[GOAL]
case h.a.mpr
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ ↑k.symm (↑h.symm a) ∈ x✝ → ∃ a_2, a_2 ∈ x✝ ∧ ↑h (↑k a_2) = a
[PROOFSTEP]
intro h'
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
h' : ∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a
⊢ ↑k.symm (↑h.symm a) ∈ x✝
[PROOFSTEP]
let ⟨a, ha₁, ha₂⟩ := h'
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
h' : ∃ a, a ∈ x✝ ∧ ↑h (↑k a) = a✝
a : α✝
ha₁ : a ∈ x✝
ha₂ : ↑h (↑k a) = a✝
⊢ ↑k.symm (↑h.symm a✝) ∈ x✝
[PROOFSTEP]
rw [← ha₂]
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
h' : ∃ a, a ∈ x✝ ∧ ↑h (↑k a) = a✝
a : α✝
ha₁ : a ∈ x✝
ha₂ : ↑h (↑k a) = a✝
⊢ ↑k.symm (↑h.symm (↑h (↑k a))) ∈ x✝
[PROOFSTEP]
simp
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
h' : ∃ a, a ∈ x✝ ∧ ↑h (↑k a) = a✝
a : α✝
ha₁ : a ∈ x✝
ha₂ : ↑h (↑k a) = a✝
⊢ a ∈ x✝
[PROOFSTEP]
apply ha₁
[GOAL]
case h.a.mpr
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
h' : ↑k.symm (↑h.symm a) ∈ x✝
⊢ ∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a
[PROOFSTEP]
exists (Equiv.symm k) ((Equiv.symm h) a)
[GOAL]
case h.a.mpr
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
h' : ↑k.symm (↑h.symm a) ∈ x✝
⊢ ↑k.symm (↑h.symm a) ∈ x✝ ∧ ↑h (↑k (↑k.symm (↑h.symm a))) = a
[PROOFSTEP]
simp [h']
[GOAL]
α : Type ?u.9577
⊢ (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h
α : Type ?u.9577
x✝ : Fintype α
⊢ (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) (Equiv.refl α) x✝ = id x✝
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {α β γ : Type ?u.9577} (k : α ≃ β) (h : β ≃ γ),
    (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) (k.trans h) =
      (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) h ∘
        (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) k
[PROOFSTEP]
simp


[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f✝ : β → γ
α✝ β✝ : Type u
f : Id (α✝ → β✝)
x : Id α✝
⊢ pure (Seq.seq f fun x_1 => x) = Seq.seq (pure f) fun x_1 => pure x
[PROOFSTEP]
simp only [map_pure, seq_pure]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f✝ : β → γ
α✝ β✝ : Type u
f : Id (α✝ → β✝)
x : Id α✝
⊢ pure (Seq.seq f fun x_1 => x) = pure (f x)
[PROOFSTEP]
rfl
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
⊢ map f <$> traverse g x = traverse (map f ∘ g) x
[PROOFSTEP]
rw [map_eq_traverse_id f]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
⊢ traverse (pure ∘ f) <$> traverse g x = traverse (map f ∘ g) x
[PROOFSTEP]
refine' (comp_traverse (pure ∘ f) g x).symm.trans _
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x
[PROOFSTEP]
congr
[GOAL]
case h.e_4.h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
⊢ Comp.instApplicativeComp = inst✝³
[PROOFSTEP]
apply Comp.applicative_comp_id
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h : β → G γ
f✝ : β → γ
x✝ : t β
f : β → F γ
g : α → β
x : t α
⊢ traverse f (g <$> x) = traverse (f ∘ g) x
[PROOFSTEP]
rw [@map_eq_traverse_id t _ _ _ _ g]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h : β → G γ
f✝ : β → γ
x✝ : t β
f : β → F γ
g : α → β
x : t α
⊢ traverse f (traverse (pure ∘ g) x) = traverse (f ∘ g) x
[PROOFSTEP]
refine' (comp_traverse (G := Id) f (pure ∘ g) x).symm.trans _
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h : β → G γ
f✝ : β → γ
x✝ : t β
f : β → F γ
g : α → β
x : t α
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x
[PROOFSTEP]
congr
[GOAL]
case h.e_4.h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h : β → G γ
f✝ : β → γ
x✝ : t β
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝³
[PROOFSTEP]
apply Comp.applicative_id_comp
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
⊢ traverse pure x = pure x
[PROOFSTEP]
have : traverse pure x = pure (traverse (m := Id) pure x) := (naturality (PureTransformation F) pure x).symm
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
this : traverse pure x = pure (traverse pure x)
⊢ traverse pure x = pure x
[PROOFSTEP]
rwa [id_traverse] at this
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t α
⊢ sequence (pure <$> x) = pure x
[PROOFSTEP]
simp [sequence, traverse_map, id_traverse]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t (F (G α))
⊢ sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)
[PROOFSTEP]
simp [sequence, traverse_map]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)
[PROOFSTEP]
rw [← comp_traverse]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x
[PROOFSTEP]
simp [map_id]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
η : ApplicativeTransformation F G
x : t (F α)
⊢ (fun {α} => ApplicativeTransformation.app η α) (sequence x) =
    sequence ((fun {α} => ApplicativeTransformation.app η α) <$> x)
[PROOFSTEP]
simp [sequence, naturality, traverse_map]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x : t β
⊢ traverse pure = pure
[PROOFSTEP]
ext
[GOAL]
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x : t β
x✝ : t α
⊢ traverse pure x✝ = pure x✝
[PROOFSTEP]
exact id_traverse _
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h✝ : β → G γ
f : β → γ
x : t β
g : α → F β
h : β → G γ
⊢ traverse (Comp.mk ∘ map h ∘ g) = Comp.mk ∘ map (traverse h) ∘ traverse g
[PROOFSTEP]
ext
[GOAL]
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h✝ : β → G γ
f : β → γ
x : t β
g : α → F β
h : β → G γ
x✝ : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) x✝
[PROOFSTEP]
exact comp_traverse _ _ _
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f✝ : β → γ
x : t β
f : β → γ
⊢ traverse (pure ∘ f) = pure ∘ map f
[PROOFSTEP]
ext
[GOAL]
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f✝ : β → γ
x : t β
f : β → γ
x✝ : t β
⊢ traverse (pure ∘ f) x✝ = (pure ∘ map f) x✝
[PROOFSTEP]
exact traverse_eq_map_id _ _
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h✝ : β → G γ
f : β → γ
x : t β
g : α → β
h : β → G γ
⊢ traverse (h ∘ g) = traverse h ∘ map g
[PROOFSTEP]
ext
[GOAL]
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h✝ : β → G γ
f : β → γ
x : t β
g : α → β
h : β → G γ
x✝ : t α
⊢ traverse (h ∘ g) x✝ = (traverse h ∘ map g) x✝
[PROOFSTEP]
rw [comp_apply, traverse_map]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h✝ : β → G γ
f : β → γ
x : t β
g : α → G β
h : β → γ
⊢ traverse (map h ∘ g) = map (map h) ∘ traverse g
[PROOFSTEP]
ext
[GOAL]
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g✝ : α → F β
h✝ : β → G γ
f : β → γ
x : t β
g : α → G β
h : β → γ
x✝ : t α
⊢ traverse (map h ∘ g) x✝ = (map (map h) ∘ traverse g) x✝
[PROOFSTEP]
rw [comp_apply, map_traverse]
[GOAL]
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f✝ : β → γ
x : t β
η : ApplicativeTransformation F G
f : α → F β
⊢ traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) =
    (fun {α} => ApplicativeTransformation.app η α) ∘ traverse f
[PROOFSTEP]
ext
[GOAL]
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f✝ : β → γ
x : t β
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x✝ =
    ((fun {α} => ApplicativeTransformation.app η α) ∘ traverse f) x✝
[PROOFSTEP]
rw [comp_apply, naturality]