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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
refine Measure.ext fun s hs => ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
⊢ r < (sum μ) s → ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K

Tactic:
hr

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K
Module: Mathlib.MeasureTheory.Measure.WithDensity

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

Tactic:
refine Measure.ext fun s hs => ?_

Goal state after:
α : 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
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict S, ENNReal.ofReal (f x) = 0 x

Tactic:
exact (ae_restrict_mem hS).mono fun x hx => ENNReal.ofReal_eq_zero.2 (le_of_lt hx)

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
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : μ s ≠ ∞
r : ℝ≥0∞
⊢ r < μ s → ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K

Tactic:
hr

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ (c • μ) s ≠ ∞
r : ℝ≥0∞
⊢ r < (c • μ) s → ∃ K ⊆ s, IsCompact K ∧ r < (c • μ) K

Tactic:
hr

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ (c • μ) s ≠ ∞
r : ℝ≥0∞
hr : r < (c • μ) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
⊢ r < (μ.restrict A) V → ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
hr

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
field_simp

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ 2 * a * x = -b + s ∨ 2 * a * x = -b - s
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
mul_self_sqrt h

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ x = x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ x < y ^ 2

Tactic:
by
  rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x / y) = √x / √y

Tactic:
rw [division_def, sqrt_mul hx, sqrt_inv, division_def]

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 : α
⊢ f x < ∞ → i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

Tactic:
h'x

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 < ∞
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x
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 < ∞
⊢ f x = AEMeasurable.mk f hf x → AEMeasurable.mk f hf x < ∞

Tactic:
h'x

Goal state after:
α : 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 < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : (μ.withDensity f) s = 0
⊢ μ s = 0

Tactic:
rw [withDensity_apply _ hs, lintegral_eq_zero_iff' hf.restrict,
    ae_eq_restrict_iff_indicator_ae_eq hs, Set.indicator_zero', Filter.EventuallyEq, ae_iff] at hμs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : μ {a | ¬s.indicator f a = 0 a} = 0
⊢ μ s = 0
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
this : 0 ≤ ‖z‖
x✝ : 0 ≤ z
h₁ : re 0 ≤ z.re
h₂ : im 0 = z.im
⊢ z.re = ‖z‖

Tactic:
by rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : ℝ≥0
hf : LipschitzWith K ⇑f
x : V₁
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
by simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : StarMul R
inst✝¹ : Monoid S
inst✝ : StarMul S
f : R →⋆* S
⊢ toUnits.comp (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits

Tactic:
ext; rfl

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

Goal state before:
pp: i j : Fin 2
⊢ (basisOneI.repr (![1, I] i)) j = (Finsupp.single i 1) j

Tactic:
fin_cases i <;> fin_cases j <;> simp

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ?m.43

Tactic:
by congrm (ℑ ($((re_add_im z).symm) • a))

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ ℑ x = 0

Tactic:
imaginaryPart,

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ (skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ) x = 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I

Tactic:
field_simp

Goal state after:
case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ 1 = -I ^ 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z / I = -(z * I)

Tactic:
by rw [div_eq_mul_inv, inv_I, mul_neg]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I‖ = 1

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)

Tactic:
ContinuousWithinAt,

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ Tendsto (f ∘ ↑e) (𝓝[↑e ⁻¹' s] ↑e.symm x) (𝓝 ((f ∘ ↑e) (↑e.symm 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
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w

Tactic:
by subst h''; exact h.mul_im_ax

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
by simp only [IsBigOWith_def]

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
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Tactic:
by
  simp only [IsBigOWith_def]
  exact eventually_map

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 β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}
⊢ {a | ∃ c, {x | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l

Tactic:
exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩

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
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]
  exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖

Tactic:
filter_upwards [hf, hg] with x using max_le

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

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range n'.succ = 0 :: List.map Nat.succ (List.range n')

Tactic:
List.range_succ_eq_map

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ 0 :: List.map Nat.succ (List.range n') = 0 :: List.map Nat.succ (List.range n')
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 α
f₁ f₂ : α → E'
h : (fun x ↦ f₁ x - f₂ x) =o[l] g
⊢ (fun x ↦ f₂ x - f₁ x) =o[l] g

Tactic:
simpa only [neg_sub] using h.neg_left

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

Goal state before:
pp: case succ
α : 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 k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k - ∑ k ∈ range (max n i), a k
⊢ abv (∑ i ∈ range (k + 1 + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + 1 + max n i), a k - ∑ k ∈ range (max n i), a k

Tactic:
| succ k hi =>

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

Goal state before:
pp: case empty
α : 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 ∈ ∅, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith 0 l (∑ i ∈ ∅, A i) g

Tactic:
apply isBigOWith_zero'

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 ^ m.succ / ↑m.succ.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
Nat.factorial_succ,

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

Goal state before:

Tactic:
‖∑ 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.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Tactic:
by
  simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ (‖a‖⁻¹ + 1)⁻¹ < ‖a‖

Tactic:
field_simp

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ 1 < 1 + ‖a‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
by
  rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]
  refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
  change ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ _
  rw [← sum_Ico_eq_sub _ hj]
  calc
    ‖∑ m ∈ Ico n j, (x ^ m / m.factorial : ℂ)‖
      = ‖∑ m ∈ Ico n j, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)‖ := by
      refine congr_arg norm (sum_congr rfl fun m hm => ?_)
      rw [mem_Ico] at hm
      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.1]
    _ ≤ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / m.factorial)‖ :=
      IsAbsoluteValue.abv_sum norm ..
    _ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (m - n).factorial) := by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr with i hi
      · rw [Complex.norm_pow]
      · simp
    _ = ‖x‖ ^ n * ∑ m ∈ range (j - n), (‖x‖ ^ m / m.factorial) := by
      simp [← mul_sum, sum_Ico_eq_sum_range]
    _ ≤ ‖x‖ ^ n * Real.exp ‖x‖ := by
      gcongr
      refine Real.sum_le_exp_of_nonneg ?_ _
      exact norm_nonneg _

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

Goal state before:
pp: x y : ℝ
⊢ cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Tactic:
by
  simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]

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

Goal state before:
pp: x : ℝ
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1

Tactic:
field_simp

Goal state after:
x : ℝ
⊢ rexp x - rexp (-x) < rexp x + rexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))

Tactic:
field_simp

Goal state after:
x : ℝ
⊢ -(rexp x + rexp (-x)) < rexp x - rexp (-x)
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
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
m_pos : 0 < m
⊢ n.succ ≤ m.pred.succ

Tactic:
Nat.succ_pred_eq_of_pos m_pos

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
m_pos : 0 < m
⊢ n.succ ≤ m
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))

Tactic:
field_simp

Goal state after:
case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inl
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, 0 =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |0 n| ≤ C * a ^ n
H : ∀ (n : ℕ), |0 n| ≤ 0 * a ^ n
h₀ : 0 < R
⊢ ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x

Tactic:
exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩

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

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
⊢ Summable fun i ↦ rexp (c * f i)

Tactic:
by
  refine (Real.summable_exp_nat_mul_iff.mpr hc).of_nonneg_of_le (fun _ ↦ by positivity) fun i ↦ ?_
  refine Real.exp_monotone ?_
  conv_rhs => rw [mul_comm]
  exact mul_le_mul_of_nonpos_left (hf i) hc.le

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x ↦ cexp (f x)) l (𝓝 0) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
  rfl

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 < ε
m : M
⊢ ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty

Tactic:
Set.image_nonempty

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
⊢ (↑f.ker).Nonempty
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1

Tactic:
mem_Icc,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ -1 ≤ c ∧ c ≤ 1
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
· exact interior_closedBall x hr

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

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

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

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
⊢ r ∈ closedBall 0 (ε / R) → {x} + r • s ⊆ u

Tactic:
hr

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ {x} + r • s ⊆ u
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ (- -2 - 2 * √5) / (2 * 4) < 0

Tactic:
exact div_neg_of_neg_of_pos (by norm_num [lt_sqrt]) (by positivity)

Goal state after: