mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc)

Tactic:
simp_rw [← sum_sfiniteSeq μa, ← sum_sfiniteSeq μc, map_sum hf.aemeasurable,
    map_sum hg.aemeasurable, prod_sum, map_sum (hf.prodMap hg).aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  rw [map_apply (hf.prodMap hg) (hs.prod ht), map_apply hf hs, map_apply hg ht]
  exact prod_prod (f ⁻¹' s) (g ⁻¹' t)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc (Prod.mk a ⁻¹' (fun p ↦ (f p.1, g p.1 p.2)) ⁻¹' s) = (map (g a) μc) (Prod.mk (f a) ⁻¹' s)

Tactic:
map_apply hgm.of_uncurry_left (measurable_prodMk_left hs),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc (Prod.mk a ⁻¹' (fun p ↦ (f p.1, g p.1 p.2)) ⁻¹' s) = μc (g a ⁻¹' Prod.mk (f a) ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s

Tactic:
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul' r f hr]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ (map (⇑F) μ) K < ∞

Tactic:
rw [F.map_apply K]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ μ (⇑F ⁻¹' K) < ∞
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
have :=
    (quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)
  rw [μ.inv_inv] at this
  have :=
    (quasiMeasurePreserving_inv_of_right_invariant μ).comp
      (this.comp (quasiMeasurePreserving_inv_of_right_invariant μ))
  simp_rw [Function.comp_def, mul_inv_rev, inv_inv] at this
  exact this

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (-f) μ

Tactic:
by simpa [hasFiniteIntegral_iff_enorm] using hfi

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ

Tactic:
by simpa [hasFiniteIntegral_iff_enorm] using hfi

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (fun a ↦ ‖f a‖) μ

Tactic:
by simpa [hasFiniteIntegral_iff_enorm] using hfi

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ

Tactic:
intro g h_mea_g h_mono_g h_ind
    have : Monotone fun n a => f a * g n a := fun m n hmn x => by dsimp; grw [h_mono_g hmn x]
    simp [lintegral_iSup, ENNReal.mul_iSup, h_mf.fun_mul (h_mea_g _), *]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (f' * g) x = (f * g) x

Tactic:
simp only [f', hx, Pi.mul_apply]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ≤ x ↔ x = 0 ∨ 1 ≤ x

Tactic:
by
  rw [sqrt_le_iff, ← sub_nonneg (a := x ^ 2), sq, ← mul_sub_one]
  grind [mul_nonneg_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), (f * i) a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: a : ℕ
⊢ √↑a < ↑a.sqrt + 1

Tactic:
sqrt_lt (by simp)

Goal state after:
a : ℕ
⊢ ↑a < (↑a.sqrt + 1) ^ 2

a : ℕ
⊢ 0 ≤ ↑a.sqrt + 1
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2

Tactic:
rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2

Tactic:
rw [← sq_norm_sub_sq_re, sub_sub_cancel]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (f' * g) x = (f * g) x

Tactic:
simp only [f', hx, Pi.mul_apply]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im } = { re := a.re, im := -a.im } + { re := b.re, im := -b.im }

Tactic:
by ext <;> simp [add_comm]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
← @preimage_equivRealProd_prod s₁ t₁

Goal state after:
s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ μ ∗ₘ (s • ν) = s • μ ∗ₘ ν

Tactic:
unfold mconv
  rw [Measure.prod_smul_right, Measure.map_smul]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : ‖(id V) x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖

Tactic:
id_apply,

Goal state after:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : ‖x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I) = 2 * ↑(im z) * I

Tactic:
add_sub_sub_cancel,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(im z) * I + ↑(im z) * I = 2 * ↑(im z) * I
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) + (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) =
    2 • (↑(ℜ a) * ↑(ℜ a) + ↑(ℑ a) * ↑(ℑ a))

Tactic:
simp [mul_add, add_mul, smul_smul, mul_smul_comm,
        smul_mul_assoc]
      abel

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsEmbedding (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
isEmbedding_iff

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (e.source.domRestrict ↑e.toPartialEquiv) ∧ Injective (e.source.domRestrict ↑e.toPartialEquiv)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_left

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun x ↦ f (a, x)) =O[l'] fun x ↦ g (a, x)

Tactic:
by
  simp only [isBigO_iff, eventually_iff, mem_prod_iff]
  rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
  exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
⊢ ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε

Tactic:
exists max n i

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
⊢ ∀ j ≥ max n i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
c : S
hc : c ≠ 0
f : α → S
l : Filter α
⊢ IsBigOWith ‖c‖⁻¹ l f fun x ↦ c * f x

Tactic:
by
  simp [IsBigOWith, inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr hc)]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
⊢ abv ((∑ k ∈ range K, f k) * ∑ k ∈ range K, g k - ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε

Tactic:
have two_mul_two : (4 : α) = 2 * 2 := by norm_num

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
⊢ abv ((∑ k ∈ range K, f k) * ∑ k ∈ range K, g k - ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : IsBigOWith c l k₁ k₂
h₂ : IsBigOWith c' l f' g'
⊢ IsBigOWith (c * c') l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
by
  simp only [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with _ hx₁ hx₂
  apply le_trans (norm_smul_le _ _)
  convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
  rw [norm_smul, mul_mul_mul_comm]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z * z ^ m / ↑(m.factorial * m.succ)‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
Nat.cast_mul,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z * z ^ m / (↑m.factorial * ↑m.succ)‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z / ↑m.succ * (z ^ m / ↑m.factorial)‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
Complex.norm_mul,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z / ↑m.succ‖ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑(m.choose I * I.factorial * (m - I).factorial))⁻¹ =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
Nat.cast_mul,

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑(m.choose I * I.factorial) * ↑(m - I).factorial)⁻¹ =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑(m.choose I * I.factorial) * ↑(m - I).factorial)⁻¹ =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
Nat.cast_mul,

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑(m.choose I) * ↑I.factorial * ↑(m - I).factorial)⁻¹ =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h₁ : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
h₂ : ∃ i_1 ∈ i :: L, f i_1 =o[l] g i_1
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (i :: L)).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) (i :: L)).prod

Tactic:
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢
    cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
⊢ cexp (↑0 * x) = cexp x ^ 0

Tactic:
by rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cexp x + cexp (-x) - (cexp x - cexp (-x)) = 2 * cexp (-x)

Tactic:
add_sub_sub_cancel,

Goal state after:
x : ℂ
⊢ cexp (-x) + cexp (-x) = 2 * cexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: z : ℂ
⊢ cos z = cos ↑z.re * cosh ↑z.im - sin ↑z.re * sinh ↑z.im * I

Tactic:
by
  convert! cos_add_mul_I z.re z.im; exact (re_add_im z).symm

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
Complex.norm_mul,

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ range j with n ≤ x_1, ‖x ^ n‖ * ‖x ^ (x_1 - n) / ↑x_1.factorial‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = 2 * cos x ^ 2 - 1

Tactic:
rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x), ← sub_add, sub_add_eq_add_sub,
    two_mul]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
Complex.norm_mul,

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ Ico n j, ‖x ^ n‖ * ‖x ^ (x_1 - n) / ↑x_1.factorial‖ ≤
    ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-↑(x / 2) * I) * (1 - cexp (↑x * I)) * I‖

Tactic:
Complex.norm_mul,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-↑(x / 2) * I) * (1 - cexp (↑x * I))‖ * ‖I‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-↑(x / 2) * I) * (1 - cexp (↑x * I))‖

Tactic:
Complex.norm_mul,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-↑(x / 2) * I)‖ * ‖1 - cexp (↑x * I)‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: z : ℂ
⊢ ‖cexp ↑z.re * (cos ↑z.im + sin ↑z.im * I)‖ = Real.exp z.re

Tactic:
Complex.norm_mul,

Goal state after:
z : ℂ
⊢ ‖cexp ↑z.re‖ * ‖cos ↑z.im + sin ↑z.im * I‖ = Real.exp z.re
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k) * a < 0

Tactic:
exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : -[m+1] ≠ 0
⊢ a ^ -[m+1] = b ^ -[m+1] ↔ a = b ∨ a = -b ∧ Even -[m+1]

Tactic:
simp only [← neg_ofNat_succ, ne_eq, neg_eq_zero, Nat.cast_eq_zero, zpow_neg, zpow_natCast,
      inv_inj, even_neg, Int.even_coe_nat] at *

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ¬m.succ = 0
⊢ a ^ m.succ = b ^ m.succ ↔ a = b ∨ a = -b ∧ Even m.succ
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
l : Filter ι
ε : ι → 𝕜
f : ι → E
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
⊢ Tendsto (ε • f) l (𝓝 0)

Tactic:
rw [← isLittleO_one_iff 𝕜] at hε ⊢
  simpa using! IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
have H : ∀ d e, 0 < d → Tendsto (fun x : ℝ => x ^ n / (d * exp x + e)) atTop (𝓝 0) := by
    intro b' c' h
    convert! (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
    ext x
    simp
  rcases lt_or_gt_of_ne hb with h | h
  · exact H b c h
  · convert! (H (-b) (-c) (neg_pos.mpr h)).neg using 1
    · ext x
      field_simp
      rw [← neg_add (b * exp x) c, div_neg, neg_neg]
    · rw [neg_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Subtype.val '' Set.Iio (expOrderIso a) = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)

Tactic:
image_subtype_val_Ioi_Iio,

Goal state after:
a : ℝ
⊢ Set.Ioo 0 ↑(expOrderIso a) = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)