mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case empty
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ ∅, MeromorphicAt (F σ) x
⊢ MeromorphicAt 1 x

Tactic:
apply MeromorphicAt.const

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

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt sin (cos x) x

Tactic:
by
  simp only [cos, div_eq_mul_inv]
  convert!
    ((((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp.sub
              ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const
          I).mul_const
      (2 : ℂ)⁻¹ using 1
  simp only [id]
  rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) sin = iteratedDeriv 0 cos

Tactic:
| zero =>

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

Goal state before:
pp: case zero
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
⊢ MeromorphicAt (f ^ 0) x

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) cos = -iteratedDeriv 0 sin

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (2 * 0) sin = (-1) ^ 0 * sin

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) sin = (-1) ^ n * sin

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (2 * 0) cos = (-1) ^ 0 * cos

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) cos = (-1) ^ n * cos

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ multichoose 1 0 = 1

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ multichoose 2 0 = ↑0 + 1

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
⊢ (ascPochhammer R 0).smeval x = (ascPochhammer ℕ 0).smeval x

Tactic:
| zero =>

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

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv^[0] f) x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
⊢ (descPochhammer ℤ 0).smeval r = (ascPochhammer ℕ 0).smeval (r - ↑0 + 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℕ
⊢ (descPochhammer ℤ 0).smeval ↑n = ↑(n.descFactorial 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
⊢ (ascPochhammer ℕ 0).smeval (-r) = (↑0).negOnePow • (descPochhammer ℤ 0).smeval r

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-↑n) * (-↑n + ↑n • 1) = 0

Tactic:
Nat.cast_id,

Goal state after:
n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-↑n) * (-↑n + n • 1) = 0
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
⊢ ∀ᶠ (y : 𝕜) in codiscreteWithin U, AnalyticAt 𝕜 f y

Tactic:
eventually_iff,

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
⊢ {x | AnalyticAt 𝕜 f x} ∈ codiscreteWithin U
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (fun x ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a

Tactic:
exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
⊢ Meromorphic (f ∘ fun x ↦ x - c) ↔ Meromorphic f

Tactic:
by
  nth_rw 2 [← meromorphic_comp_add_const_iff_meromorphic (c := -c)]
  simp_rw [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type u_1
inst✝² : RCLike 𝕂
𝔸 : Type u_2
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
⊢ 1 ≤ (binomialSeries 𝔸 a).radius

Tactic:
by_cases ha : ∀ (k : ℕ), a ≠ k

Goal state after:
case pos
𝕂 : Type u_1
inst✝² : RCLike 𝕂
𝔸 : Type u_2
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
⊢ 1 ≤ (binomialSeries 𝔸 a).radius

case neg
𝕂 : Type u_1
inst✝² : RCLike 𝕂
𝔸 : Type u_2
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ¬∀ (k : ℕ), a ≠ ↑k
⊢ 1 ≤ (binomialSeries 𝔸 a).radius
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (fun x ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a

Tactic:
exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
⊢ (descPochhammer ℤ 0).smeval (r + s) =
    ∑ ij ∈ antidiagonal 0, ↑(Nat.choose 0 ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case zero
a : ℂ
B : Set ℂ := Metric.ball 0 1
⊢ Set.EqOn (iteratedDerivWithin 0 (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ 0).smeval a * (1 + x) ^ (a - ↑0))
    B

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 0 f s) (p.iteratedFDerivSeries 0) s x r

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
⊢ p.iteratedFDerivSeries 0 n = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x ↦ a ^ x) (a ^ x * log a) x

Tactic:
by
  simpa using (hasStrictDerivAt_const _ _).rpow (hasStrictDerivAt_id x) ha

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case zero
p : ℝ
h : ↑0 ≤ p
⊢ ContDiff ℝ ↑0 fun x ↦ x ^ p

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case zero
r x : ℝ
⊢ (deriv^[0] fun x ↦ x ^ r) = fun x ↦ Polynomial.eval r (descPochhammer ℝ 0) * x ^ (r - ↑0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
J2 : iteratedFDerivWithin 𝕜 n (f - g) s x = 0
⊢ (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i ↦ v (σ i)

Tactic:
have J3 : iteratedFDerivWithin 𝕜 n g s x = iteratedFDeriv 𝕜 n g x :=
    iteratedFDerivWithin_eq_iteratedFDeriv hs (gcont.of_le le_top).contDiffAt hx

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
J2 : iteratedFDerivWithin 𝕜 n (f - g) s x = 0
J3 : iteratedFDerivWithin 𝕜 n g s x = iteratedFDeriv 𝕜 n g x
⊢ (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i ↦ v (σ i)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
| ∑ σ, (p n) fun i ↦ v (σ i)

Tactic:
rw [← Equiv.sum_comp (Equiv.mulLeft σ)]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
| ∑ i, (p n) fun i_1 ↦ v (((Equiv.mulLeft σ) i) i_1)
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
⊢ s ⊆ ⋃ y ∈ N, closedEBall y ↑ε

Tactic:
refine hN.trans fun x hx ↦ ?_

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
x : X
hx : x ∈ ⋃ y ∈ N, eball y ↑ε
⊢ x ∈ ⋃ y ∈ N, closedEBall y ↑ε
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsCover coveringRadius Set.univ carrier

Tactic:
by
    simpa [h_carrier, h_covering] using D.isCover_coveringRadius

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ ↑D.packingRadius < dist x y

Tactic:
have hsep : ENNReal.ofReal D.packingRadius < ENNReal.ofReal (dist x y) := by
    simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
hsep : ENNReal.ofReal ↑D.packingRadius < ENNReal.ofReal (dist x y)
⊢ ↑D.packingRadius < dist x y
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
h : 0 < x.toReal
⊢ x.log = ↑(Real.log x.toReal)

Tactic:
by
  simp [log, (ENNReal.toReal_pos_iff.1 h).1.ne', (ENNReal.toReal_pos_iff.1 h).2.ne]

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

Goal state before:
pp: y : EReal
⊢ ∃ a, a.log = y

Tactic:
cases y with

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

Tactic:
simp only [EReal.top_add_coe, exp_top, exp_coe]

Goal state after:
case top.coe
a✝ : ℝ
⊢ ∞ = ∞ * ENNReal.ofReal (Real.exp a✝)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
y : ℝ
⊢ (x * ↑y).exp = x.exp ^ y

Tactic:
rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ liminf (fun n ↦ u n / ↑n) atTop ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
liminf_le_iff'

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (0 ^ y).log = ↑y * log 0

Tactic:
rw [ENNReal.zero_rpow_of_pos y_pos, log_zero, EReal.mul_bot_of_pos]

Goal state after:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ liminf (fun n ↦ (u n).log / ↑n) atTop ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp

Tactic:
liminf_le_iff'

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ 0 * f)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n ↦ c * f n
x : α
⊢ c⁻¹ * (c * f x) = f x

Tactic:
simp [← mul_assoc, inv_mul_cancel₀ hc0]

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * ↑n).exp
⊢ expGrowthInf u ≤ a

Tactic:
apply expGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
  gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
⊢ (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
    ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
ffine

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
⊢ ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (k ^ 0 * f) ↔ SuperpolynomialDecay l k f

Tactic:
| zero =>

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

Goal state before:
pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
⊢ ∀ a' ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n)),
    ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a' * b' ≤ linearGrowthSup (u ∘ v)

Tactic:
intro a

Goal state after:
case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
⊢ a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n)) →
    ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a * b' ≤ linearGrowthSup (u ∘ v)
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
⊢ ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
intro a

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
⊢ a ∈ t' → ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
apply closedBall_subset_closedBall'

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := ⋯
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ r a + dist (x a) (x b) ≤ τ * r b
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ Tendsto (fun n ↦ ↑(μ (s n)).toNNReal) atTop (𝓝 ↑(μ (⋂ n, s n)).toNNReal)

Tactic:
refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal <| ?_).comp <|
        tendsto_measure_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) hm ?_

Goal state after:
case refine_1.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ μ (⋂ n, s n) ≠ ∞

case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ ∃ i, μ (s i) ≠ ∞