mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ pushout.inr f g ▷ Q ≫ (pushoutSymmetry f g).hom ▷ Q = pushout.inl g f ▷ Q

Tactic:
by
  simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
⊢ (finset x hd).Nonempty

Tactic:
by
  obtain ⟨i, hi⟩ := mem_range_left x hd k.succ (by grind)
  exact ⟨i, by simpa using hi⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono j
hi : innerAnodyneExtensions i
⊢ innerAnodyneExtensions sq₁₂.ι

Tactic:
refine (innerAnodyneExtensions.arrow_mk_iso_iff ?_).1
    (innerAnodyneExtensions_pushoutObjObjι sq₁₂.flipTensor hi)

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono j
hi : innerAnodyneExtensions i
⊢ Arrow.mk sq₁₂.flipTensor.ι ≅ Arrow.mk sq₁₂.ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono j
hi : anodyneExtensions i
⊢ anodyneExtensions sq₁₂.ι

Tactic:
refine (anodyneExtensions.arrow_mk_iso_iff ?_).1
    (anodyneExtensions_pushoutObjObjι sq₁₂.flipTensor hi)

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono j
hi : anodyneExtensions i
⊢ Arrow.mk sq₁₂.flipTensor.ι ≅ Arrow.mk sq₁₂.ι
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
refine ⟨c, hc.1, fun k hk ↦ ?_⟩

Goal state after:
case refine_2.inr.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
⊢ (v k) c < 1
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
⊢ IsPathConnected (sphere x r)

Tactic:
have : f '' {0}ᶜ = sphere x r := by
    apply Subset.antisymm
    · rintro - ⟨y, hy, rfl⟩
      have : ‖y‖ ≠ 0 := by simpa using hy
      simp [f, norm_smul, abs_of_nonneg hr, mul_assoc, inv_mul_cancel₀ this]
    · intro y hy
      refine ⟨y - x, ?_, ?_⟩
      · intro H
        simp only [mem_singleton_iff, sub_eq_zero] at H
        simp only [H, mem_sphere_iff_norm, sub_self, norm_zero] at hy
        exact rpos.ne hy
      · simp [f, mem_sphere_iff_norm.1 hy, mul_inv_cancel₀ rpos.ne']

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
this : f '' {0}ᶜ = sphere x r
⊢ IsPathConnected (sphere x r)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inr.inr
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_gt : 1 < (v j) a
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
refine ⟨c, hc.1, fun k hk ↦ ?_⟩

Goal state after:
case refine_2.inr.inr.inr
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_gt : 1 < (v j) a
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
⊢ (v k) c < 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
⊢ ?m.165 ≠ 0

Tactic:
by linarith [h.log_div_log_pos ha₀ ha₁]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
⊢ n ≤ ⋯.choose ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
refine ⟨fun hmn ↦ ⟨fun z ↦ (z - z₀) ^ (m - n) • g z, by fun_prop, ?_⟩, fun ⟨h, hh, hfh⟩ ↦ ?_⟩

Goal state after:
case neg.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
hmn : n ≤ ⋯.choose
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • (fun z ↦ (z - z₀) ^ (m - n) • g z) z

case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
⊢ n ≤ ⋯.choose
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe.a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ 1 ≤ r

Tactic:
by_contra! hr
      have := hfF.self_of_nhds
      simp_all

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
ι : Type u_5
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
⊢ MeromorphicAt (∑ n ∈ s, G n) x

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticAt_const.meromorphicAt
  | insert σ s hσ hind =>
    rw [Finset.sum_insert hσ]
    apply (h σ (Finset.mem_insert_self σ s)).add
      (hind (fun τ hτ ↦ h τ (Finset.mem_insert_of_mem hτ)))

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

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
rw [mul_comm, ← mul_assoc]

Goal state after:
case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = c ^ f x * log c * derivWithin f s x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ (descPochhammer ℤ n).smeval a * (a - ↑n) * (1 + z) ^ (a - ↑n - 1) =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - ↑n - 1)

pp: case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane

Tactic:
· congr
      simp [descPochhammer_succ_right, Polynomial.smeval_mul, Polynomial.smeval_natCast]

Goal state after:
case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑r * ↑(‖p n‖₊ ^ (1 / ↑n)) ≤ 1

Tactic:
← ENNReal.coe_mul,

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑(r * ‖p n‖₊ ^ (1 / ↑n)) ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
rcases ne_or_eq x 0 with (hx | rfl)
  · exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt
  replace h : 1 ≤ p := h.neg_resolve_left rfl
  apply hasDerivAt_of_hasDerivAt_of_ne fun x hx =>
    (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt
  exacts [continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h)),
    continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))]

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

Goal state before:
pp: case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ x.log.exp = x

Tactic:
← ENNReal.ofReal_toReal hx_top,

Goal state after:
case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ (ENNReal.ofReal x.toReal).log.exp = ENNReal.ofReal x.toReal
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ y = (↑y * x.log).exp

Tactic:
by
  rw [← log_rpow, exp_log]

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

Goal state before:
pp: ⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ⊤ b / ↑b = ⊤

Tactic:
exact ⟨1, fun n n_pos ↦ top_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

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

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup v

Tactic:
refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']

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

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthInf (-u) = -linearGrowthSup u

Tactic:
rw [linearGrowthSup, ← liminf_neg]

Goal state after:
u : ℕ → EReal
⊢ linearGrowthInf (-u) = liminf (-fun n ↦ u n / ↑n) atTop
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]

Goal state after:
case refine_1
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ⊥ * ↑n ≤ 0

case refine_2
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ 0 ≤ b * ↑n
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x ↦ 1) =o[l] k
⊢ f =o[l] fun x ↦ k x * k x ^ (z - 1)

Tactic:
simpa using! this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthSup u

Tactic:
have v_0 := hv₀.symm.lt_of_le <| (linearGrowthInf_natCast_nonneg v).trans (liminf_le_limsup)

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthSup u
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf u

Tactic:
have v_0 := hv₀.symm.lt_of_le <| (linearGrowthInf_natCast_nonneg v).trans (liminf_le_limsup)

Goal state after:
case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf u
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : 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)
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
have d_Union (s : ℕ → Set α) (hm : Monotone s) :
    Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n))) := by
    refine Tendsto.sub ?_ ?_ <;>
      refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm
    · exact hμ _
    · exact hν _

Goal state after:
α : 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,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ (linearGrowthSup fun n ↦ u (m * n)) = ↑m * linearGrowthSup u

Tactic:
have : Tendsto (fun n : ℕ ↦ ((m * n : ℕ) : EReal) / n) atTop (𝓝 m) := by
    refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)
    rw [mul_comm, natCast_mul x m, ← mul_div]
    exact mul_div_cancel (natCast_ne_bot x) (natCast_ne_top x) (Nat.cast_ne_zero.2 hx.ne.symm)
  exact h.linearGrowthSup_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ (∫⁻ (x : α), f x ∂μ) / μ univ * μ univ = ∫⁻ (x : α), f x ∂μ

Tactic:
ENNReal.div_mul_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
⊢ ⨍ (x : α), 0 ∂μ = 0

Tactic:
by rw [average, integral_zero]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
⊢ (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ

Tactic:
by
  simpa [laverage_eq] using toReal_laverage hf hf'

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

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x ↦ μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
⊢ d ∈ {d | μ ≤ d + ν} → measure_sub ≤ d

Tactic:
h_d

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x ↦ μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : d ∈ {d | μ ≤ d + ν}
⊢ measure_sub ≤ d
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact (haveLebesgueDecomposition_spec μ ν).2.1

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
⊢ r • μ = ↑r • μ.singularPart ν + ν.withDensity (↑r • μ.rnDeriv ν)

Tactic:
rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
      ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)

Tactic:
rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]

Goal state after: