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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

Tactic:
← lintegral_prod_swap,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (z : β × α), f z.swap ∂(ν.restrict t).prod (μ.restrict s) = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
y : G
yins : y ∈ s
hy : f y = (fun x ↦ x * f g) x✝
⊢ f (y * g⁻¹) = x✝

Tactic:
simp [hy]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst✝⁴] U
hne : U.Nonempty
h : μ U = 0
⊢ μ K ≤ 0

Tactic:
← hU.interior_eq

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst✝⁴] U
hne : (interior U).Nonempty
h : μ U = 0
⊢ μ K ≤ 0
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst✝⁴] U
h'U : U.Nonempty
h : μ U ≠ ∞
K : Set G
hK : IsCompact K
⊢ μ K < ∞

Tactic:
← hU.interior_eq

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst✝⁴] U
h'U : (interior U).Nonempty
h : μ U ≠ ∞
K : Set G
hK : IsCompact K
⊢ μ K < ∞
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b c : R
⊢ discrim (-a) (-b) (-c) = discrim a b c

Tactic:
by
  simp [discrim]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ENNReal.ofReal (ε / 2) * ENNReal.ofReal (∑' (n : ℕ), 2⁻¹ ^ n) ≤ ENNReal.ofReal ε

pp: case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)

Tactic:
inv_eq_one_div,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ENNReal.ofReal (ε / 2) * ENNReal.ofReal (∑' (n : ℕ), (1 / 2) ^ n) ≤ ENNReal.ofReal ε

case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N)⁻¹ < δ
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f n x) < δ

Tactic:
eventually_atTop

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N)⁻¹ < δ
⊢ ∃ a, ∀ (b : ι), a ≤ b → ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f b x) < δ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

Tactic:
have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]

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

Goal state before:
pp: ⊢ 1 < √2

Tactic:
rw [← Real.sqrt_one]; gcongr; simp

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

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

Tactic:
sub_sub_cancel

Goal state after:
z : ℂ
⊢ z.re ^ 2 = z.re ^ 2
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
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'

Tactic:
by
      rw [withDensity_congr_ae hf.ae_eq_mk]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ |(↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j).re| + |(↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j).im| < ε

Tactic:
simpa using! add_lt_add H₁ H₂

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

Goal state before:
pp: ⊢ I⁻¹ = -I

Tactic:
inv_eq_one_div,

Goal state after:
⊢ 1 / I = -I
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ f z.1

Tactic:
lintegral_prod _ hφ.aemeasurable,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν ∂μ.withDensity f = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ f z.1
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ g z.2

Tactic:
lintegral_prod _ hφ.aemeasurable,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ g z.2
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ

Tactic:
conv in (∫⁻ _, _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
by
  exact funext <| e.symm_apply_apply

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ re 1 = 1

Tactic:
rw [← ofReal_one, ofReal_re]

Goal state after:
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 * ↑(re z)

Tactic:
add_add_sub_cancel,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(re z) = 2 * ↑(re z)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x : ℝ
h : HasSum (fun x ↦ ↑(f x)) (↑x) L
⊢ HasSum f x L

Tactic:
simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.hasSum h

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
rw [e.eventually_nhdsWithin _ hx]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝[s] x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Contravariant { x // 0 ≤ x } K (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2

Tactic:
by
    rintro ⟨x, hx⟩ y z hyz
    dsimp at *
    rw [RCLike.le_iff_re_im, map_zero, map_zero, eq_comm] at hx
    obtain ⟨r, rfl⟩ := ((is_real_TFAE x).out 3 1).1 hx.2
    simp only [RCLike.lt_iff_re_im (K := K), mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero,
      mul_im, add_zero, mul_eq_mul_left_iff] at hyz ⊢
    refine ⟨lt_of_mul_lt_mul_of_nonneg_left hyz.1 <| by simpa using hx, hyz.2.resolve_right ?_⟩
    rintro rfl
    simp at hyz

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
subst h''; exact h.star_add

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

Goal state before:
pp: case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
⊢ ‖f'' x‖ ≤ 0

Tactic:
have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
      ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
        inf_le_left

Goal state after:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ ‖f'' x‖ ≤ 0
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:

Tactic:
(fun H => A i H + ∑ j ∈ s, A j H)
      =o[l] fun H => ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖ :=
          (hAB i (by simp)).add_add (h (fun j hj => hAB j (by simp [hj])))
    _ =ᶠ[l] fun H => ‖B i H‖ + ∑ j ∈ s, ‖B j H‖ := by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : IsBigOWith C (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
⊢ IsBigOWith C l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
by
  simp only [IsBigOWith_def] at *
  obtain ⟨s₁, hs₁, s₂, hs₂, hbound⟩ := Filter.eventually_prod_iff.mp hAB
  filter_upwards [hs₂] with H hH
  calc
    ‖∑ j ∈ i H, A j H‖ ≤ ∑ j ∈ i H, ‖A j H‖ := norm_sum_le ..
    _ ≤ ∑ j ∈ i H, C * ‖B j H‖ :=
        Finset.sum_le_sum fun j _ => hbound (Filter.eventually_top.mp hs₁ j) hH
    _ = C * ∑ j ∈ i H, ‖B j H‖ := (Finset.mul_sum ..).symm
    _ = C * ‖∑ j ∈ i H, ‖B j H‖‖ := by
        congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
f : α → E'
g : α → 𝕜
l : Filter α
h : f =o[l] g
⊢ Tendsto (fun x ↦ (g x)⁻¹ • f x) l (𝓝 0)

Tactic:
by
  simpa only [div_eq_inv_mul, ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero] using
    h.norm_norm.tendsto_div_nhds_zero

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

Goal state before:
pp: case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ ∀ᶠ (x : α) in l, g x = 0 → f x = 0

Tactic:
apply (Filter.Tendsto.eventually_ge_atTop h 1).mono

Goal state after:
case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ ∀ (x : α), 1 ≤ g x / f x → g x = 0 → f x = 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case a
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
convert! Tendsto.comp tendsto_inv_atTop_zero h

Goal state after:
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
x✝ : α
⊢ f x✝ / g x✝ = ((fun r ↦ r⁻¹) ∘ fun x ↦ g x / f x) x✝
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
add_add_sub_cancel,

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

Goal state before:
pp: x : ℂ
⊢ sin (x * I) = sinh x * I

Tactic:
have h : I * sin (x * I) = -sinh x := by
    rw [mul_comm, ← sinh_mul_I]
    ring_nf
    simp

Goal state after:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ sin x / cos x * cos x = sin x

Tactic:
div_mul_cancel₀ _ hx

Goal state after:
x : ℂ
hx : cos x ≠ 0
⊢ sin x = sin x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Tactic:
change ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ _

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

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
⊢ sin x / cos x * cos x = sin x

Tactic:
div_mul_cancel₀ _ hx

Goal state after:
x : ℝ
hx : cos x ≠ 0
⊢ sin x = sin x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cexp ↑x + cexp (-↑x)).re = (cexp ↑x).re + (cexp (-↑x)).re

Tactic:
Complex.add_re

Goal state after:
x : ℝ
⊢ (cexp ↑x).re + (cexp (-↑x)).re = (cexp ↑x).re + (cexp (-↑x)).re
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ m ∈ range 3, x ^ m / ↑m.factorial + x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤ 1 + x + x ^ 2

Tactic:
show 3 = 1 + 1 + 1 from rfl

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ m ∈ range (1 + 1 + 1), x ^ m / ↑m.factorial +
      x ^ (1 + 1 + 1) * (↑(1 + 1 + 1) + 1) / (↑(1 + 1 + 1).factorial * ↑(1 + 1 + 1)) ≤
    1 + x + x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (rexp x / x ^ n)⁻¹ = x ^ n * rexp (-x)

Tactic:
inv_eq_one_div,

Goal state after:
n : ℕ
x : ℝ
⊢ 1 / (rexp x / x ^ n) = x ^ n * rexp (-x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin π = 0

Tactic:
← mul_div_cancel_left₀ π two_ne_zero,

Goal state after:
⊢ sin (2 * π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos π = -1

Tactic:
← mul_div_cancel_left₀ π two_ne_zero,

Goal state after:
⊢ cos (2 * π / 2) = -1
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
ker_normedMk

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 16) = √(2 + √(2 + √2)) / 2

Tactic:
trans cos (π / 2 ^ 4)
  · congr
    norm_num
  · simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 3) ^ 2 = 3 / 4

Tactic:
rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]

Goal state after:
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < δ + ε
⊢ False

Tactic:
rw [add_comm] at hxy

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
⊢ False
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < δ + ε
⊢ False

Tactic:
rw [add_comm] at hxy

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
⊢ False
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ δ + ε
⊢ False

Tactic:
rw [add_comm] at hxy

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
⊢ False
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
· rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
rw [← closure_thickening hδ, thickening_closure, thickening_thickening hε hδ]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

Tactic:
eventually_atTop

Goal state after:
case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ a, ∀ (b : ℕ), a ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f