mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := ⋯
B : s = ⋃ n, t n
⊢ Monotone t

Tactic:
intro m n hmn

Goal state after:
case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
B : s = ⋃ n, t n
m n : ℕ
hmn : m ≤ n
⊢ t m ⊆ t n
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
b : β
hb : b ∈ Ioi (f a)
h2f : b ∉ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
⊢ BddAbove (f '' Ici a)

Tactic:
suffices ∀ i, a ≤ i → f i < b from ⟨b, by aesop (add simp [upperBounds, le_of_lt])⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
b : β
hb : b ∈ Ioi (f a)
h2f : b ∉ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
⊢ ∀ (i : α), a ≤ i → f i < b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:

Tactic:
_ = liminf (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (x : ℝ) in Icc a b, (G (n : ℝ)⁻¹) x)) atTop := by
        apply Filter.liminf_congr
        filter_upwards with n
        rw [← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm (G_integrable n)]
        congr with y
        exact abs_eq_self.mpr (hg.monotoneOn univ |>.slope_nonneg trivial trivial)
      _ ≤ ENNReal.ofReal (g b - g a) := by
        refine Filter.liminf_le_of_frequently_le'
          (Filter.Frequently.of_forall fun n ↦ ENNReal.ofReal_le_ofReal ?_)
        rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab]
        convert!
          hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegral_slope_le hab (by simp) using 2
        simp [g]
      _ = ENNReal.ofReal (f b - f a) := by grind

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ENNReal.ofReal (∫ (x : ℝ) in Icc a b, ‖deriv f x‖ ∂volume) ≤ ENNReal.ofReal (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
ENNReal.ofReal_le_ofReal_iff (by linarith),

Goal state after:
case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in Icc a b, ‖deriv f x‖ ∂volume ≤ f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
⊢ ∃ u,
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint fun z ↦ Icc z.1 z.2) ∧ HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)

Tactic:
obtain ⟨u, ⟨hu₁, hu₂, hu₃, hu₄⟩⟩ : ∃ u ⊆ t, u.Countable ∧
      u.PairwiseDisjoint (fun z ↦ Icc z.1 z.2) ∧ volume (s \ ⋃ z ∈ u, Icc z.1 z.2) = 0 := by
    apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
    · grind [Metric.closedBall, Real.dist_eq, Pi.sub_apply, abs_le']
    · intro A hA
      simp only [Pi.sub_apply, Real.volume_closedBall, ENNReal.coe_ofNat, Real.volume_Icc]
      rw [show 6 = ENNReal.ofReal 6 by norm_num, ← ENNReal.ofReal_mul (by norm_num),
          ENNReal.ofReal_le_ofReal_iff (by grind)]
      linarith
    · simp +contextual [t]
    · simp [isClosed_Icc]
    · intro x hx
      apply Eventually.frequently
      have := hasDerivAt_iff_tendsto_slope.mp hx.right
      obtain ⟨δ, hδ₁, hδ₂⟩ := (Metric.tendsto_nhdsWithin_nhds).mp
        (hasDerivAt_iff_tendsto_slope.mp hx.right) η hη
      have evn_bound {α : ℝ} (hα : 0 < α) : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α := by
        rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
        exact ⟨Ioo (-α) α, by grind, isOpen_Ioo, by grind⟩
      have evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε :=
        eventually_mem_of_tendsto_nhdsWithin (fun _ a ↦ a)
      filter_upwards [evn_pos, evn_bound hη, evn_bound hδ₁,
                      evn_bound (α := (b - x) / 2) (by simp [hx.left.right])]
        with ε hε₁ hε₂ hε₃ hε₄
      refine ⟨(x, x + ε), ⟨⟨hx.1.1, by linarith, by linarith⟩, ?_⟩, by simp, rfl⟩
      exact hδ₂ (by grind) (by simp [abs_eq_self.mpr hε₁.le, hε₃])

Goal state after:
case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : u ⊆ t
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₄ : volume (s \ ⋃ z ∈ u, Icc z.1 z.2) = 0
⊢ ∃ u,
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint fun z ↦ Icc z.1 z.2) ∧ HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
this✝ : Countable ↑u
this : Pairwise (Disjoint on fun z ↦ Icc (↑z).1 (↑z).2)
hu₄ : volume (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) = 0
vol_sum : ∑' (a : ↑u), (ENNReal.ofReal ((↑a).2 - (↑a).1)).toReal = b - d
⊢ Summable fun a ↦ (ENNReal.ofReal ((↑a).2 - (↑a).1)).toReal

Tactic:
by grind [tsum_def]

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.succ
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
n : ℕ
ih :
  (∀ k ≤ n,
      let u := fun t ↦ (x - t) ^ k / ↑k !;
      let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
      ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t) →
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ f x - taylorWithinEval f (n + 1) [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / ↑(n + 1)!) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: case succ
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  (∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑n + 1) f (x + t • y)) →
    f (x + y) =
      (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
        (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
⊢ f (x + y) =
    (∑ k ∈ Finset.range (n + 1 + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑(n + 1)!)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ (n + 1) • (iteratedFDeriv ℝ (n + 1 + 1) f (x + t • y)) fun x ↦ y

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.hv'.h
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] =ᵐ[MeasureTheory.volume.restrict (Ι x₀ x)]
    deriv fun t ↦ iteratedDerivWithin k f [[x₀, x]] t

Tactic:
rw [Filter.EventuallyEq, MeasureTheory.ae_restrict_iff' (by measurability)]
      filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _
      rw [iteratedDerivWithin_succ]
      grind [derivWithin_of_mem_nhds, Icc_mem_nhds, uIcc]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ Set.InjOn Norm.norm {y | SameRay ℝ x y}

Tactic:
rintro y hy z hz h
  rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩
  rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩
  rw [norm_smul, norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr,
    norm_of_nonneg hs] at h
  rw [h]

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: case inl
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x = z
hy : y = z
⊢ a • x + b • y ∈ ball z 0

Tactic:
exact (hne (hx.trans hy.symm)).elim

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case inr.x
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := ⋯
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a + ↑i * δ' ≤ a + (↑i + 1) * δ'

Tactic:
convert! h_mono (show i ≤ i + 1 by lia)

Goal state after:
case e'_4.e'_6
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ ↑i + 1 = ↑(i + 1)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
⊢ Tendsto (fun z ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
rw [Metric.tendsto_nhdsWithin_nhds]

Goal state after:
case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ ≤ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
simp_rw [← norm_pow, ← norm_mul, norm_sum_le]

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

Goal state before:
pp: case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ ≤ ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
simp_rw [← norm_pow, ← norm_mul, norm_sum_le]

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

Goal state before:
pp: ⊢ ContinuousOn tan {x | cos x ≠ 0}

Tactic:
suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0} by
    have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
    rwa [h_eq] at this

Goal state after:
⊢ ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
rcases le_or_gt y 0 with hy | hy

Goal state after:
case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2

case inr
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

pp: case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
· simp [hy]

Goal state after:
case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (angle x y) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
by
  unfold angle
  rw [Real.sin_arccos]
  nth_rw 2 [← Real.sqrt_sq (mul_nonneg (norm_nonneg x) (norm_nonneg y))]
  rw [← Real.sqrt_mul' _ (by positivity), sq]
  rcases eq_or_ne x 0 with (rfl | hx); · simp
  rcases eq_or_ne y 0 with (rfl | hy); · simp
  simp only [real_inner_self_eq_norm_mul_norm]
  field_simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
⊢ sin (angle x (x + y)) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)

Tactic:
rw [sin_angle hx hy]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
⊢ √(⟪x, x⟫ * ⟪x + y, x + y⟫ - ⟪x, x + y⟫ * ⟪x, x + y⟫) / (‖x‖ * ‖x + y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
· ext; simp [NeZero.ne]

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ Continuous (U.domRestrict (U.piecewise (fun x ↦ cexp (f x / ↑n)) fun x ↦ g x ^ (1 / ↑n)))

Tactic:
domRestrict_piecewise,

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ Continuous (U.domRestrict fun x ↦ cexp (f x / ↑n))
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∈ V
⊢ ((divisor f U).restrict hV) x = (divisor f V) x

Tactic:
rw [Function.locallyFinsuppWithin.restrict_apply]
    simp [hf, hx, hf.mono_set hV, hV hx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x

Tactic:
have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : AnalyticAt 𝕜 f x
h₂ : f x ≠ 0
⊢ meromorphicTrailingCoeffAt f x = f x

Tactic:
rw [h₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0) h₂]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : AnalyticAt 𝕜 f x
h₂ : f x ≠ 0
⊢ f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ 0 • f z
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicTrailingCoeffAt (fun x ↦ 0) x = 0

Tactic:
apply MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicOrderAt (fun x ↦ 0) x = ⊤
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : ¬meromorphicOrderAt f₁ x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f₁ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g z
⊢ g x = meromorphicTrailingCoeffAt f₂ x

Tactic:
h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g (h.symm.trans h₃g)

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : ¬meromorphicOrderAt f₁ x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f₁ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g z
⊢ g x = g x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : ((z - x) ^ Exists.choose hf * (z - x) ^ n) • g z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ (z - x) ^ Exists.choose hf * (z - x) ^ n ≠ 0

Tactic:
exact mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz)) (zpow_ne_zero _ (sub_ne_zero.mpr hz))

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

Goal state before:
pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : meromorphicOrderAt f x = ↑n
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o with ⟨g, g_an, gx, hg⟩
    lift n to ℕ using by simpa [h'o] using ho.le
    have : (0 : E) = (x - x) ^ n • g x := by
      have : 0 < n := by simpa [h'o] using ho
      simp [zero_pow_eq_zero.2 this.ne']
    rw [this]
    have : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x := by fun_prop
    apply this.continuousWithinAt.tendsto.congr'
    filter_upwards [hg] with y hy using by simp [hy]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
h : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicTrailingCoeffAt (f ∘ g) x = 0

Tactic:
apply MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
h : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤