mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
by
  wlog hab : a ≤ b generalizing a b with h
  · specialize h (uIcc_comm a b ▸ hf) (by linarith)
    have : f b ≤ f a := hf (by simp) (by simp) (by linarith)
    rw [intervalIntegral.integral_symm, uIcc_of_ge (by linarith)]
    refine neg_mem_Icc_iff.mpr ?_
    simp only [neg_zero, neg_sub]
    rwa [uIcc_of_le (by linarith)] at h
  rw [uIcc_of_le hab] at hf
  obtain ⟨G, hGf, hG, hG'⟩ := hf.exists_tendsto_deriv_liminf_lintegral_enorm_le hab
  have hG'₀ : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤ :=
    lt_of_le_of_lt hG' ENNReal.ofReal_lt_top |>.ne_top
  have integrable_f_deriv := integrable_of_tendsto hGf hG hG'₀
  rw [MeasureTheory.ae_restrict_iff' (by simp)] at hGf
  rw [← uIcc_of_le hab] at hGf hG hG'
  have : f a ≤ f b := hf (by simp [hab]) (by simp [hab]) hab
  rw [uIcc_of_le (by linarith), mem_Icc]
  have f_deriv_nonneg {x : ℝ} (hx : x ∈ Ioo a b) : 0 ≤ deriv f x := by
    rw [← derivWithin_of_mem_nhds (Icc_mem_nhds hx.left hx.right)]
    exact hf.derivWithin_nonneg
  constructor
  · apply intervalIntegral.integral_nonneg_of_ae_restrict hab
    rw [Filter.EventuallyLE, ← restrict_Ioo_eq_restrict_Icc,
      MeasureTheory.ae_restrict_iff' measurableSet_Ioo]
    exact Filter.Eventually.of_forall @f_deriv_nonneg
  · have ebound := lintegral_enorm_le_liminf_of_tendsto
      ((MeasureTheory.ae_restrict_iff' (by measurability) |>.mpr hGf))
      (fun n ↦ (hG n).aemeasurable.enorm)
    grw [hG'] at ebound
    rw [uIcc_of_le hab,
        ← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm integrable_f_deriv,
        ENNReal.ofReal_le_ofReal_iff (by linarith),
        integral_Icc_eq_integral_Ioc,
        ← intervalIntegral.integral_of_le hab] at ebound
    convert! ebound using 1
    refine intervalIntegral.integral_congr_uIoo ?_
    rw [uIoo_of_le hab]
    intro x hx
    exact Eq.symm <| abs_eq_self.mpr <| f_deriv_nonneg hx

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E}, HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (↑i * (x - x₀) ^ (i - 1) * 1)) • c') x
i : ℕ
a✝ : i ∈ Finset.range (n + 1)
⊢ ((↑(i + 1)!)⁻¹ * (↑(i + 1) * (x - x₀) ^ (i + 1 - 1) * 1)) • iteratedDerivWithin (i + 1) f s x₀ =
    ((↑i !)⁻¹ * (x - x₀) ^ i) • iteratedDerivWithin i (derivWithin f s) s x₀

Tactic:
rw [← iteratedDerivWithin_succ']

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E}, HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (↑i * (x - x₀) ^ (i - 1) * 1)) • c') x
i : ℕ
a✝ : i ∈ Finset.range (n + 1)
⊢ ((↑(i + 1)!)⁻¹ * (↑(i + 1) * (x - x₀) ^ (i + 1 - 1) * 1)) • iteratedDerivWithin (i + 1) f s x₀ =
    ((↑i !)⁻¹ * (x - x₀) ^ i) • iteratedDerivWithin (i + 1) f s x₀
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 ℝ
h : StrictConvex 𝕜 (closedBall 0 1)
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall 0 r)

Tactic:
by simpa only [smul_unitClosedBall_of_nonneg hr.le] using h.smul r

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
⊢ StrictConvexSpace ℝ E

Tactic:
by
  refine StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
    ((convex_closedBall _ _).strictConvex ?_)
  simp only [interior_closedBall _ one_ne_zero, closedBall_sdiff_ball, Set.Pairwise,
    frontier_closedBall _ one_ne_zero, mem_sphere_zero_iff_norm]
  intro x hx y hy hne
  rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩
  exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩

Goal state after:
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, I).1
h_subset : uIoc (I i).1 (I i).2 ⊆ uIoc a b
⊢ Integrable (fun x ↦ ‖f x‖) (volume.restrict (uIoc (I i).1 (I i).2))

Tactic:
exact IntegrableOn.mono_set h.def'.norm h_subset |>.integrable

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

Goal state before:
pp: x : ℂ
⊢ sin x = -1 ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x

Tactic:
rw [← neg_eq_iff_eq_neg, ← cos_add_pi_div_two, cos_eq_one_iff]

Goal state after:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x + ↑π / 2) ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inl
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ sin (x + y) / cos (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
sin_add,

Goal state after:
case inl
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y + cos x * sin y) / cos (x + y) = (tan x + tan y) / (1 - tan x * tan y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: z w : ℂ
⊢ cos z = w ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
by
  rw [← sub_eq_zero]
  simpa [field, cos, exp_neg] using Eq.congr (by ring) rfl

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

Goal state before:
pp: case inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ π / 2 ≤ (2 * ↑r + 1) * π / 2

Tactic:
← one_mul (π / 2),

Goal state after:
case inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 * (π / 2) ≤ (2 * ↑r + 1) * π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ (2 * ↑r + 1) * π / 2 ≤ -(π / 2)

Tactic:
← one_mul (π / 2),

Goal state after:
case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ (2 * ↑r + 1) * π / 2 ≤ -(1 * (π / 2))
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ deriv f y = f' y

Tactic:
by rw [this hy]

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

Goal state before:
pp: case inl
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ sin x ^ 2 < x ^ 2

pp: case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
case inl =>
    exact pow_lt_pow_left₀ (sin_lt hx₀)
      (sin_nonneg_of_nonneg_of_le_pi hx₀.le (by linarith [two_le_pi])) (by simp)

Goal state after:
case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ deriv f y = f' y

Tactic:
by rw [this hy]

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * π / 2 < π / 2
⊢ False

Tactic:
← one_mul (π / 2),

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * π / 2 < 1 * (π / 2)
⊢ False
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case hdb
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ 1 - ‖w‖ ≤ ‖1 + w‖

Tactic:
← norm_one (α := ℂ)

Goal state after:
case hdb
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖1‖ - ‖w‖ ≤ ‖1 + w‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (abs_nonneg (‖x‖ - ‖y‖)), norm_sub_pow_two_real,
    inner_eq_mul_norm_of_angle_eq_zero h, sq_abs (‖x‖ - ‖y‖)]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 - 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

Tactic:
simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]
      congr 1
      apply meromorphicOrderAt_congr
      simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
        disjoint_principal_right] at h₁
      have : U ∈ 𝓝[≠] x := by
        apply mem_nhdsWithin.mpr
        use U, h₂, hx, Set.inter_subset_left
      filter_upwards [this, h₁ x hx] with a h₁a h₂a
      simp only [Set.mem_compl_iff, Set.mem_sdiff, Set.mem_ofPred_eq, not_and] at h₂a
      tauto

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

Goal state before:
pp: 𝕜 : 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
⊢ (divisor (f₁ + f₂) U)⁻ ≤ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻

Tactic:
by
  intro z
  by_cases! hz : z ∉ U
  · simp [hz]
  simp only [Function.locallyFinsuppWithin.negPart_apply, Function.locallyFinsuppWithin.max_apply]
  by_cases hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤
  · simp [divisor_apply (hf₁.add hf₂) hz, hf₁₂, negPart_nonneg]
  rw [← negPart_min]
  apply ((le_iff_posPart_negPart _ _).1 (min_divisor_le_divisor_add hf₁ hf₂ hz hf₁₂)).2

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

Goal state before:
pp: case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
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 g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g

Tactic:
use n, g, h₁g, h₂g

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ (divisor (fun x ↦ x - z₀) U) x = 0

Tactic:
rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) hu,
      ← untop₀_coe 0]
    congr
    exact (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr
      ⟨(· - z₀), analyticAt_id.fun_sub analyticAt_const, by simp [sub_ne_zero_of_ne hx]⟩

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
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 g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ toMeromorphicNFAt f x =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g

Tactic:
use n, g, h₁g, h₂g

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
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
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case h₂
𝕜 : 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 = toMeromorphicNFAt f x x

Tactic:
simp [toMeromorphicNFOn, hf, hx]

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

Goal state before:
pp: case neg
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
hw : w ∉ ball 0 R
⊢ MeromorphicNFOn (canonicalFactor R w ^ F w) (ball 0 R)

Tactic:
· simp only [hw, not_false_eq_true, locallyFinsuppWithin.apply_eq_zero_of_notMem, zpow_zero]
      exact analyticOnNhd_const.meromorphicNFOn

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

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
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ log ‖meromorphicTrailingCoeffAt f x‖ = ∑ᶠ (u : 𝕜), ↑(D u) * log ‖x - u‖ + log ‖g x‖

Tactic:
meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
        (((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).smul h₁g.meromorphicAt)
          h₁x h₂x h),

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ log ‖meromorphicTrailingCoeffAt ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) x‖ =
    ∑ᶠ (u : 𝕜), ↑(D u) * log ‖x - u‖ + log ‖g x‖
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a b : Circle
⊢ (rotation a).trans (rotation b) = rotation (b * a)

Tactic:
ext1
  simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g

Tactic:
· unfold φ
        rw [finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀]
        · filter_upwards [codiscreteWithin_mono (by tauto) η₀.compl_mem_codiscrete,
            self_mem_codiscreteWithin (closedBall 0 R)] with a ha h₂a
          simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply]
          rw [← smul_assoc, ← Finset.prod_smul, Finset.prod_eq_one, one_smul]
          intro x hx
          rw [smul_eq_mul, ← zpow_add', neg_add_cancel, zpow_zero]
          simp_all only [ne_eq, Subtype.forall, mem_closedBall, dist_zero_right,
            locallyFinsuppWithin.support_neg, mem_compl_iff, mem_support, Decidable.not_not,
            Finite.mem_toFinset, neg_add_cancel, not_true_eq_false, neg_eq_zero, and_self, or_self,
            or_false]
          apply canonicalFactor_ne_zero _ (by simp_all) (by grind)
          by_contra h
          simp_all

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z ↦ expR (B * expR (c * |u z|))

Tactic:
refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ (f - g) =O[l] fun z ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ ∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)

Tactic:
refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ (f - g) =O[cobounded ℂ ⊓ l] fun z ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
x y : X
γ✝ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
he : ∀ (γ : Path x y), γ 0 = p ↑e
g : (γ : Path x y) → Path.Homotopic.Quotient (↑e) ((cov.liftPath ↑γ ↑e ⋯) 1) :=
  fun γ ↦ Path.Homotopic.Quotient.mk { toContinuousMap := cov.liftPath ↑γ ↑e ⋯, source' := ⋯, target' := ⋯ }
_i : Setoid (Path x y) := Path.Homotopic.setoid x y
γ γ' : Path x y
hγ : γ ≈ γ'
⊢ g γ = Path.Homotopic.Quotient.mk ({ toContinuousMap := cov.liftPath ↑γ' ↑e ⋯, source' := ⋯, target' := ⋯ }.cast ⋯ ⋯)

Tactic:
Path.Homotopic.Quotient.eq

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
x y : X
γ✝ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
he : ∀ (γ : Path x y), γ 0 = p ↑e
g : (γ : Path x y) → Path.Homotopic.Quotient (↑e) ((cov.liftPath ↑γ ↑e ⋯) 1) :=
  fun γ ↦ Path.Homotopic.Quotient.mk { toContinuousMap := cov.liftPath ↑γ ↑e ⋯, source' := ⋯, target' := ⋯ }
_i : Setoid (Path x y) := Path.Homotopic.setoid x y
γ γ' : Path x y
hγ : γ ≈ γ'
⊢ { toContinuousMap := cov.liftPath ↑γ ↑e ⋯, source' := ⋯, target' := ⋯ }.Homotopic
    ({ toContinuousMap := cov.liftPath ↑γ' ↑e ⋯, source' := ⋯, target' := ⋯ }.cast ⋯ ⋯)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ Path.Homotopic.Quotient.mk (γ₀.map ⋯) = Path.Homotopic.Quotient.mk (γ₁.map ⋯) →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁

Tactic:
Path.Homotopic.Quotient.eq

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁

Tactic:
Path.Homotopic.Quotient.eq

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → γ₀.Homotopic γ₁