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

Goal state before:
pp: f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := fun E ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1)).PairwiseDisjoint fun i ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ |∫ (x : ℝ) in uIoc (I i).1 (I i).2, f x ∂volume| ≤ ∫ (x : ℝ) in uIoc (I i).1 (I i).2, ‖f x‖ ∂volume

Tactic:
exact abs_integral_le_integral_abs

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

Goal state before:
pp: case inl
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
l : ℤ
⊢ -y ≠ (2 * ↑l + 1) * ↑π / 2

Tactic:
Ne,

Goal state after:
case inl
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
l : ℤ
⊢ ¬-y = (2 * ↑l + 1) * ↑π / 2
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
x : E
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + Function.const E (f c) x‖ = ‖f x‖ + ‖Function.const E (f c) x‖

Tactic:
by simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

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

Goal state before:
pp: x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x ↦ |tan x|) (𝓝[≠] x) atTop

Tactic:
simp only [← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_tan]

Goal state after:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x ↦ ‖Complex.tan ↑x‖) (𝓝[≠] x) atTop
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
⊢ BddAbove (slope f x '' {y | y ∈ s ∧ y < x})

Tactic:
refine bddAbove_iff_subset_Iic.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ y' ∈ Iic (slope f x y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : x * y < 1
| (tan (arctan x) + y) / (1 - tan (arctan x) * y)

Tactic:
← tan_arctan y

Goal state after:
x y : ℝ
h : x * y < 1
| (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: x y : ℂ
⊢ SameRay ℝ x y ↔ (x / y).arg = 0

Tactic:
← Real.Angle.toReal_zero,

Goal state after:
x y : ℂ
⊢ SameRay ℝ x y ↔ (x / y).arg = Real.Angle.toReal 0
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)

Tactic:
by
  have hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) := by
    apply borelCaratheodory_zero (by positivity) (by fun_prop) ?_ hR hz (by simp)
    intro x hx
    simp only [Set.mem_ofPred_eq, sub_re]
    calc (f x).re - (f 0).re ≤ M - (f 0).re := by gcongr; exact hf₁ hx
      _ ≤ M + ‖f 0‖ := by linarith [neg_le_abs (f 0).re, abs_re_le_norm (f 0)]
  have h_denom_ne : R - ‖z‖ ≠ 0 := by linarith [mem_ball_zero_iff.mp hz]
  calc ‖f z‖ ≤ ‖f z - f 0‖ + ‖f 0‖ := norm_le_norm_sub_add _ _
    _ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ := by gcongr
    _ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖) := by field_simp; ring

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩

Tactic:
convert! (isCoveringMap_npow n _).comp_homeomorph (.inv₀ 𝕜)
    · simp [Homeomorph.inv₀]
    · simpa using hn

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] g
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
rw [eventuallyEq_iff_sub] at *

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f - g =ᶠ[codiscreteWithin U] 0
⊢ f - g =ᶠ[𝓝[≠] x] 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∉ U
⊢ (divisor (f₁ + f₂) U)⁻ z ≤ ((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻) z

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
⊢ (divisor (f₁ + f₂) U)⁻ z ≤ ((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻) z

Tactic:
· simp [hz]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
⊢ (divisor (f₁ + f₂) U)⁻ z ≤ ((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∉ U
⊢ (divisor (f₁ • f₂) U) z = (divisor f₁ U + divisor f₂ U) z

Tactic:
· simp [hz]

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ ∅, MeromorphicOn (f i) U
h₂f : ∀ i ∈ ∅, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ divisor (∏ i ∈ ∅, f i) U = ∑ i ∈ ∅, divisor (f i) U

Tactic:
rw [prod_empty, sum_empty]
    exact divisor_ofNat 1

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
z : 𝕜
hn : ¬n = 0
hz : z ∉ U
⊢ (divisor (f ^ n) U) z = (n • divisor f U) z

Tactic:
· simp [hz]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
hn : ¬n = 0
hz : z ∉ U
⊢ (divisor (f ^ n) U) z = (n • divisor f U) z

Tactic:
· simp [hz]

Goal state after:
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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

Tactic:
· suffices 0 ≤ meromorphicOrderAt (f₁ + f₂) x by simp_all
      calc 0
      _ ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) :=
        le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg
      _ ≤ meromorphicOrderAt (f₁ + f₂) x :=
        meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
by_cases h₃f : Function.HasFiniteMulSupport f

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : {σ | f σ x = 0}.Subsingleton
h₃f : Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (∏ᶠ (i : ι), f i) x

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : {σ | f σ x = 0}.Subsingleton
h₃f : ¬Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (∏ᶠ (i : ι), 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
x : 𝕜
f : 𝕜 → E
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

Tactic:
by_cases h₁ : ¬ MeromorphicAt f x

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f 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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h : n₁ < n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
z : 𝕜
h₁z : f₁ z = (z - x) ^ n₁ • g₁ z
h₂z : f₂ z = (z - x) ^ n₂ • g₂ z
h₃z : z ∈ {x}ᶜ
⊢ (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + (z - x) ^ (n₂ - n₁) • g₂) z

Tactic:
simp only [Pi.add_apply, h₁z, h₂z, Pi.smul_apply, smul_add, ← smul_assoc, smul_eq_mul,
      add_right_inj]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h : n₁ < n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
z : 𝕜
h₁z : f₁ z = (z - x) ^ n₁ • g₁ z
h₂z : f₂ z = (z - x) ^ n₂ • g₂ z
h₃z : z ∈ {x}ᶜ
⊢ (z - x) ^ n₂ • g₂ z = ((z - x) ^ n₁ * (z - x) ^ (n₂ - n₁)) • g₂ z
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f

Tactic:
by
  filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with a ha
  rcases ha with ha | ha
  · simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 ha.meromorphicNFAt).symm]
  · simp only [Set.mem_compl_iff] at ha
    simp [toMeromorphicNFOn, ha, hf]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
· simp [meromorphicOrderAt_congr hg₂, hg₁.meromorphicOrderAt_nonneg]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
ih : ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t (n + 1))) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t (n + 1))) ∧ Γ 0 = e

Tactic:
obtain ⟨Γ, cont, eqOn, Γ_0⟩ := ih

Goal state after:
case succ
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t (n + 1))) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t (n + 1))) ∧ Γ 0 = e
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL ↑conjCLE
x✝ : ℂ
⊢ g x✝ = (restrictScalars ℝ map ∘SL ↑conjCLE) x✝

Tactic:
simp only [hmap, ContinuousLinearEquiv.coe_coe, comp_apply, conjCLE_apply,
          starRingEnd_self_apply]

Goal state after:
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
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ (U \ {x | AnalyticAt 𝕜 f x})ᶜ ∈ 𝓝[≠] x

Tactic:
← Filter.eventually_mem_set

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, x ∈ (U \ {x | AnalyticAt 𝕜 f x})ᶜ
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |2⁻¹| = 2⁻¹

Tactic:
rw [abs_of_pos]

Goal state after:
⊢ 0 < 2⁻¹
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
hzx : z - x ≠ 0
⊢ (z - x) ^ n • deriv g z + deriv ((fun x ↦ x ^ n) ∘ fun x_1 ↦ x_1 - x) z • g z =
    (z - x) ^ n • deriv g z + (↑n * (z - x) ^ (n - 1)) • g z

Tactic:
deriv_comp _ (by fun_prop (disch := grind)) (by fun_prop)

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
hzx : z - x ≠ 0
⊢ (z - x) ^ n • deriv g z + (deriv (fun x ↦ x ^ n) (z - x) * deriv (fun x_1 ↦ x_1 - x) z) • g z =
    (z - x) ^ n • deriv g z + (↑n * (z - x) ^ (n - 1)) • g z
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E), ∂_{m} (∂_{c • n} f) = c • ∂_{m} (∂_{n} f)

Tactic:
by simp [lineDerivOp_left_smul, lineDerivOp_smul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ circleAverage f₁ c R = circleAverage f₂ c R

Tactic:
unfold circleAverage
  congr 1
  exact intervalIntegral.integral_congr (fun x ↦ by simp [hf (circleMap_mem_sphere' c R x)])

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : thickening e (closedBall c R) ⊆ {x | HarmonicAt f x}
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
thickening_closedBall h₁e (pos_of_mem_ball hw).le

Goal state after:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: case h₁f
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)

Tactic:
apply ContinuousOn.circleAverage
    · rw [herglotzRieszKernel_fun_def]
      apply (continuousOn_herglotz_riesz hw).smul (hf.2.mono _)
      grind [closure_ball c (pos_of_mem_ball hw).ne', mem_closedBall_iff_norm]
    · grind [norm_nonneg (w - c)]

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑(-x) * I)‖ ≤ C

Tactic:
exact him (-x) (neg_nonpos.2 hx)

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

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ (R ^ 2 - r ^ 2) * (R - r) ≤ (R + r) * (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

Tactic:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]

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

Goal state before:
pp: case hb
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)

Tactic:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]

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

Goal state before:
pp: case hd
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R - r

Tactic:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑(-x) * I)‖ ≤ C

Tactic:
exact him (-x) (neg_nonpos.2 hx)

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

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ |sin x| ≤ |x|

Tactic:
exact abs_sin_le_abs

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

Goal state before:
pp: x : ℝ
⊢ deriv (fun x ↦ (log x)⁻¹) x = -x⁻¹ / log x ^ 2

Tactic:
have := mt (continuousAt (𝕜 := ℝ)) not_continuousAt_inv_log_neg_one
  have := mt (continuousAt (𝕜 := ℝ)) not_continuousAt_inv_log_one
  have := not_differentiableAt_inv_log_zero
  obtain (⟨_, _, _⟩ | rfl | rfl | rfl) :
      (x ≠ -1 ∧ x ≠ 0 ∧ x ≠ 1) ∨ x = -1 ∨ x = 0 ∨ x = 1 := by tauto
  · simp_all
  all_goals rw [deriv_zero_of_not_differentiableAt ‹_›]; simp

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

Goal state before:
pp: x : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
hx₂ : x ≠ -1
⊢ HasDerivAt (fun x ↦ log (log x)) (x⁻¹ / log x) x

Tactic:
simpa using (differentiableAt_log_log hx₀ hx₁ hx₂).hasDerivAt

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

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
⊢ r.re + 1 ≠ 0

Tactic:
Ne,

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re + 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr
a b : ℝ
r : ℂ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0

Tactic:
Ne,

Goal state after:
case inr
a b : ℝ
r : ℂ
h : ¬r = -1 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ↑r ≠ ↑(-1) ∧ 0 ∉ [[a, b]]

Tactic:
Ne,

Goal state after:
case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ¬↑r = ↑(-1) ∧ 0 ∉ [[a, b]]
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in a..b, |x - a| ^ n

Tactic:
rw [uIoc_of_le hab, ← integral_of_le hab]

Goal state after: