mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
x✝ : X ⊕ Y
⊢ Sum.dist (Sum.inl p) x✝ ≤ Sum.dist (Sum.inl p) (Sum.inr q) + Sum.dist (Sum.inr q) x✝

Tactic:
simp only [Sum.dist_eq_glueDist p q]

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
x✝ : X ⊕ Y
⊢ glueDist (fun x ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl p) x✝ ≤
    glueDist (fun x ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl p) (Sum.inr q) +
      glueDist (fun x ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr q) x✝
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
c : ι → Set (↑I × ↑I)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t,
    t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
  have hδ := half_pos δ_pos
  simp_rw [Subtype.ext_iff]
  have h : (0 : ℝ) ≤ 1 := zero_le_one
  refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
  obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) trivial
  exact ⟨i, fun t ht ↦ hsub (Metric.mem_ball.mpr <| (max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <|
    abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <| half_lt_self δ_pos)⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case refine_2
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x y : (i : ι) × E i), Sigma.dist x y = Sigma.dist y x

Tactic:
rintro ⟨i, x⟩ ⟨j, y⟩

Goal state after:
case refine_2
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = Sigma.dist ⟨j, y⟩ ⟨i, x⟩
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case refine_3
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x y : (i : ι) × E i), Sigma.dist x y = 0 → x = y

Tactic:
rintro ⟨i, x⟩ ⟨j, y⟩

Goal state after:
case refine_3
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0 → ⟨i, x⟩ = ⟨j, y⟩
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
⊢ m₀ ≥ n → ∀ n_1 ≥ n, dist (u m₀) (u n_1) < ε

Tactic:
hm₀

Goal state after:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
⊢ ∀ n_1 ≥ n, dist (u m₀) (u n_1) < ε
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix x s < longestPrefix y s
⊢ longestPrefix y s = longestPrefix x s

Tactic:
· have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
        inter_cylinder_longestPrefix_nonempty hs hne y
      have A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty :=
        Ay.mono (inter_subset_inter_right s (cylinder_anti _ L))
      have Z := disjoint_cylinder_of_longestPrefix_lt hs xs (Nat.lt_succ_self _)
      rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H] at Z
      exact (A'y.not_disjoint Z).elim

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ c) (f a) ∂μ = c * μ (f ⁻¹' s)

Tactic:
by
  rw [← lintegral_map (measurable_const.indicator hs) hf, lintegral_indicator_const hs,
    Measure.map_apply hf hs]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
s : Set β
hs : MeasurableSet s
f : β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
by
  rw [← hg.map_eq, setLIntegral_map hs hf hg.measurable]

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
have fx : f x = A.some := by simp_rw [f, if_neg xs]

Goal state after:
case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = A.some
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
⊢ MeasurableAdd₂ (Measure α)

Tactic:
refine ⟨Measure.measurable_of_measurable_coe _ fun s hs => ?_⟩

Goal state after:
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (b.1 + b.2) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ ↦ ∫⁻ (x : α), f x ∂μ

Tactic:
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ ↦ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x})
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
⊢ F =ᵐ[μ] univ ↔ F = univ

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s

Tactic:
sum_apply _ hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s
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 μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
⊢ Measurable fun x ↦ μ ((fun y ↦ y * x) ⁻¹' s)

Tactic:
convert! this using 1

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
⊢ (fun x ↦ μ ((fun y ↦ y * x) ⁻¹' s)) = fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
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:
by
  refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul' r f hr]
  simp only [Pi.smul_apply, smul_eq_mul]

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

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

Tactic:
lt_top_iff_ne_top

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), f a ∂μ ≠ ∞
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]

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

Goal state before:
pp: x : ℝ
⊢ √(x * x) = |x|

Tactic:
by
  rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]

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

Goal state before:
pp: x : ℝ
⊢ √x ≤ x ↔ x = 0 ∨ 1 ≤ x

Tactic:
rw [sqrt_le_iff, ← sub_nonneg (a := x ^ 2), sq, ← mul_sub_one]
  grind [mul_nonneg_iff]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqConj f).lim.im = ((starRingEnd ℂ) f.lim).im

Tactic:
simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
⊢ CauSeq.lim ⟨fun n ↦ -(↑f n).im, ⋯⟩ = (-⟨fun n ↦ (↑f n).im, ⋯⟩).lim
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * (B * star B) * star U = 1

Tactic:
hB₂,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * 1 * star U = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
⊢ automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = (g • automorphize f) ⟦b⟧

Tactic:
simp only [automorphize, Pi.smul_apply', comp_apply]

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
⊢ Quotient.lift (fun b ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ ⟦b⟧ =
    g ⟦b⟧ • Quotient.lift (fun b ↦ ∑' (a : α), f (a • b)) ⋯ ⟦b⟧
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
real_smul_eq_coe_mul r (_ - _),

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, ↑x = z

Tactic:
simp_rw [neg_iff (K := K), ext_iff (K := K)]; aesop

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
⊢ Function.Involutive star

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

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

Goal state before:
pp: case mpr
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
case mpr =>
    rw [isBigO_iff]
    obtain ⟨c, ⟨_, hc⟩⟩ := h
    exact ⟨c, hc⟩

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 β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun x ↦ f (x, b)) =O[l] fun x ↦ g (x, b)

Tactic:
by
  simp only [isBigO_iff, eventually_iff, mem_prod_iff]
  rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
  exact mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩

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

Goal state before:
pp: n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial (l + m) = a * b

Tactic:
← h₁,

Goal state after:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial (l + m) = n.ascFactorial l * b
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (x + y) ^ m / ↑m.factorial = ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
rw [add_pow, div_eq_mul_inv, sum_mul]

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ ∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * ↑(m.choose i) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 ↦ x1 ≤ x2) (‖f x‖ / ‖g x‖) c

Tactic:
exact div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ u =o[l] fun _x ↦ 1

Tactic:
exact huv.trans_isBigO (hv.isBigO_one 𝕜)

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

Goal state before:
pp: x y : ℂ
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I

Tactic:
sin_add,

Goal state after:
x y : ℂ
⊢ sin x * cos (y * I) + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case calc_2
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
cos_sub

Goal state after:
case calc_2
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin (x + x) = 2 * sin x * cos x

Tactic:
sin_add,

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

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2

Tactic:
rw [tan_eq_sin_div_cos, div_pow]
  simp [field]

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

Goal state before:
pp: x : ℝ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cos (3 * x)) = ↑(4 * cos x ^ 3 - 3 * cos x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [← ofReal_inj]

Goal state after:
x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [← ofReal_inj]

Goal state after:
x y : ℝ
⊢ ↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh x + sinh x = rexp x

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cosh x - sinh x) = ↑(rexp (-x))
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh x ^ 2 - sinh x ^ 2 = 1

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cosh x ^ 2 - sinh x ^ 2) = ↑1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh x ^ 2 = cosh x ^ 2 - 1

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
rw [← ofReal_inj]

Goal state after:
x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
rw [show 3 = 1 + 1 + 1 from rfl]
      repeat rw [Finset.sum_range_succ]
      norm_num [Nat.factorial]
      nlinarith

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ rexp (x / 2) ^ 2 ≤ ?m.47

Tactic:
grw [Real.exp_bound' (x := x / 2) (by grind) (by grind) (n := 3) (by simp)]

Goal state after:
case ha
x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 ≤ rexp (x / 2)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ ⇑e) =o[𝓝 (e.symm b)] (g ∘ ⇑e)

Tactic:
simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => e.isBigOWith_congr

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

Goal state before:
pp: case bc
α : 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 : ℕ := ⋯
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
⊢ a - l • ε < f j

Tactic:
exact hl _ <| hi.1.trans hj

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

Goal state before:
pp: ⊢ sin (π / 2 + π / 2) = 0

Tactic:
sin_add,

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

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

Tactic:
by simp [sub_eq_add_neg, cos_add]

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

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ ‖rexp (-r)‖ < 1

Tactic:
norm_of_nonneg (exp_nonneg _),

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ rexp (-r) < 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : 1 < v a
⊢ Tendsto (fun n ↦ v (1 + a ^ n)⁻¹) atTop (𝓝 0)

Tactic:
map_inv₀,

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : 1 < v a
⊢ Tendsto (fun n ↦ (v (1 + a ^ n))⁻¹) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by simp [sub_eq_add_neg, cos_add]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
⊢ Summable fun n ↦ ↑n ^ k * r ^ n

Tactic:
convert! this using 1

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
⊢ (fun n ↦ ↑n ^ k * r ^ n) = fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₁ γ₂ : Path x y
h : (fun γ ↦ ⇑γ.toContinuousMap) γ₁ = (fun γ ↦ ⇑γ.toContinuousMap) γ₂
⊢ γ₁ = γ₂

Tactic:
by
    simp only [DFunLike.coe_fn_eq] at h
    cases γ₁; cases γ₂; congr

Goal state after: