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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
⊢ ∃ x, (s x) a ≠ 0

Tactic:
have a_pos : 0 < ‖a‖ := by simp only [ha, norm_pos_iff, Ne, not_false_iff]

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
⊢ ∃ x, (s x) a ≠ 0
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
H : Type uH
inst✝¹⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹³ : TopologicalSpace M
inst✝¹² : ChartedSpace H M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : IsManifold I ∞ M
inst✝⁹ : SigmaCompactSpace M
inst✝⁸ : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩
x j : M
h_ρjx_ne_zero : (ρ j) x ≠ 0
⊢ s_loc j x ∈ t x

Tactic:
have h_x_in_tsupport_ρj : x ∈ tsupport (ρ j) := subset_closure (mem_support.mpr h_ρjx_ne_zero)

Goal state after:
E : Type uE
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
H : Type uH
inst✝¹⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹³ : TopologicalSpace M
inst✝¹² : ChartedSpace H M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : IsManifold I ∞ M
inst✝⁹ : SigmaCompactSpace M
inst✝⁸ : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩
x j : M
h_ρjx_ne_zero : (ρ j) x ≠ 0
h_x_in_tsupport_ρj : x ∈ tsupport ⇑(ρ j)
⊢ s_loc j x ∈ t x
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
hxK : x ∈ v n
⊢ x ∈ K

Tactic:
exact vK n hxK

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

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)

Tactic:
rwa [uIcc_of_le (by linarith)] at h

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

Goal state before:
pp: a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ IntervalIntegrable (deriv (p - q)) volume a b

Tactic:
apply (hp.intervalIntegrable_deriv.sub hq.intervalIntegrable_deriv).congr_ae

Goal state after:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ (fun x ↦ deriv p x - deriv q x) =ᵐ[volume.restrict (uIoc a b)] deriv (p - q)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case hf
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}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ∃ a ∈ t, (Prod.snd - Prod.fst) a = x_1 ∧ a.1 = x

Tactic:
obtain ⟨δ, hδ₁, hδ₂⟩ := (Metric.tendsto_nhdsWithin_nhds).mp
        (hasDerivAt_iff_tendsto_slope.mp hx.right) η hη

Goal state after:
case hf
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}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ∃ a ∈ t, (Prod.snd - Prod.fst) a = x_1 ∧ a.1 = x
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖(↑n !)⁻¹ * (x - y) ^ n‖ * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C

Tactic:
Real.norm_eq_abs

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ |(↑n !)⁻¹ * (x - y) ^ n| * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
n : ℕ
ih :
  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
⊢ n + 1 ≤ n + 1

Tactic:
by rfl

Goal state after:
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
⊢ Tendsto (fun z ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
let g := fun z ↦ ∑' n, f n * z ^ n

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
⊢ Tendsto (fun z ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
Module: Mathlib.Topology.Order.ExtrClosure

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst✝³] s)
U : Set X
Uo : IsOpen[inst✝³] U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst✝³] s
⊢ ContinuousWithinAt f (U ∩ s) x

Tactic:
· exact (hc _ hxs).mono (inter_subset_right.trans subset_closure)

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

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

Tactic:
simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]

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

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

Tactic:
rw [← cos_zero, eq_comm, cos_eq_cos_iff]

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

Goal state before:
pp: case neg
z : ℂ
h : ∃ k, z = (2 * ↑k + 1) * ↑π / 2
⊢ tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)

Tactic:
tan_add (Or.inr ⟨h, h⟩)

Goal state after:
case neg
z : ℂ
h : ∃ k, z = (2 * ↑k + 1) * ↑π / 2
⊢ (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x - x ^ 3 / 6 ≤ sin x

Tactic:
obtain rfl | hx := hx.eq_or_lt
  · simp
  exact (sin_gt_sub_cube hx).le

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

Goal state before:
pp: case hx₁
x y : ℝ
h : x * y < 1
⊢ arctan (-x) + -arctan y < π / 2

Tactic:
← arctan_neg

Goal state after:
case hx₁
x y : ℝ
h : x * y < 1
⊢ arctan (-x) + arctan (-y) < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ cos y < 1 / √(y ^ 2 + 1)

Tactic:
have hy3 : ↑0 < y ^ 2 + 1 := by linarith [sq_nonneg y]

Goal state after:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
⊢ cos y < 1 / √(y ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * 2⁻¹ / (1 - 2⁻¹ ^ 2)) - arctan 7⁻¹ = π / 4

pp: case h₁
⊢ -1 < 2⁻¹

pp: case h₂
⊢ 2⁻¹ < 1

Tactic:
← arctan_one,

Goal state after:
⊢ arctan (2 * 2⁻¹ / (1 - 2⁻¹ ^ 2)) - arctan 7⁻¹ = arctan 1

case h₁
⊢ -1 < 2⁻¹

case h₂
⊢ 2⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) / (1 - (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) ^ 2)) - arctan 239⁻¹ = π / 4

pp: case h₁
⊢ -1 < 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)

pp: case h₂
⊢ 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2) < 1

pp: case h₁
⊢ -1 < 5⁻¹

pp: case h₂
⊢ 5⁻¹ < 1

Tactic:
← arctan_one,

Goal state after:
⊢ arctan (2 * (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) / (1 - (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) ^ 2)) - arctan 239⁻¹ = arctan 1

case h₁
⊢ -1 < 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)

case h₂
⊢ 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2) < 1

case h₁
⊢ -1 < 5⁻¹

case h₂
⊢ 5⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ 2 * (|x| / 2) = ‖x‖

Tactic:
Real.norm_eq_abs

Goal state after:
x : ℝ
⊢ 2 * (|x| / 2) = |x|
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
hz' : ‖z - c‖ ≠ 0
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
simpa [g', hne, g, div_pow, mul_comm, field] using this

Goal state after:
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ normSq ↑z < 1

Tactic:
rw [← Complex.norm_mul_self_eq_normSq, ← sq]

Goal state after:
z : 𝔻
⊢ ‖↑z‖ ^ 2 < 1
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
⊢ normSq ↑z ≤ 1

Tactic:
rw [← Complex.norm_mul_self_eq_normSq, ← sq]

Goal state after:
z : 𝕔𝔻
⊢ ‖↑z‖ ^ 2 ≤ 1
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
· rw [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← dist_eq_norm_sub,
      ← dist_eq_norm_sub, ← div_eq_inv_mul, div_le_iff₀]
    · exact dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz
    · simpa

Goal state after:
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
U : Set 𝕜
hf : MeromorphicOn f U
⊢ {x | MeromorphicNFAt f x} ∈ Filter.codiscreteWithin U

Tactic:
filter_upwards [hf.analyticAt_mem_codiscreteWithin] with _ ha

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
a✝ : 𝕜
ha : AnalyticAt 𝕜 f a✝
⊢ MeromorphicNFAt f a✝
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 : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ 0 =ᶠ[𝓝[≠] x] 0

Tactic:
by rfl

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

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

Tactic:
meromorphicOrderAt_eq_top_iff

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 0 = 0
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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ meromorphicOrderAt f x = ↑n

Tactic:
rw [meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
(h₁g.zpow h₂g (n := n)).meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt (f ^ n) x).untop₀)
        (by simp_all [zpow_ne_zero])

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
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 ^ n) x = g x ^ n

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

Goal state before:
pp: case pos.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt f₂ x = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff

Goal state after:
case pos.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = 0
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) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff

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 : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
by_cases hf₁ : MeromorphicAt f₁ x; swap
  · have : ¬ MeromorphicAt f₂ x := by
      contrapose hf₁
      exact hf₁.congr hf₁₂.symm
    simp [hf₁, this]
  rw [eq_comm]
  cases h₁f₁ : meromorphicOrderAt f₁ x with
  | top =>
    rw [meromorphicOrderAt_eq_top_iff] at h₁f₁ ⊢
    filter_upwards [hf₁₂, h₁f₁] using by grind
  | coe n =>
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 h₁f₁
    rw [meromorphicOrderAt_eq_int_iff (hf₁.congr hf₁₂)]
    use g, h₁g, h₂g
    filter_upwards [hf₁₂, h₃g] using by grind

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

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hn : analyticOrderAt f x = ⊤
⊢ meromorphicOrderAt f x = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff

Goal state after:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hn : analyticOrderAt f x = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖

Tactic:
classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, ∀ z ∈ ball 0 R, meromorphicOrderAt (canonicalFactor R i ^ (divisor f (ball 0 R)) i) z ≠ ⊤

Tactic:
intro z hz x hx
    rw [meromorphicOrderAt_zpow (meromorphic_canonicalFactor R z x)]
    lift (meromorphicOrderAt (canonicalFactor R z) x) to ℤ using
      (meromorphicOrderAt_canonicalFactor_ne_top z (pos_of_mem_ball hx)) with ℓ
    simp [← WithTop.coe_mul]

Goal state after: