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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
⊢ Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))

Tactic:
measure_iUnion hsd hsm

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
⊢ Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (∑' (i : ℕ), μ (s i) + ε / 2))
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
A : Set G
⊢ (Measure.map (fun h ↦ h * g) μ) A = μ A

Tactic:
rw [map_mul_right_eq_self μ g]

Goal state after:
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ (comap (⇑f) μ) ((fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
hf.comap_apply

Goal state after:
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
hf.comap_apply

Goal state after:
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)

Tactic:
hf.comap_apply

Goal state after:
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)
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
⊢ (comap (⇑f) μ) ((fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
hf.comap_apply

Goal state after:
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
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s
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
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
hf.comap_apply

Goal state after:
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
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = μ (⇑f '' s)
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
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = μ (⇑f '' s)

Tactic:
hf.comap_apply

Goal state after:
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
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = μ (⇑f '' s)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ (map Prod.swap ρ).snd = ρ.fst

Tactic:
rw [Measure.snd, Measure.map_map measurable_snd measurable_swap]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Tactic:
by
  simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]

Goal state after:
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✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
⊢ map (fun x ↦ g * x) μ ≪ map (fun x ↦ g * x) (map Inv.inv μ)

Tactic:
exact (absolutelyContinuous_inv μ).map (measurable_const_mul g)

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

Goal state before:
pp: case inr
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ✝ : Measure G
inst✝⁶ : μ✝.IsHaarMeasure
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : T1Space G
inst✝² : WeaklyLocallyCompactSpace G
inst✝¹ : (𝓝[≠] 1).NeBot
μ : Measure G
inst✝ : μ.IsHaarMeasure
h : μ 1 ≠ 0
⊢ NullSingletonClass μ

Tactic:
obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1

Goal state after:
case inr
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ✝ : Measure G
inst✝⁶ : μ✝.IsHaarMeasure
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : T1Space G
inst✝² : WeaklyLocallyCompactSpace G
inst✝¹ : (𝓝[≠] 1).NeBot
μ : Measure G
inst✝ : μ.IsHaarMeasure
h : μ 1 ≠ 0
K : Set G
K_compact : IsCompact K
K_nhds : K ∈ 𝓝 1
⊢ NullSingletonClass μ
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
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
rw [← μ.inv_inv]
  exact
    (quasiMeasurePreserving_inv μ.inv).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)

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 g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

Tactic:
by
  rw [← lintegral_add_left' (hf.edist hh)]
  refine lintegral_mono fun a => ?_
  apply edist_triangle_right

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))
⊢ ⋃ n, s ∩ notConvergentSeq f g n (notConvergentSeqLTIndex ⋯ hf hsm hs hfg n) ⊆ s

Tactic:
← Set.inter_iUnion

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))
⊢ s ∩ ⋃ i, notConvergentSeq f g i (notConvergentSeqLTIndex ⋯ hf hsm hs hfg i) ⊆ s
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
by
  rw [norm_def, normSq_apply, sq, sq]

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

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

Tactic:
have : z.im * z.im = 1 - z.re * z.re := by
    replace hz := sq_eq_one_iff.mpr (.inl hz)
    rw [Complex.sq_norm, normSq_apply] at hz
    linarith

Goal state after:
z : ℂ
hz : ‖z‖ = 1
this : z.im * z.im = 1 - z.re * z.re
⊢ ‖z - 1‖ ^ 2 = 2 * (1 - z.re)
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ ↑q * a < ↑q * b

Tactic:
exact mul_lt_mul_of_pos_left hab <| NNRat.cast_pos.2 hq

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + μ.withDensity (∑' (n : ℕ), s.indicator 1)

Tactic:
congr 2 with x

Goal state after:
case e_a.e_f
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
x : α
⊢ s.indicator f x = (∑' (n : ℕ), s.indicator 1) x
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
nth_rw 1 [← star_star x]

Goal state after:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
obtain rfl | hx := eq_or_ne x 0
  · exact ⟨1, by simp⟩
  · exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩

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
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ((starRingEnd 𝕜) z) =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        z

Tactic:
subst h''; exact h.conj_re_ax

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def, eventually_principal]

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

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ f'' =o[𝓟 s] g'

Tactic:
apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
    exact fun x hx ↦ (h x hx).symm

Goal state after:
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
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ (∑ i ∈ s, A i) =o[l] g'

Tactic:
exact Finset.sum_induction A (· =o[l] g') (fun _ _ ↦ .add) (isLittleO_zero ..) h

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ c • f' x) ↔ f =o[l] f'

Tactic:
rw [← isLittleO_norm_right]

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c • f' x‖) ↔ f =o[l] f'
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'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =o[l] B i
⊢ (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E'' : Type u_9
inst✝¹ : Norm F
inst✝ : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =o[l] g ↔ Tendsto (fun x ↦ ‖g x‖) l atTop

Tactic:
simp only [← isLittleO_one_left_iff ℝ]
  exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
    (isBigO_const_one ℝ c l).trans_isLittleO⟩

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ = rexp x

Tactic:
rw [exp, Complex.exp, ← cauSeqRe, lim_re]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Tactic:
· exact sub_pos.2 hc

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

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 ≤ sin x ^ 2 + cos x ^ 2

Tactic:
exact le_add_of_nonneg_right (sq_nonneg _)

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

Goal state before:
pp: x : ℝ
⊢ 1 - 1 / 2 - cos (2 * x) / 2 = 1 / 2 - cos (2 * x) / 2

Tactic:
sub_half

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

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

Tactic:
norm_exp_ofReal_mul_I

Goal state after:
x : ℝ
⊢ 1 = 1
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case hbc
α : 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
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
i : ℕ
a✝ : i ∈ {i ∈ range K | max N M + 1 ≤ i}
⊢ abv (∑ k ∈ range (K - i), g k) + abv (-∑ k ∈ range K, g k) ≤ 2 * Q

Tactic:
rw [two_mul, abv_neg abv]

Goal state after:
case hbc
α : 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
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
i : ℕ
a✝ : i ∈ {i ∈ range K | max N M + 1 ≤ i}
⊢ abv (∑ k ∈ range (K - i), g k) + abv (∑ k ∈ range K, g k) ≤ Q + Q
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)
⊢ 1 + x + x ^ 2 < 1 / (1 - x)

Tactic:
by rw [lt_div_iff₀] <;> nlinarith

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
⊢ ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}

Tactic:
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 1 ε ↔ ↑x ∈ {x | ‖x‖ < ε}
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ uniformity (M ⧸ S) = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}

Tactic:
rw [uniformity_eq_comap_nhds_one_left, (nhds_one_hasBasis.comap _).eq_biInf]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ ⨅ i, ⨅ (_ : 0 < i), Filter.principal ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' {x | ‖x‖ < i}) =
    ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ ≤ 1 * ‖m‖

Tactic:
simp [norm_mk_le_norm]

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

Goal state before:
pp: x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ cos y < cos x

Tactic:
← sin_pi_div_two_sub,

Goal state after:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < cos x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ ‖m + x‖ < ‖f m‖ + ε

Tactic:
hquot.norm

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ ‖m + x‖ < sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑f.ker) + ε
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ ‖f m‖ ≤ ‖m‖

Tactic:
hquot.norm

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑f.ker) ≤ ‖m‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (closedBall x r) = sphere x r

Tactic:
by
  rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_sdiff_ball]

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
h'r : r < 1
⊢ Tendsto (fun n ↦ ↑n * r ^ n) atTop (𝓝 0)

Tactic:
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r

Goal state after: