mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
| w x < 1

Tactic:
← WithAbs.ofAbs_toAbs w x

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
| w (WithAbs.toAbs w x).ofAbs < 1
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case succ
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ dist (f (g (u n))) y ≤ (↑c * ↑f'symm.nnnorm) ^ (n + 1) * dist (f b) y ∧
    dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ (n + 1)) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y

Tactic:
refine ⟨?_, Ign⟩

Goal state after:
case succ
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ dist (f (g (u n))) y ≤ (↑c * ↑f'symm.nnnorm) ^ (n + 1) * dist (f b) y
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * ‖f' (x' - y' - f'.symm (↑A x' - ↑A y'))‖ = ↑‖↑f'.symm‖₊ * ‖↑A y' - ↑A x' - f' (y' - x')‖

Tactic:
congr 2

Goal state after:
case e_a
𝕜 : 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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ f' (x' - y' - f'.symm (↑A x' - ↑A y')) = ↑A y' - ↑A x' - f' (y' - x')
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ f '' univ = univ

Tactic:
image_univ,

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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ range f = univ
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀ p ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s)), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
⊢ ∀ y ∈ B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖

Tactic:
rw [closure_prod_eq] at this
    intro y y_in
    apply this ⟨x, y⟩
    have : B ∩ closure s ⊆ closure (B ∩ s) := isOpen_ball.inter_closure
    exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩

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

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

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty]
    apply MeromorphicAt.const
  | insert a s ha hs =>
    rw [Finset.prod_insert ha]
    apply (hf a (Finset.mem_insert_self a s)).mul
      (hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))

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
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
z : 𝕜
⊢ f z - g z = f z + -g z

Tactic:
sub_eq_add_neg

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

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt sin ((cexp (x * I) + cexp (-x * I)) * 2⁻¹) x

Tactic:
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

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)

Tactic:
simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (ascPochhammer ℕ (k + 1)).smeval (r + 1) =
    (ascPochhammer ℕ (k + 1)).smeval r + (k + 1).factorial • multichoose (r + 1) k
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) y

Tactic:
· rw [meromorphicAt_comp_add_const_iff_meromorphicAt]
    aesop

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ choose r 1 = r ^ 1

Tactic:
by
  rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']

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 ∘ fun x ↦ x + -c)

Tactic:
sub_eq_add_neg

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

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ HasDerivAt (fun y ↦ ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x

Tactic:
convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1

Goal state after:
case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 • ((r + 1) * ↑(-x) ^ r)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.2 * (p.1 ^ p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ =
    (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.1 ^ p.2 * p.2 * p.1⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
congr 2

Goal state after:
case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1

case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ binomialSeries ℝ a =
    Complex.reCLM.compFormalMultilinearSeries ((binomialSeries ℂ a).compContinuousLinearMap Complex.ofRealCLM)

pp: case e'_12
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

pp: case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ (1 + x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
· ext; simp [Function.comp_def]

Goal state after:
case e'_12
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ (1 + x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n)).compContinuousLinearMap
        Complex.ofRealCLM)

pp: case e'_12
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
· ext n
    simp only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply,
      FormalMultilinearSeries.compContinuousLinearMap_apply]
    simp
    norm_cast

Goal state after:
case e'_12
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (deriv fun x ↦ x ^ p) =Θ[atTop] fun x ↦ x ^ (p - 1)

Tactic:
calc deriv (fun (x : ℝ) ↦ x ^ p) = fun x => p * x ^ (p - 1) := Real.deriv_rpow_const' p
    _ =Θ[atTop] fun x ↦ x ^ (p - 1) :=
      Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ ↑ε
⊢ edist (f x) (f x₀) ≤ ↑K₂ * ↑ε

Tactic:
hf x x₀,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ ↑ε
⊢ ↑K₂ * edist x x₀ ≤ ↑K₂ * ↑ε
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ
⊢ (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)

Tactic:
simp only [log, ENNReal.ofReal_ne_top,
    ENNReal.ofReal_eq_zero, if_false]

Goal state after:
x : ℝ
⊢ (if x ≤ 0 then ⊥ else ↑(Real.log (ENNReal.ofReal x).toReal)) = if x ≤ 0 then ⊥ else ↑(Real.log x)
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: ⊢ StrictMono exp

Tactic:
by
  intro x y h
  induction x
  · rw [exp_bot, pos_iff_ne_zero, ne_eq, exp_eq_zero_iff]
    exact h.ne'
  · induction y
    · simp at h
    · simp_rw [exp_coe]
      exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_strictMono (mod_cast h), Real.exp_pos _⟩
    · simp
  · exact (not_top_lt h).elim

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✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
⊢ Tendsto (fun a ↦ |k a ^ z * f a|) l (𝓝 0)

Tactic:
have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds

Goal state after:
α : 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
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
⊢ Tendsto (fun a ↦ |k a ^ z * f a|) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a b : EReal
hb : 0 ≤ b
h : ⊥ < b
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ m, ⊥ * ↑n ≤ ↑m ∧ ↑m ≤ b * ↑n

Tactic:
refine Eventually.of_forall fun n ↦ ⟨0, ?_, ?_⟩ <;> rw [Nat.cast_zero]
    · apply mul_nonpos_iff.2 -- Split apply and exact for a 0.5s. gain
      exact .inr ⟨bot_le, n.cast_nonneg'⟩
    · positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
by
  by_cases hμ : IsFiniteMeasure (μ.restrict s); swap
  · simp [laverage, not_isFiniteMeasure_iff.mp hμ]
  by_cases hμ0 : μ s = 0
  · rw [laverage, ← setLIntegral_univ]
    exact le_of_eq_of_le (setLIntegral_measure_zero univ f <| by simp [hμ0]) zero_le
  apply le_of_le_of_eq (laverage_mono_ae <| Eventually.filter_mono ae_restrict_le ae_le_essSup)
  have : NeZero (μ.restrict s) :=
    have : NeZero (μ s) := { out := hμ0 }
    restrict.neZero
  exact laverage_const (μ.restrict s) _

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
⊢ ∃ u ⊆ t', u.PairwiseDisjoint B ∧ ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b

Tactic:
have A : ∀ a ∈ t', r a ≤ 1 := by
      intro a ha
      apply ha.2.trans (hR1 (c a))

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
A : ∀ a ∈ t', r a ≤ 1
⊢ ∃ u ⊆ t', u.PairwiseDisjoint B ∧ ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
h : NeZero μ
c : E
⊢ ⨍ (_x : α), c ∂μ = c

Tactic:
rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_one, one_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᵐ[μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ

Tactic:
rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]

Goal state after: