mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_3
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
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) 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
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ ((x - x✝¹) ^ (n + 1) / ((↑n + 1) * ↑n !)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] x✝¹ =
    (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x✝¹ • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x✝¹

Tactic:
iteratedDerivWithin_succ

Goal state after:
case e'_3
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
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) 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
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ ((x - x✝¹) ^ (n + 1) / ((↑n + 1) * ↑n !)) • derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] x✝¹ =
    (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x✝¹ • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x✝¹
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: 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
a✝³ : ℝ
a✝² : a✝³ ≠ x₀
a✝¹ : a✝³ ≠ x
a✝ : a✝³ ∈ Ι x₀ x
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] a✝³ = deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) a✝³

Tactic:
iteratedDerivWithin_succ

Goal state after:
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
a✝³ : ℝ
a✝² : a✝³ ≠ x₀
a✝¹ : a✝³ ≠ x
a✝ : a✝³ ∈ Ι x₀ x
⊢ derivWithin (iteratedDerivWithin k f [[x₀, x]]) [[x₀, x]] a✝³ =
    deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) a✝³
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|

Tactic:
exact H b a hb ha h (le_of_not_ge hab)

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 → ‖x + y‖ ≠ 2
⊢ StrictConvexSpace ℝ E

Tactic:
refine
    StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
      ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, ?_⟩
  rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne,
    div_eq_one_iff_eq (two_ne_zero' ℝ)]
  exact h hx hy hne

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ^ 2 ≤ 4 - ε ^ 2

Tactic:
sq,

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ * ‖x + y‖ ≤ 4 - ε ^ 2
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: case inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr)

Goal state after:
case inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (fun x ↦ deriv (fun x ↦ x ^ n) x) fun a ↦ interior (fun a ↦ Ici 0 a) a

Tactic:
simp_rw [deriv_pow_field, interior_Ici]

Goal state after:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (fun x ↦ ↑n * x ^ (n - 1)) fun a ↦ Ioi 0 a
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
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
obtain ⟨x, hx_mem, hx_max⟩ := isCompact_closedBall (0 : E) r |>.exists_isMaxOn
    (nonempty_closedBall.mpr hr_nn)
    (h_an.continuousOn.mono <| closedBall_subset_ball hr_lt).norm
  suffices Set.EqOn f (Function.const E (f x)) (ball 0 b) by
    rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]
  apply eq_const_of_exists_max h_an (closedBall_subset_ball hr_lt hx_mem) (fun z hz ↦ ?_)
  obtain ⟨w, hw, hw'⟩ := hr z hz
  exact hw'.trans (hx_max hw)

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

Goal state before:
pp: case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (z + z) = (tan z + tan z) / (1 - tan z ^ 2)

Tactic:
sq,

Goal state after:
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)
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 ^ 2)

Tactic:
sq,

Goal state after:
case neg
z : ℂ
h : ∃ k, z = (2 * ↑k + 1) * ↑π / 2
⊢ tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)
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✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0

Tactic:
refine fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => ?_) hz

Goal state after:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
z : E
hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
w : E
hw : w ∈ frontier U
⊢ ‖(f - g) w‖ ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) = 1 / √(1 + x ^ 2)

Tactic:
rw [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]

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

Goal state before:
pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arctan (x / √(1 - x ^ 2))

Tactic:
arctan_eq_arcsin

Goal state after:
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √(1 - x ^ 2) / √(1 + (x / √(1 - x ^ 2)) ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √(1 - x ^ 2) / √((1 - x ^ 2 + x ^ 2) / (1 - x ^ 2)))

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
div_div

Goal state after:
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / (√(1 - x ^ 2) * √((1 - x ^ 2 + x ^ 2) / (1 - x ^ 2))))

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
⊢ x - x ^ 3 / 6 < sin x

Tactic:
have hmono : StrictMonoOn f (Set.Ici 0) := by
    apply strictMonoOn_of_deriv_pos (convex_Ici 0) (by fun_prop)
    grind [one_sub_sq_div_two_lt_cos, interior_Ici]

Goal state after:
x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
hmono : StrictMonoOn f (Ici 0)
⊢ x - x ^ 3 / 6 < sin x
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ angle x 1 = |x.arg|

Tactic:
by simp [angle_eq_abs_arg, hx]

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

Goal state before:
pp: case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
simp only [hx, hy, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]

Goal state after:
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ False ∨ False ∨ ↑‖y‖ / ↑‖x‖ * x = y
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
simp only [real_inner_self_eq_norm_mul_norm]

Goal state after:
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - ⟪x, y⟫ * ⟪x, y⟫)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h : angle x y = π
⊢ angle x z + angle y z = π

Tactic:
rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
left✝ : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
⊢ angle x z + angle (r • x) z = π
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr.refine_1
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₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
⊢ ‖g' w‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
mem_sphere_iff_norm

Goal state after:
case inr.refine_1
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₁)
w : ℂ
hw : ‖w - c‖ = R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
⊢ ‖g' w‖ ≤ R₂ / R₁ ^ (n + 1)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ ‖deriv f c‖ ≤ R₂ / R₁

Tactic:
rw [norm_deriv_eq_norm_fderiv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ ‖fderiv ℂ f c‖ ≤ R₂ / R₁
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (f ^ n) x

pp: case neg.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
· left
    filter_upwards [hf] with z hz
    simp_all only [Pi.zero_apply, Pi.pow_apply, zero_zpow n hn]

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ MeromorphicNFAt (f ^ n) x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
hu : ¬(MeromorphicOn.divisor f U) u = 0
⊢ u ∈ f ⁻¹' {0}

Tactic:
· rw [Set.mem_preimage, Set.mem_singleton_iff]
      have := h₁f ((MeromorphicOn.divisor f U).supportWithinDomain hu)
        |>.meromorphicOrderAt_eq_zero_iff.not
      simp only [h₁f.meromorphicOn, (MeromorphicOn.divisor f U).supportWithinDomain hu,
        MeromorphicOn.divisor_apply, WithTop.untop₀_eq_zero, not_or] at hu
      simp_all [hu.1]

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
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
  · exact (hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx).trans (hf x hx).eq_nhdsNE_toMeromorphicNFAt
  · simp [toMeromorphicNFOn, hf, hx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport fun u ↦ (x - u) ^ d u) ⊆ ↑(Finite.toFinset h₁)
⊢ ∏ i ∈ Finite.toFinset h₁, (x - i) ^ update d x 0 i = ∏ᶠ (u : 𝕜), (x - u) ^ d u

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport fun u ↦ (x - u) ^ d u) ⊆ ↑(Finite.toFinset h₁)
⊢ ∀ x_1 ∈ Finite.toFinset h₁, (x - x_1) ^ update d x 0 x_1 = (x - x_1) ^ d x_1
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ 0 ≤ divisor g U

Tactic:
divisor_of_toMeromorphicNFOn (hφ.inv.smul h₁f),

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ 0 ≤ divisor (φ⁻¹ • f) U
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case zero
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
⊢ (p ∘ fun x ↦ e) 0 = γ 0

Tactic:
exact γ_0.symm

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

Goal state before:
pp: case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ IsOpen[instTopologicalSpaceSubtype] {u | meromorphicOrderAt f ↑u = ⊤}

Tactic:
· apply isOpen_iff_forall_mem_open.mpr
    intro z hz
    conv =>
      arg 1; intro; left; right; arg 1; intro
      rw [meromorphicOrderAt_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
    simp only [mem_ofPred_eq] at hz
    rw [meromorphicOrderAt_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at hz
    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
    use Subtype.val ⁻¹' t'
    simp only [mem_compl_iff, mem_singleton_iff, isOpen_induced h₂t', mem_preimage,
      h₃t', and_self, and_true]
    intro w hw
    simp only [mem_ofPred_eq]
    -- Trivial case: w = z
    by_cases h₁w : w = z
    · rw [h₁w]
      tauto
    -- Nontrivial case: w ≠ z
    use t' \ {z.1}, fun y h₁y _ ↦ h₁t' y (mem_of_mem_sdiff h₁y) (mem_of_mem_inter_right h₁y)
    constructor
    · exact h₂t'.sdiff isClosed_singleton
    · apply (mem_sdiff w).1
      exact ⟨hw, mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
x : ℝ
⊢ 0 < ε + sSupNormIm f x

Tactic:
by
  linarith [sSupNormIm_nonneg f x]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖invInterpStrip f z ε‖ = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
simp only [invInterpStrip, norm_mul]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (z - 1)‖ * ‖(↑ε + ↑(sSupNormIm f 1)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1))

Tactic:
by_cases hM0_one : 1 ≤ ε + sSupNormIm f 0
    -- `1 ≤ sSupNormIm f 0`
    · apply le_trans _ (le_max_left _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
        one_re, Real.rpow_le_one_of_one_le_of_nonpos hM0_one (sub_nonpos.mpr hset.2)]
    -- `0 < sSupNormIm f 0 < 1`
    · rw [not_le] at hM0_one; apply le_trans _ (le_max_right _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
        one_re]
      apply Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 0) (le_of_lt hM0_one) _
      simp only [neg_le_sub_iff_le_add, le_add_iff_nonneg_left, hset.1]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
H : Tendsto (fun R ↦ δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0))
⊢ Tendsto (fun R ↦ δ * expR (d * R) + B * expR (c * R) + Real.log A) atTop atBot

Tactic:
rw [mul_zero, add_zero] at H

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
H : Tendsto (fun R ↦ δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 δ)
⊢ Tendsto (fun R ↦ δ * expR (d * R) + B * expR (c * R) + Real.log A) atTop atBot
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case calc_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ I₁ + I • I₂ - (↑w.re - ↑z.re + (↑w.im - ↑z.im) * I) • f z =
    I₁ - (↑w.re - ↑z.re) • f z + I • (I₂ - (↑w.im - ↑z.im) • f z)

Tactic:
rw [add_smul, smul_sub, smul_smul, mul_comm I]; abel

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ0' : μ s ≠ 0
c : ℝ
hc : c ∈ uIoo a b
heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
exact ⟨c, hc, by rwa [← setAverage_congr hs_ev]⟩

Goal state after: