mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
k : ℕ
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))

Tactic:
rcases le_or_gt m k with hmk | hmk

Goal state after:
case succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))

case succ.inr
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : ↑k < m
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
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
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩
  exact nhds_basis_closedBall.eventually_iff.2
    ⟨r, hr₀, norm_eqOn_closedBall_of_isMaxOn (DifferentiableOn.diffContOnCl fun x hx =>
        (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt) fun x hx =>
      (hr <| ball_subset_closedBall hx).2⟩

Goal state after:
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
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
⊢ U ⊆ V

Tactic:
have hVo : IsOpen V := by
    simpa only [ho.mem_nhds_iff, ofPred_and, ofPred_mem_eq]
      using isOpen_setOfPred_mem_nhds_and_isMaxOn_norm hd

Goal state after:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
⊢ U ⊆ V
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c

Tactic:
have h4 : ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f⁻¹ z := by filter_upwards [hf, h1] with z h using h.inv

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
h4 : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)

Goal state after:
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = 1 / cos x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

Tactic:
rw [lt_iff_not_ge] at hx_gt
    refine hx_gt ?_
    rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, neg_mul_eq_neg_mul,
      mul_le_mul_iff_left₀ (half_pos pi_pos)]
    have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
    rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]
    · norm_num
      assumption_mod_cast
    · exact zero_lt_two

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

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this✝ : x / π ≤ sin (x / 2)
this : (x / π) ^ 2 ≤ 1 / 2 - cos (2 * (x / 2)) / 2
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
ring_nf at this ⊢

Goal state after:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this✝ : x / π ≤ sin (x / 2)
this : x ^ 2 * π⁻¹ ^ 2 ≤ 1 / 2 + cos x * (-1 / 2)
⊢ cos x ≤ 1 - x ^ 2 * π⁻¹ ^ 2 * 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hx₁
⊢ -(π / 2) < π / 3

Tactic:
field_simp
    norm_num

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

Goal state before:
pp: case hx₂
⊢ π / 3 < π / 2

Tactic:
field_simp
    norm_num

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

Goal state before:
pp: case hx₁
⊢ -(π / 2) < π / 6

Tactic:
field_simp
    norm_num

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

Goal state before:
pp: case hx₂
⊢ π / 6 < π / 2

Tactic:
field_simp
    norm_num

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
⊢ Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

Tactic:
suffices sInf (slope f x '' Ioo x b) = sInf (slope f x '' {y ∈ S | x < y}) by rwa [← this]

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
⊢ sInf (slope f x '' Ioo x b) = sInf (slope f x '' {y | y ∈ S ∧ x < y})
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
⊢ t ∈ Ioi x → (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)

Tactic:
(ht' : x < t)

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ Tendsto (fun x ↦ ↑z ^ ↑x) atTop (𝓝 ↑0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_iff_norm_lt_one.mpr z.norm_lt_one
    |>.comp tendsto_PNat_val_atTop_atTop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : E
⊢ divisor (fun x ↦ e) U = 0

Tactic:
ext x
  simp only [divisor_def, meromorphicOrderAt_const, Function.locallyFinsuppWithin.coe_zero,
    Pi.zero_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero,
    LinearOrderedAddCommGroupWithTop.top_ne_zero, imp_false, ite_eq_left_iff, WithTop.zero_ne_top,
    Decidable.not_not, and_imp]
  tauto

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 : 𝕜
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
hf : MeromorphicAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
use 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 : 𝕜
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
hf : MeromorphicAt f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ ↑(analyticOrderNatAt f x) • g

Tactic:
use 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 : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
⊢ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ ↑(analyticOrderNatAt f x) • g
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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] 1 • g
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • g z

Tactic:
use 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 : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] 1 • g
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • g z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
⊢ (divisor (fun x ↦ x - z₀) U) z₀ = 1

Tactic:
by
  rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) h, ← untop₀_coe 1]
  congr
  exact (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr ⟨fun _ ↦ 1, analyticAt_const, by simp⟩

Goal state after:
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 g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
h₄ : MeromorphicAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
use 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 g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
h₄ : MeromorphicAt f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0

Tactic:
filter_upwards [h] with z hf hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf✝ : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf✝ • f z = 0
z : 𝕜
hf : (z - x) ^ Exists.choose hf✝ • f z = 0
hz : ¬z = x
⊢ f z = 0
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 : 𝕜
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ toMeromorphicNFAt f x x = 0 x

Tactic:
· simp [h₂f, toMeromorphicNFAt, hf]

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
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
simp only [toMeromorphicNFAt, hf, ↓reduceDIte]
    exact analyticAt_const.meromorphicNFAt

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 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

Tactic:
use 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 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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ ENat.map (fun x ↦ ↑x) (analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose ⋯ • f z) x) - ↑(Exists.choose ⋯) = ↑n ↔
    ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
obtain ⟨m, h⟩ := ENat.ne_top_iff_exists.mp h

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
⊢ ENat.map (fun x ↦ ↑x) (analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose ⋯ • f z) x) - ↑(Exists.choose ⋯) = ↑n ↔
    ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos.coe
𝕜 : 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
n : ℤ
h₁f₁ : meromorphicOrderAt f₁ x = ↑n
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z

Tactic:
use 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
n : ℤ
h₁f₁ : meromorphicOrderAt f₁ x = ↑n
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z = ↑(d z)

Tactic:
meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ ∃ g,
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧ ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ, (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z_1 = (z_1 - z) ^ d z • g z_1
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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ g (x, a)
⊢ Continuous[instTopologicalSpaceProd, inst✝²] g

Tactic:
continuous_iff_continuousAt

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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ g (x, a)
⊢ ∀ (x : ↑I × A), ContinuousAt g x
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
⊢ meromorphicTrailingCoeffAt f x = (∏ᶠ (u : 𝕜), (x - u) ^ update D x 0 u) • g x

Tactic:
have t₀ : MeromorphicAt (∏ᶠ u, (· - u) ^ D u) x :=
    (FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x
  rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (by fun_prop) h₁x h₂x h),
    t₀.meromorphicTrailingCoeffAt_smul h₁g.meromorphicAt,
    h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g]
  simp [meromorphicTrailingCoeffAt_factorizedRational hD]

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

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
have h₁ := f.norm_map z

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : ‖f z‖ = ‖z‖
⊢ (f z).im = z.im ∨ (f z).im = -z.im
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
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), (cov.liftHomotopy (↑F) f₀' F_0) (1, x) = f₁' x

Tactic:
← ContinuousMap.curry_apply

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
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), ((cov.liftHomotopy (↑F) f₀' F_0).curry 1) x = f₁' x
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
γ₀ γ₁ : C(↑I, X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : γ₀ 0 = p e
h₁ : γ₁ 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
⊢ (cov.liftPath γ₀ e h₀) 0 = (cov.liftPath γ₁ e h₁) 0

Tactic:
simp_rw [liftPath_zero]

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

Goal state before:
pp: case η₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ∀ x ∈ t₁,
    meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f S₀R) x *
        meromorphicTrailingCoeffAt ((fun x_1 ↦ x_1 - x) ^ (divisor f S₀R) x) w =
      1

pp: case η₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ∀ x ∈ t₂,
    meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f B₀R) x *
        meromorphicTrailingCoeffAt (canonicalFactor R x ^ (-(divisor f B₀R) x)) w =
      1

Tactic:
case η₁ =>
        intro x hx
        rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop), ← zpow_add₀,
          add_neg_cancel, zpow_zero]
        apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero (by fun_prop)
          (meromorphicOrderAt_canonicalFactor_ne_top x hR)

Goal state after:
case η₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ∀ x ∈ t₁,
    meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f S₀R) x *
        meromorphicTrailingCoeffAt ((fun x_1 ↦ x_1 - x) ^ (divisor f S₀R) x) w =
      1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∃ x,
    ∀
      y ∈
        (fun a ↦ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1,
      y ≤ x

Tactic:
use ((max 1 ((ε + sSupNormIm f 0) ^ (-(1 : ℝ)))) * max 1 ((ε + sSupNormIm f 1) ^ (-(1 : ℝ)))) * B

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∀
    y ∈
      (fun a ↦ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
        verticalClosedStrip 0 1,
    y ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪v i, w n⟫_ℝ) • w m ⊗ₜ[ℝ] w n

Tactic:
OrthonormalBasis.sum_inner_mul_inner v

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

Goal state before:
pp: case e_a
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑(((fderiv ℝ (fderiv ℝ f) x) I) 1) = ↑(((fderiv ℝ (fderiv ℝ f) x) 1) I)

Tactic:
norm_cast
    apply h₁f.isSymmSndFDerivAt (by simp)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl

Goal state before:
pp: case inl
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
exact continuousOn_singleton f x

Goal state after: