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
x : 𝕜
⊢ (divisor (fun x ↦ e) U) x = 0 x

Tactic:
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]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : E
x : 𝕜
⊢ MeromorphicOn (fun x ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ divisor (fun x ↦ ∏ i ∈ s, f i x) U = ∑ i ∈ s, divisor (f i) U

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

Goal state after:
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
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x

Tactic:
by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅

Goal state after:
case pos
𝕜 : 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
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
h₄f : {σ ∈ s | f σ x = 0} = ∅
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x

case neg
𝕜 : 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
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
h₄f : ¬{σ ∈ s | f σ x = 0} = ∅
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x
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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
⊢ ⋯.choose x = g x

Tactic:
apply Filter.EventuallyEq.eq_of_nhds

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
⊢ ⋯.choose =ᶠ[𝓝 x] g
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
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hord : analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicNFAt (f ∘ g) x

Tactic:
rw [analyticOrderAt_eq_top] at hord

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hord : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = 0
⊢ MeromorphicNFAt (f ∘ g) x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicNFAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)

Tactic:
rw [show x = (x + c) - c by ring] at h

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt (f ∘ fun x ↦ x + c) (x + c - c)
⊢ MeromorphicNFAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicNFAt f (x + c)

Tactic:
rw [show f = ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) by aesop]
    rw [show x = (x + c) - c by ring] at h
    exact h.comp_analyticAt (g := fun z ↦ z - c) (by fun_prop)

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 = 0 ^ n • g x

Tactic:
apply Filter.EventuallyEq.eq_of_nhds

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.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 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
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    ((fun x_1 ↦ x_1 - x) ^ n • g) x

Tactic:
rw [eq_comm]

Goal state after:
case neg
𝕜 : 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
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
⊢ ((fun x_1 ↦ x_1 - x) ^ n • g) x =
    (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : 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 : 0 ≤ MeromorphicOn.divisor f U
x : 𝕜
hx : x ∈ U
this : 0 ≤ meromorphicOrderAt f x
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
assumption

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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
simp only [← tendsto_norm_atTop_iff_cobounded]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
⊢ Tendsto (fun x ↦ ‖f x‖) (𝓝[≠] x) atTop
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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h₁f₁ : ¬↑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
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h₁ : ↑n₁ = ↑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
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
WithTop.coe_eq_coe,

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h₁f₁ : ¬↑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
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h₁ : n₁ = 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
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
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] f

Tactic:
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with a ha
  rcases ha with ha | ha
  · simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 ha.meromorphicNFAt).symm]
  · simp only [Set.mem_compl_iff] at ha
    simp [toMeromorphicNFOn, ha, hf]

Goal state after:
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
rw [eq_comm]

Goal state after:
case pos
𝕜 : 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
⊢ meromorphicOrderAt f₂ x = meromorphicOrderAt f₁ x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
by
  convert! h₁.meromorphicTrailingCoeffAt_zpow (n := n) <;> simp

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

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

Tactic:
classical
  by_cases hd : d.support.Finite
  · simp [meromorphicOrderAt_eq d hd]
  · rw [← mulSupport] at hd
    simp [finprod_of_infinite_mulSupport hd]

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 : 𝕜 → E
x c : 𝕜
⊢ meromorphicTrailingCoeffAt (f ∘ fun x ↦ x + c) x = meromorphicTrailingCoeffAt f (x + c)

Tactic:
classical
  by_cases h : ¬ MeromorphicAt f (x + c)
  · simp_all [meromorphicAt_comp_add_const_iff_meromorphicAt.not.2 h]
  rw [MeromorphicAt.meromorphicTrailingCoeffAt_comp (by simp_all) (by fun_prop)
    (by simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top])]
  simp [meromorphicTrailingCoeffAt_id_sub_const]

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

Goal state before:
pp: case mp
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ canonicalFactor R w z = 0 → z = w

Tactic:
contrapose
    exact canonicalFactor_ne_zero hw (ball_subset_closedBall hz)

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

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

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

Tactic:
· intro z hz
    apply zpow (fun x hx ↦ meromorphic_canonicalFactor R z x)

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

Goal state before:
pp: case mp.inl
𝕜 : 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‖
h : D u = 0
⊢ D u = 0

Tactic:
assumption

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

Goal state before:
pp: this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10000000000

Tactic:
assumption

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

Goal state before:
pp: this : |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000

Tactic:
assumption

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

Goal state before:
pp: this : |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case 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
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩ = id ⟨e₀, he⟩

Tactic:
rw [Path.map_symm, ← Path.map_trans]

Goal state after:
case 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
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.trans pγ'.symm).map ⋯)) ⟨e₀, he⟩ = id ⟨e₀, he⟩
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0

Tactic:
← ofReal_add,

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑(ε + sSupNormIm f 0) ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 1) ≠ 0

Tactic:
← ofReal_add,

Goal state after:
case hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑(ε + sSupNormIm f 1) ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

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

Tactic:
simp only [hz1, one_mul, Real.rpow_zero, sub_self, Real.rpow_neg_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 1), mul_one]

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f 1
Module: Mathlib.Analysis.Complex.HalfPlane

Goal state before:
pp: x : ℝ
⊢ IsOpen {z | x < z.re}

Tactic:
simpa using isOpen_re_gt_EReal x

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

Goal state before:
pp: case pos.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ ¬z = 0

Tactic:
rw [eq_comm]

Goal state after:
case pos.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ ¬0 = z
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ ↑z.re + ↑y * I ∈ closedBall c r

Tactic:
by
  refine le_trans ?_ (mem_closedBall.mp z_in_ball)
  rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
    Real.sq_sqrt (by positivity)]
  suffices (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2 by simpa
  cases mem_uIoc.mp y_in_I <;> nlinarith

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

Goal state before:
pp: E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : E → F
ι : Type u_5
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
⊢ Δ f = fun x ↦ ∑ i, (iteratedFDeriv ℝ 2 f x) ![v i, v i]

Tactic:
ext x
  simp [laplacian, canonicalCovariantTensor_eq_sum E v, tensorIteratedFDerivTwo_eq_iteratedFDeriv]

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

Goal state before:
pp: 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
c : ℝ
h : HarmonicAt f x
⊢ HarmonicAt (c • f) x

Tactic:
constructor
  · exact h.1.const_smul c
  · filter_upwards [laplacian_smul_nhds c h.1, h.2]
    simp_all

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

Goal state before:
pp: 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
⊢ (fun w ↦ (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - (w - z).re • f z) =o[𝓝 z] fun w ↦ w - z

Tactic:
by
  suffices (fun x ↦ (∫ t in z.re..x, f (t + z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re]
      fun x ↦ x - z.re from
    this.comp_tendsto (continuous_re.tendsto z) |>.trans_isBigO isBigO_re_sub_re
  let r₁ := r - dist z c
  have r₁_pos : 0 < r₁ := by simpa only [mem_ball, sub_pos, r₁] using hz
  let s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
  have zRe_mem_s : z.re ∈ s := by simp [s, r₁_pos]
  have f_contOn : ContinuousOn (fun (x : ℝ) ↦ f (x + z.im * I)) s :=
    f_cont.comp ((continuous_add_const _).comp continuous_ofReal).continuousOn <|
      fun _ ↦ mem_ball_re_aux
  have int1 : IntervalIntegrable (fun (x : ℝ) ↦ f (x + z.im * I)) volume z.re z.re :=
    ContinuousOn.intervalIntegrable <| f_contOn.mono <| by simpa
  have int2 : StronglyMeasurableAtFilter (fun (x : ℝ) ↦ f (x + z.im * I)) (𝓝 z.re) :=
    f_contOn.stronglyMeasurableAtFilter isOpen_Ioo _ zRe_mem_s
  have int3 : ContinuousAt (fun (x : ℝ) ↦ f (x + z.im * I)) z.re :=
    isOpen_Ioo.continuousOn_iff.mp f_contOn zRe_mem_s
  simpa using intervalIntegral.integral_hasDerivAt_right int1 int2 int3 |>.isLittleO

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hab : a ≠ b
hf : ContinuousOn f [[a, b]]
⊢ volume (Ι a b) ≠ 0

Tactic:
simpa using sub_ne_zero.mpr hab.symm

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

Goal state before:
pp: c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (2 * ↑π * I)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z

Tactic:
by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]

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

Goal state before:
pp: a b : ℂ
⊢ ((a.re + b.re) * (a - b).re + (a + b).im * (a - b).im) / ‖a - b‖ ^ 2 = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2

Tactic:
sub_re,

Goal state after:
a b : ℂ
⊢ ((a.re + b.re) * (a.re - b.re) + (a + b).im * (a - b).im) / ‖a - b‖ ^ 2 = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
⊢ ⇑reCLM ∘ log ∘ (⇑conjCLE ∘ g * g) =ᶠ[𝓝 z] ⇑reCLM ∘ (log ∘ ⇑conjCLE ∘ g + log ∘ g)

Tactic:
by
      filter_upwards [t₀] with x hx
      simp only [Function.comp_apply, Pi.mul_apply, conjCLE_apply, Pi.add_apply]
      congr
      rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]
      · simp [Complex.slitPlane_arg_ne_pi hx.1, Real.pi_pos, Real.pi_nonneg]
      · simpa [ne_eq, map_eq_zero] using hx.2

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ negMulLog = fun x ↦ -(x * log x)

Tactic:
simp [negMulLog_def]

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
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
⊢ ContinuousOn (fun x ↦ f ↑x) (Ici 0)

Tactic:
refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x : ℝ
hx : x ∈ Ici 0
⊢ ↑x ∈ closure {z | 0 < z.re}