mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.LIntegral

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
convert! (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm
  simp [map_mul_left_eq_self μ g]

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

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

Tactic:
by
  refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
    ← lintegral_add_left hf]
  simp only [Pi.add_apply]

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

Goal state before:
pp: case refine_1
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 : Set G
Ks : K ⊆ s
K_comp : IsCompact K
hK : r < μ K
⊢ closure[inst✝³] K ⊆ s

Tactic:
exact IsCompact.closure_subset_measurableSet K_comp s_meas Ks

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : TopologicalSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
c : ℝ≥0
hc : c ≠ 0
⊢ ↑c ≠ 0

Tactic:
by simp [hc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
s : Set α
⊢ (c • μ) s ≠ ∞ ↔ μ s ≠ ∞

Tactic:
simp [ENNReal.mul_eq_top, hc, h'c]

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

Goal state before:
pp: x y : ℝ≥0
⊢ sqrt (x * y) = sqrt x * sqrt y

Tactic:
sqrt_eq_iff_eq_sq,

Goal state after:
x y : ℝ≥0
⊢ x * y = (sqrt x * sqrt y) ^ 2
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∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : g =ᵐ[μ.withDensity f'] AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

Tactic:
rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z

Goal state after:
case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x
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 : ι
hn : notConvergentSeqLTIndex ⋯ hf hsm hs hfg N ≤ n
x : α
hx : x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg
⊢ edist (g x) (f n x) < δ

Tactic:
refine lt_of_le_of_lt ?_ hN

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)⁻¹ < δ
n : ι
hn : notConvergentSeqLTIndex ⋯ hf hsm hs hfg N ≤ n
x : α
hx : x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg
⊢ edist (g x) (f n x) ≤ (↑N)⁻¹
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
have F_le_bound := all_ae_norm_ofReal_F_le_bound h_bound
  rw [← ae_all_iff] at F_le_bound
  apply F_le_bound.mp ((ae_tendsto_ofReal_norm h_lim).mono _)
  intro a tendsto_norm F_le_bound
  exact le_of_tendsto' tendsto_norm F_le_bound

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

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
simp_rw [abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]

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

Goal state before:
pp: z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = ↑2 * ↑(Real.nnabs z.im)

Tactic:
NNReal.coe_two,

Goal state after:
z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = 2 * ↑(Real.nnabs z.im)
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∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by
  let f' := hf.mk f
  calc
    ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, g a ∂μ.withDensity f' := by
      rw [withDensity_congr_ae hf.ae_eq_mk]
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]
    _ = ∫⁻ a, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ (↑f n).im) j - (fun n ↦ (↑f n).im) i| < ε

Tactic:
simpa only [← ofReal_sub, norm_real, sub_re, sub_im] using (abs_im_le_norm _).trans_lt <| H _ ij

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ ↑_q • _a₁ ≤ _q • _a₂

Tactic:
← NNRat.cast_smul_eq_nnqsmul ℚ

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ ↑_q • _a₁ ≤ ↑_q • _a₂
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ ↑_q • _a₁ < _q • _a₂

Tactic:
← NNRat.cast_smul_eq_nnqsmul ℚ

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ ↑_q • _a₁ < ↑_q • _a₂
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ ↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)

Tactic:
by
  simp only [sub_conj, ofReal_mul, ofReal_ofNat, mul_right_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 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 : Type u_5
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
r : R
hr : star r * r = 1 ∧ r * star r = 1
⊢ f r ∈ unitary S

Tactic:
simpa [map_star, map_mul] using! And.intro congr(f $(hr.1)) congr(f $(hr.2))

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (↑r * z) = r * im z

Tactic:
by
  simp only [add_zero, ofReal_im, zero_mul, ofReal_re, mul_im]

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

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

Tactic:
re_add_im,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z - (starRingEnd K) z = z - (↑(re z) - ↑(im z) * I)
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
re_add_im,

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

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

Tactic:
neg_sub,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -I * (starRingEnd K) z) / 2 = I * (z - (starRingEnd K) z) / 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z✝ z w : K
⊢ re (z * w) * re (z * w) + im (z * w) * im (z * w) = (re z * re z + im z * im z) * (re w * re w + im w * im w)

Tactic:
simp only [mul_im, mul_re]
    ring

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

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
⊢ x ∈ e.target

Tactic:
rw [h']

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
⊢ x ∈ univ
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
hx : x ∈ e.source
⊢ 𝓝 (↑e.symm (↑e x)) = 𝓝 x

Tactic:
e.left_inv hx

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 x = 𝓝 x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y

Tactic:
rw [RCLike.le_iff_re_im] at *

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)
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
⊢ (algebraMap ℝ 𝕜) 0 = 0

Tactic:
by subst h''; exact h.algebraMap.map_zero'

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
⊢ (IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i) → IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i

Tactic:
intro hg

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
⊢ IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i
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 : IsBigOWith c l f' k'
hg : IsBigOWith c l g' k'
⊢ IsBigOWith c l (fun x ↦ (f' x, g' x)) k'

Tactic:
isBigOWith_iff

Goal state after:
α : 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‖
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 = 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

Tactic:
rw [hk]

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) (k + max n i) - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range (k + max n i), a k - ∑ k ∈ range (max n i), a k
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 ↔ (fun _x ↦ 1) =o[l] g

Tactic:
exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
    (isBigO_const_one ℝ c l).trans_isLittleO⟩

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

Goal state before:
pp: x : ℂ
⊢ (cexp ((starRingEnd ℂ) x) - cexp ((starRingEnd ℂ) (-x))) / 2 = (starRingEnd ℂ) (sinh x)

Tactic:
exp_conj,

Goal state after:
x : ℂ
⊢ ((starRingEnd ℂ) (cexp x) - cexp ((starRingEnd ℂ) (-x))) / 2 = (starRingEnd ℂ) (sinh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) (cexp x) - cexp ((starRingEnd ℂ) (-x))) / 2 = (starRingEnd ℂ) (sinh x)

Tactic:
exp_conj,

Goal state after:
x : ℂ
⊢ ((starRingEnd ℂ) (cexp x) - (starRingEnd ℂ) (cexp (-x))) / 2 = (starRingEnd ℂ) (sinh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (cexp ((starRingEnd ℂ) x) + cexp ((starRingEnd ℂ) (-x))) / 2 = (starRingEnd ℂ) (cosh x)

Tactic:
exp_conj,

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

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) (cexp x) + cexp ((starRingEnd ℂ) (-x))) / 2 = (starRingEnd ℂ) (cosh x)

Tactic:
exp_conj,

Goal state after:
x : ℂ
⊢ ((starRingEnd ℂ) (cexp x) + (starRingEnd ℂ) (cexp (-x))) / 2 = (starRingEnd ℂ) (cosh x)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
cases le_total x 0

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ rexp |x| ≤ rexp x + rexp (-x)

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ rexp |x| ≤ rexp x + rexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
add_neg_cancel,

Goal state after:
x : ℂ
⊢ cexp 0 = 1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
neg_sub,

Goal state after:
x : ℂ
⊢ cexp (x * I) - cexp (-(x * I)) = cexp (x * I) - cexp (-x * I)
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 : α
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x

Tactic:
neg_sub,

Goal state after:
α : 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 : α
⊢ f₁ x - -f₂ x = f₁ x + f₂ x
Module: Mathlib.Analysis.Asymptotics.Lemmas

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

Tactic:
isBigOWith_iff

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

Goal state before:
pp: x : ℝ
⊢ cos |x| = cos x

Tactic:
cases le_total x 0

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ cos |x| = cos x

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cos |x| = cos x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh |x| = cosh x

Tactic:
cases le_total x 0

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ cosh |x| = cosh x

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cosh |x| = cosh x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
add_neg_cancel,

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

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

Tactic:
neg_sub,

Goal state after:
x : ℝ
⊢ ‖1 - cexp (I * ↑x)‖ = ‖1 - cexp (↑x * I)‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm✝ : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a < -(a - (k + (k + 1)) • ε)

Tactic:
neg_sub,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm✝ : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a < (k + (k + 1)) • ε - a
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
⊢ IsBigOWith (‖c‖ / sInf (Norm.norm '' f '' s)) (𝓟 s) (fun x ↦ c) f

Tactic:
by
  refine isBigOWith_principal.mpr fun x hx ↦ ?_
  rw [mul_comm_div]
  replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
  have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩
  refine le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
    h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx
  obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty
  rw [← hnormCx, ← hCx]
  exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ -(f j - f i) < ε

Tactic:
neg_sub,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ f i - f j < ε
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 α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
m : ℕ
| -(abv x ^ m - 1) / -(abv x - 1)

Tactic:
neg_sub,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
m : ℕ
| (1 - abv x ^ m) / -(abv x - 1)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x : ℝ
⊢ √(rexp x) = rexp (x / 2)

Tactic:
sqrt_eq_iff_eq_sq,

Goal state after:
x : ℝ
⊢ rexp x = rexp (x / 2) ^ 2

case hx
x : ℝ
⊢ 0 ≤ rexp x

case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 π
⊢ 0 ≤ sin x

Tactic:
rw [← closure_Ioo pi_ne_zero.symm] at hx
  exact
    closure_lt_subset_le continuous_const continuous_sin
      (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)

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

Goal state before:
pp: x : ℝ
⊢ cos (-(π / 2 - x)) = sin x

Tactic:
neg_sub,

Goal state after:
x : ℝ
⊢ cos (x - π / 2) = sin x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap (fun x ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
simp_rw [norm_exp, comap_comap, Function.comp_def]

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

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ sin x * sin x = 0

Tactic:
mul_eq_zero,

Goal state after:
x : ℝ
⊢ sin x = 0 ↔ sin x = 0 ∨ sin x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ cos x = 0 ↔ cos x * cos x = 0

Tactic:
mul_eq_zero,

Goal state after:
x : ℝ
⊢ cos x = 0 ↔ cos x = 0 ∨ cos x = 0
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 - 0) * dist y x = dist y x

Tactic:
by rw [sub_zero, one_mul]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
s : Set E
⊢ ‖0‖₊ • ediam s ≤ ediam (0 • s)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
    · simp
    simp [zero_smul_set hs, ← Set.singleton_zero]

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

Goal state before:
pp: n : ℕ
⊢ √(2 - sqrtTwoAddSeries 0 n) = sin (π / 2 ^ (n + 2)) * 2

Tactic:
sqrt_eq_iff_eq_sq,

Goal state after:
n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = (sin (π / 2 ^ (n + 2)) * 2) ^ 2

case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2

Tactic:
congr <;> norm_num

Goal state after: