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
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ ∑ k ∈ t, μ (F k) + ∑ k ∈ t, δ k + ε / 2

Tactic:
by
          rw [← sum_add_distrib]
          gcongr
          apply hF

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
h : H
⊢ Measure.map (fun x ↦ h * x) (Measure.map (⇑f) μ) = Measure.map (⇑f) μ

Tactic:
rw [map_map (measurable_const_mul _) hf]

Goal state after:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
h : H
⊢ Measure.map ((fun x ↦ h * x) ∘ ⇑f) μ = Measure.map (⇑f) μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ 1 * ν s = ν s

Tactic:
one_mul

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ ν s = ν s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ (μ.withDensity f) univ < ∞

Tactic:
withDensity_apply _ MeasurableSet.univ,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∫⁻ (a : α) in univ, f a ∂μ < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = 1 * g a

Tactic:
one_mul

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = g a
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᵐ[μ] f
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞

Tactic:
rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
have : ∀ᵐ x ∂μ, .ofReal (f x).toReal = f x := by filter_upwards [hf] with x hx; simp [hx]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √x * √x = x

Tactic:
by
  rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x = 1 * i x

Tactic:
one_mul

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x = i x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ √(0 ^ 2 + (z.im - w.im) ^ 2) = dist z.im w.im

Tactic:
zero_pow two_ne_zero,

Goal state after:
z w : ℂ
h : z.re = w.re
⊢ √(0 + (z.im - w.im) ^ 2) = dist z.im w.im
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.im = w.im
⊢ √((z.re - w.re) ^ 2 + 0 ^ 2) = dist z.re w.re

Tactic:
zero_pow two_ne_zero,

Goal state after:
z w : ℂ
h : z.im = w.im
⊢ √((z.re - w.re) ^ 2 + 0) = dist z.re w.re
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 < ∞
h'x : f x = AEMeasurable.mk f hf x
⊢ AEMeasurable.mk f hf x < ∞

Tactic:
rwa [← h'x]

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

Goal state before:
pp: ⊢ I * I = -1

Tactic:
I_mul_I

Goal state after:
⊢ -1 = -1
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ I ^ 4 = 1

Tactic:
(by simp : 4 = 2 * 2),

Goal state after:
⊢ I ^ (2 * 2) = 1
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ -(1 * I) = -I

Tactic:
one_mul

Goal state after:
⊢ -I = -I
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∞
⊢ map (fun x ↦ x.1 * x.2) (μ.prod (s • ν)) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)

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

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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1 * ‖1‖

Tactic:
one_mul

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = ‖1‖
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖↑((algebraMap R ℝ) r) * x‖ ≤ ‖r‖ * ‖x‖

Tactic:
norm_mul,

Goal state after:
z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖↑((algebraMap R ℝ) r)‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.Analysis.Complex.Basic

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

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

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
x✝ : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
this : IsStarNormal x
⊢ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
simp [sq, ← star_mul_self_eq_realPart_sq_add_imaginaryPart_sq x, h]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ ‖↑r * x‖ = ‖r‖ * ‖x‖

Tactic:
norm_mul,

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ ‖↑r‖ * ‖x‖ = ‖r‖ * ‖x‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ re x ∧ im x = 0 ↔ ∃ s, x = star s * s

Tactic:
refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ (∃ s, x = star s * s) → 0 ≤ re x ∧ im x = 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖reLm x‖ ≤ 1 * ‖x‖

Tactic:
one_mul

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖reLm x‖ ≤ ‖x‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖imLm x‖ ≤ 1 * ‖x‖

Tactic:
one_mul

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖imLm x‖ ≤ ‖x‖
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 : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      r

Tactic:
subst h''; exact h.ofReal_re_ax

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

Goal state before:
pp: case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
one_mul

Goal state after:
case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ ‖f x‖ ≤ ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
one_mul

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ ‖g x‖
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'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Tactic:
by
  simp_rw [IsLittleO_def]
  refine forall_congr' fun c => forall_congr' fun hc => ?_
  rw [isBigOWith_insert]
  rw [h, norm_zero]
  positivity

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range n = n' ::ₘ Multiset.range n'

Tactic:
by
  rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯

Tactic:
by
  rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]

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
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k

Tactic:
tsub_eq_iff_eq_add_of_le ji

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
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖ = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)

Tactic:
norm_mul,

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ c₁ * c₂ * (‖g₁ a✝‖ * ‖g₂ a✝‖) = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ < 1 * ↑n

Tactic:
one_mul

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ < ↑n
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ cexp (↑n * x) * cexp (1 * x) = cexp (↑n * x) * cexp x

Tactic:
one_mul

Goal state after:
x : ℂ
n : ℕ
⊢ cexp (↑n * x) * cexp x = cexp (↑n * x) * cexp x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v

Tactic:
· simp only [IsLittleO_def]
    rintro ⟨φ, hφ, huvφ⟩ c hpos
    rw [NormedAddGroup.tendsto_nhds_zero] at hφ
    exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

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

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
x : α
hx : f x ≠ 0
⊢ ‖f x * g x‖ ≤ c * ‖h✝ x‖ ↔ ‖g x‖ ≤ c * ‖h✝ x / f x‖

Tactic:
norm_mul,

Goal state after:
case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
x : α
hx : f x ≠ 0
⊢ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖ ↔ ‖g x‖ ≤ c * ‖h✝ x / f x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h✝ x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h✝ x‖

Tactic:
norm_mul,

Goal state after:
case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h✝ x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cos ↑x + sin ↑x * I‖ = 1

Tactic:
by
  have := Real.sin_sq_add_cos_sq x
  simp_all [add_comm, norm_def, normSq, sq, sin_ofReal_re, cos_ofReal_re, mul_re]

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

Goal state before:
pp: z : ℂ
⊢ ‖cexp z‖ = Real.exp z.re

Tactic:
by
  rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
hn : n₁ ≤ n
⊢ ‖f n‖ ≤ max C₀ C₁ * ‖g n‖

Tactic:
induction n using Nat.strongRecOn with

Goal state after:
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 < ε
n : N
⊢ ∃ m, f m = n ∧ ‖m‖ < ‖n‖ + ε

Tactic:
obtain ⟨m, rfl⟩ := hquot.surjective n
  have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty := by
    rw [Set.image_nonempty]
    exact ⟨0, f.ker.zero_mem⟩
  rcases Real.lt_sInf_add_pos nonemp hε
    with ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩
  exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by
    rwa [hquot.norm]⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ ‖x - (r • x + (y - r • y))‖ = ‖x - y - r • (x - y)‖

Tactic:
smul_sub,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ ‖x - (r • x + (y - r • y))‖ = ‖x - y - (r • x - r • y)‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 1 * dist y x = dist y x

Tactic:
one_mul

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ dist y x = dist y x
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1

Tactic:
mem_closedBall,

Goal state after:
case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : dist y x ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
⊢ (Summable fun n ↦ ξ ^ n) ↔ ‖ξ‖ < 1

Tactic:
refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩
  obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists
  simp only [norm_pow, dist_zero_right] at hk
  rw [← one_pow k] at hk
  exact lt_of_pow_lt_pow_left₀ _ zero_le_one hk

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖↑(u n) * r ^ n‖) =O[atTop] fun n ↦ ↑(u n) * ‖r‖ ^ n

Tactic:
by
      apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
      apply (norm_mul_le _ _).trans
      have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
      exact this.trans (le_of_eq (by ring))

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

Goal state before:
pp: ⊢ -(1 * I) = -I

Tactic:
one_mul

Goal state after:
⊢ -I = -I
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
⊢ ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Tactic:
rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂

Goal state after:
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n

Tactic:
norm_mul,

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n * w ^ n‖ ≤ C

Tactic:
norm_mul,

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n‖ * ‖w ^ n‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = 1 * cexp (↑z.arg * I)

Tactic:
one_mul

Goal state after:
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = cexp (↑z.arg * I)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x / ↑(n + 1) * (x ^ n / ↑n !)‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
norm_mul,

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x / ↑(n + 1)‖ * ‖x ^ n / ↑n !‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
⊢ x = y

Tactic:
by
  rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
by
  rw [← exp_lt_exp, exp_log hx, exp_log hy]

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

Goal state before:
pp: case inr
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y

Tactic:
exact (log_le_iff_le_exp hx).mp h

Goal state after: