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

Goal state before:
pp: case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
rw [h, neg_div, ← div_neg, neg_mul, neg_neg]

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2) + ∑ z ∈ u_coe x, dist (f z.1) (f z.2))
    atTop (𝓝 y)
s : Finset ↑u
⊢ dist (f d) (f b) ≤ dist (f ((T s).2 0).1) (f ((T s).2 (u_coe s).card).2)

Tactic:
simp [T]

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

Goal state before:
pp: case inr.hg
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk : k ≤ n
⊢ AbsolutelyContinuousOnInterval (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x

Tactic:
rcases hk.eq_or_lt with rfl | hk
    · exact hf₂
    replace hf₁ := hf₁.of_le (m := k.succ) (by norm_cast)
    grind [ContDiffOn.absolutelyContinuousOnInterval, uniqueDiffOn_uIcc,
      contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin]

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
| Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))

Tactic:
enter [1, n]
      rw [← mul_add, ← sum_add_distrib]
      enter [2, 2, i]
      rw [← add_mul, sub_add_sub_cancel]

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n i : ℕ
| (l - ∑ k ∈ range (i + 1), f k) * z ^ i
Module: Mathlib.Analysis.Convex.StrictConvexSpace

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

Tactic:
by
  rcases eq_or_ne r 0 with (rfl | hr)
  · rw [closedBall_zero, mem_singleton_iff] at hx hy
    exact (hne (hx.trans hy.symm)).elim
  · simp only [← interior_closedBall _ hr] at hx hy ⊢
    exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
div_eq_inv_mul,

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
div_eq_inv_mul,

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
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
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖x‖ / r ≤ 1
y : E
hy : ‖y‖ / r ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r

Tactic:
div_eq_inv_mul,

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 - δ
x : E
hx : r⁻¹ * ‖x‖ ≤ 1
y : E
hy : r⁻¹ * ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: 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
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖1 - z‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖1 - z‖ * (F + 1) < ε / 4

Tactic:
lt_div_iff₀ (by positivity)

Goal state after:
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
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖1 - z‖ * (F + 1) < ε / 4
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖1 - z‖ * (F + 1) < ε / 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ

Tactic:
tan,

Goal state after:
θ : ℂ
⊢ sin θ / cos θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ
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
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
tan,

Goal state after:
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)
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‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x ↦ ‖f x‖) (closedBall 0 r) x
this : EqOn f (Function.const E (f x)) (ball 0 b)
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
by
    rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]

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

Goal state before:
pp: z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan z = (tan ↑z.re + tanh ↑z.im * I) / (1 - tan ↑z.re * tanh ↑z.im * I)

Tactic:
by
  convert! tan_add_mul_I h; exact (re_add_im z).symm

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

Goal state before:
pp: x : ℝ
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  case inl => simp
  case inr => exact (one_sub_sq_div_two_lt_cos hx).le

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

Goal state before:
pp: ⊢ arctan (1 / √3) = π / 6

Tactic:
← tan_pi_div_six,

Goal state after:
⊢ arctan (tan (π / 6)) = π / 6
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2

Tactic:
rw [sub_lt_self_iff, ← arctan_zero]
    exact tanOrderIso.symm.strictMono h

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

Goal state before:
pp: x y : ℝ
⊢ |cos x - cos y| ≤ |x - y|

Tactic:
simpa [edist_dist] using! lipschitzWith_cos x y

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

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ angle x y / (π / 2) ≤ ‖x - y‖

Tactic:
div_eq_inv_mul,

Goal state after:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ (π / 2)⁻¹ * angle 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 : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ angle x y = 0

Tactic:
refine ⟨fun h => ?_, inner_eq_mul_norm_of_angle_eq_zero⟩
  have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
  rw [angle, h, div_self h₁, Real.arccos_one]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖

Tactic:
calc
    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
    _ = ‖x‖ * ‖y‖ := by ring

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

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

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

Tactic:
· simp [hz, ← exp_nat_mul, mul_div_cancel₀ (b := ↑n) (f z) (mod_cast hn), ← hf hz,
        Function.comp_apply]

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
hz : z ∉ U
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn✝ : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
hmem : 1 ∈ ball 0 (R₁ / dist z c)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
rw [map_sub] at hgf

Goal state after:
case inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn✝ : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z) - g (f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
hmem : 1 ∈ ball 0 (R₁ / dist z c)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2.refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a✝ : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a✝)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a✝ ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
N : Set A
haN : a✝ ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a✝} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a✝} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
a : A
ha : a ∈ N
⊢ (t n, a).1 ∈ Set.Icc 0 (t n)

Tactic:
rw [← t_0]

Goal state after:
case refine_2.refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a✝ : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a✝)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a✝ ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
N : Set A
haN : a✝ ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a✝} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a✝} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
a : A
ha : a ∈ N
⊢ (t n, a).1 ∈ Set.Icc (t 0) (t n)
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
convert! meromorphicNFAt_prod h₁f h₂f
  exact (Finset.prod_apply _ s f).symm

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
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0

Tactic:
by
  constructor
  · intro h
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h
    filter_upwards [h₃g, self_mem_nhdsWithin, eventually_nhdsWithin_of_eventually_nhds
      ((h₁g.continuousAt.ne_iff_eventually_ne continuousAt_const).mp h₂g)]
    simp_all [zpow_ne_zero, sub_ne_zero]
  · simp_all [meromorphicOrderAt_eq_top_iff, Eventually.frequently]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ u ∈ Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u

Tactic:
simp_all only [mem_mulSupport, ne_eq, ne_iff]

Goal state after:
case mpr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ ∃ a, ¬((fun x ↦ x - u) ^ d u) a = 1 a
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
⊢ (∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ (∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x

Tactic:
· simp only [← not_lt, ho, not_true_eq_false, iff_false, not_exists]
    intro c hc
    apply not_tendsto_atTop_of_tendsto_nhds hc.norm
    rw [tendsto_norm_atTop_iff_cobounded]
    exact tendsto_cobounded_of_meromorphicOrderAt_neg ho

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ (∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
⊢ meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    apply meromorphicTrailingCoeffAt_const
  | insert σ s₁ hσ hind =>
    have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
    rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]

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

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w - meromorphicOrderAt (fun z ↦ ↑R * (z - w)) w = -1

Tactic:
fun_meromorphicOrderAt_mul (by fun_prop) (by fun_prop)

Goal state after:
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w -
      (meromorphicOrderAt (fun z ↦ ↑R) w + meromorphicOrderAt (fun z ↦ z - w) w) =
    -1
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (canonicalFactor R w) w = -1

Tactic:
by
  unfold canonicalFactor
  rw [fun_meromorphicOrderAt_div (by fun_prop) (by fun_prop),
    fun_meromorphicOrderAt_mul (by fun_prop) (by fun_prop)]
  have : meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w = 0 := by
    refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_
    · apply AnalyticAt.meromorphicNFAt
      fun_prop
    · rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]
      rw [mem_ball_iff_norm, sub_zero] at h
      grind
  simp [this, meromorphicOrderAt_const, (pos_of_mem_ball h).ne',
    meromorphicOrderAt_id_sub_const]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
hx : (fun x ↦ ↑(D u) * log ‖x - u‖) = 0
y : 𝕜
hy : 1 < ‖y‖
⊢ D u = 0

Tactic:
have := congrFun hx (y + u)

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
hx : (fun x ↦ ↑(D u) * log ‖x - u‖) = 0
y : 𝕜
hy : 1 < ‖y‖
this : ↑(D u) * log ‖y + u - u‖ = 0 (y + u)
⊢ D u = 0