mathlib-initiative/mathlib-tactics huggingface dataset:
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:
classical
  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.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
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
ta : ↑I × A
x✝ : ta ∈ Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun y ↦ (t n, y)) ⁻¹' (q e).source)) ∩ frontier {a | a.1 ≤ t n}
left✝¹ : ta.1 ∈ Set.Icc 0 (t n.succ)
hav : ta.2 ∈ v
left✝ : ta.2 ∈ N
ha : ta.2 ∈ (g' ∘ fun y ↦ (t n, y)) ⁻¹' (q e).source
hfr : ta ∈ frontier {a | a.1 ≤ t n}
ht : ta.1 = t n
⊢ ta.1 ∈ Set.Icc (t n) (t (n + 1))

Tactic:
rw [ht]; exact ⟨le_rfl, t_mono n.le_succ⟩

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

Tactic:
rwa [smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)] at hf

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

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
n : ℤ
hn : ↑n = meromorphicOrderAt f x
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
h₃f : n = 0
h₁G : AnalyticAt 𝕜 (Classical.choose ⋯) x
left✝ : Classical.choose ⋯ x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • Classical.choose ⋯ z
⊢ Classical.choose ⋯ =ᶠ[𝓝 x] fun {x} ↦ 0 ^ n • g x

Tactic:
apply (h₁G.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop)).1

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
h₃f : n = 0
h₁G : AnalyticAt 𝕜 (Classical.choose ⋯) x
left✝ : Classical.choose ⋯ x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • Classical.choose ⋯ z
⊢ Classical.choose ⋯ =ᶠ[𝓝[≠] x] fun {x} ↦ 0 ^ n • g x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : MeromorphicOn f U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
⊢ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
by
  simp_rw [eventually_iff, mem_codiscreteWithin, disjoint_principal_right]
  intro x hx
  filter_upwards [(meromorphicOrderAt_ne_top_iff_eventually_ne_zero (hf x hx)).1 (h'f x hx)]
    with y hy
  simp [hy]

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

Goal state before:
pp: case neg
𝕜 : 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) = ⊤
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
F : 𝕜 → E
h₁F : AnalyticAt 𝕜 F (g x)
h₂F : F (g x) ≠ 0
h₃F : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • F z
h₁ : meromorphicTrailingCoeffAt (f ∘ g) x = meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x
⊢ meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r) x • (F ∘ g) x =
    meromorphicTrailingCoeffAt (fun x_1 ↦ g x_1 - g x) x ^ r • F (g x)

Tactic:
simp_all only [ne_eq, Function.comp_apply, not_false_eq_true, smul_left_inj]

Goal state after:
case neg
𝕜 : 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) = ⊤
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
F : 𝕜 → E
h₁F : AnalyticAt 𝕜 F (g x)
h₂F : ¬F (g x) = 0
h₃F : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • F z
h₁ : meromorphicTrailingCoeffAt (f ∘ g) x = meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x
⊢ meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r) x = meromorphicTrailingCoeffAt (fun x_1 ↦ g x_1 - g x) x ^ r
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
h_num_ne_zero : ↑R ^ 2 - (starRingEnd ℂ) w * z ≠ 0
⊢ canonicalFactor R w z ≠ 0

Tactic:
rw [canonicalFactor_apply]

Goal state after:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
h_num_ne_zero : ↑R ^ 2 - (starRingEnd ℂ) w * z ≠ 0
⊢ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w)) ≠ 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

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

Tactic:
by
  classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all

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

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

Tactic:
by
  rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
        (((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).smul h₁g.meromorphicAt)
          h₁x h₂x h),
    ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).meromorphicTrailingCoeffAt_smul
      h₁g.meromorphicAt, h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g,
    norm_smul, log_mul, log_norm_meromorphicTrailingCoeffAt hD]
  · simp only [ne_eq, norm_eq_zero]
    apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero
      ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x)
    apply FactorizedRational.meromorphicOrderAt_ne_top
  · simp_all

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

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

Tactic:
mul_self_eq_mul_self_iff

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : (f z).im = z.im ∨ (f z).im = -z.im
⊢ (f z).im = z.im ∨ (f z).im = -z.im
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖(‖map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖

case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ restrictScalars ℝ map = ‖map 1‖ • { toLinearMap := ‖map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := ?refine_1 }.toContinuousLinearMap
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
U : Set 𝕜
hf : MeromorphicOn f U
a : 𝕜
hx : a ∈ U
h₁f h₁a : ∀ᶠ (x : 𝕜) in 𝓝[≠] a, f x = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

Tactic:
exact h₁a

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

Goal state before:
pp: ⊢ 0.3678794412⁻¹ < rexp 1

Tactic:
exact lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z ↦ expR (B * expR (c * |u z|))
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
⊢ ‖expR (B₁✝ * expR (c₁✝ * |u z|))‖ ≤ ‖expR (B₂✝ * expR (c₂✝ * |u z|))‖

Tactic:
simp only [Real.norm_eq_abs, Real.abs_exp]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z ↦ expR (B * expR (c * |u z|))
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
⊢ expR (B₁✝ * expR (c₁✝ * |u z|)) ≤ expR (B₂✝ * expR (c₂✝ * |u z|))
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
hz : 1 ≤ ‖z‖
⊢ ‖expR (B₁✝ * ‖z‖ ^ c₁✝)‖ ≤ expR (B₂✝ * ‖z‖ ^ c₂✝)

Tactic:
simp only [Real.norm_eq_abs, Real.abs_exp]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z ↦ expR (B * ‖z‖ ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
hz : 1 ≤ ‖z‖
⊢ expR (B₁✝ * ‖z‖ ^ c₁✝) ≤ expR (B₂✝ * ‖z‖ ^ c₂✝)
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)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a

Tactic:
by
    rw [liftHomotopy_apply, cov.const_of_comp (ContinuousMap.continuous _) _ t 0]
    · apply cov.liftPath_zero
    · intro t t'; simp_rw [← p.comp_apply, cov.liftPath_lifts]
      exact (F.prop t a ha).trans (F.prop t' a ha).symm

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

Goal state before:
pp: 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
⊢ ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      ((∏ n ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R n ^ (-(divisor f B₀R) n)) w) *
          ∏ n ∈ t₁, meromorphicTrailingCoeffAt ((fun x ↦ x - n) ^ (divisor f S₀R) n) w) •
        h w =
    h w

Tactic:
rw [smul_smul, mul_mul_mul_comm, ← Finset.prod_mul_distrib, ← Finset.prod_mul_distrib,
        Finset.prod_eq_one ?η₁, Finset.prod_eq_one ?η₂, mul_one, one_smul]
      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)
      case η₂ =>
        intro x hx
        rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop), ← zpow_add₀,
          locallyFinsuppWithin.coe_neg, Pi.neg_apply, neg_add_cancel, zpow_zero]
        rw [meromorphicTrailingCoeffAt_id_sub_const]
        grind

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
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
by
  by_cases hf : MeromorphicAt f x
  · simp [meromorphicOrderAt_smul hg.meromorphicAt hf, hg.meromorphicOrderAt_eq,
      hg.analyticOrderAt_eq_zero.mpr hg']
  · rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
    rwa [meromorphicAt_smul_iff_of_ne_zero hg hg']

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

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im = b
⊢ ‖f z‖ ≤ C

Tactic:
exact hle_b _ hzb

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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
hab : a - b < a + b
⊢ ‖f z‖ ≤ C

Tactic:
have hb : 0 < b := by simpa only [sub_eq_add_neg, add_lt_add_iff_left, neg_lt_self_iff] using hab

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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 0 = sSupNormIm f l

Tactic:
by
  simp_rw [sSupNormIm, image_comp]
  have : scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l} := by
    ext e
    simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
    constructor
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ↑l + z * (↑u - ↑l)
      simp [hz₁, hz₂]
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ((z - l) / (u - l))
      constructor
      · norm_cast
        rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
        simp [hz₁]
      · rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp [hz₂]
  rw [this]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re

Tactic:
← mul_inv_le_iff₀',

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re))⁻¹ ≤ (ε + sSupNormIm f 1) ^ z.re

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ sSupNormIm f 0 ^ (1 - z).re * ‖↑(sSupNormIm f 1) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h1).mp (sSupNormIm_nonneg f _)) _]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)

Tactic:
gcongr
    · exact sSupNormIm_nonneg f _
    · exact sub_nonneg.mpr hz.2
    rw [sSupNormIm]
    apply csSup_le _
    · simpa [comp_apply, mem_image, forall_exists_index,
        and_imp, forall_apply_eq_imp_iff₂] using ha
    · use ‖(f 0)‖, 0
      simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
⊢ (lift (bilinearIteratedFDerivWithinTwo 𝕜 f s e)) (e₁ ⊗ₜ[𝕜] e₂) = ((bilinearIteratedFDerivWithinTwo 𝕜 f s e) e₁) e₂

Tactic:
lift.tmul

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
⊢ ((bilinearIteratedFDerivWithinTwo 𝕜 f s e) e₁) e₂ = ((bilinearIteratedFDerivWithinTwo 𝕜 f s e) e₁) e₂
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
⊢ (lift (bilinearIteratedFDerivTwo 𝕜 f e)) (e₁ ⊗ₜ[𝕜] e₂) = ((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂

Tactic:
lift.tmul

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
⊢ ((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂ = ((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η x : ℝ
⊢ (fun θ ↦ f (circleMap c R θ)) (x + 2 * π) = (fun θ ↦ f (circleMap c R θ)) x

Tactic:
by simp [periodic_circleMap c R x]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..0 + 2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..η + 2 * π, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)

Tactic:
zero_add,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..η + 2 * π, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
x : ℝ
⊢ (fun w ↦ f (circleMap 0 1 w)) (x + 2 * π) = (fun w ↦ f (circleMap 0 1 w)) x

Tactic:
simp [periodic_circleMap 0 1 x]

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

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
⊢ ∃ F, AnalyticOnNhd ℂ F univ ∧ (fun z ↦ (F z).re) = f

Tactic:
by
  let g := ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I)
  have hg : Differentiable ℂ g :=
    fun x ↦ (HarmonicAt.differentiableAt_complex_partial (hf x (mem_univ x)))
  obtain ⟨F, hF⟩ := hg.isExactOn_univ.with_val_at 0 (f 0)
  have h₁F : ∀ z₁, HasDerivAt F (g z₁) z₁ := by simp_all
  have h₂F : Differentiable ℂ F := fun x ↦ (h₁F x).differentiableAt
  have h₃F : Differentiable ℝ F := h₂F.restrictScalars (𝕜 := ℝ)
  use F, (h₂F.differentiableOn).analyticOnNhd isOpen_univ
  ext x
  rw [← Complex.reCLM_apply, ← Function.comp_apply (f := reCLM)]
  refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
  case hd => exact hf.contDiffOn.differentiableOn two_ne_zero
  case heq =>
    intro y hy
    simp only [fderivWithin_univ]
    rw [fderiv_comp y (by fun_prop) (by fun_prop)]
    ext x
    trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))
    · simp only [map_smul, map_add]
      simp [(h₁F y).hasFDerivAt.restrictScalars ℝ |>.fderiv, g]
    · simp
  all_goals simp_all

Goal state after: