mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
⊢ (divisor (f ∘ fun x ↦ x + c) U) (x - c) = (divisor f (U + {c})) x

Tactic:
have := meromorphicOn_comp_add_const_iff_meromorphicOn.2 h

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
⊢ (divisor (f ∘ fun x ↦ x + c) U) (x - c) = (divisor f (U + {c})) x
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
U : Set 𝕜
hf : MeromorphicOn f U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U

Tactic:
intro z hz

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (toMeromorphicNFOn f U) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
⊢ ∀ a ∈ Finite.toFinset h₁, ((fun x ↦ x - a) ^ d a) x ≠ 0

Tactic:
intro z hz

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
⊢ ((fun x ↦ x - z) ^ d z) x ≠ 0
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
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x

Tactic:
rcases lt_or_ge 0 (meromorphicOrderAt f x) with ho | ho
  · simp [ho, tendsto_zero_of_meromorphicOrderAt_pos ho]
  simp only [← not_le, ho, not_true_eq_false, iff_false]
  intro hc
  rcases ho.eq_or_lt with ho | ho
  · obtain ⟨c, c_ne, h'c⟩ := tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho
    apply c_ne
    exact tendsto_nhds_unique h'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:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
⊢ MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) univ

Tactic:
intro z hz

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : z ∈ univ
⊢ MeromorphicNFAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ MeromorphicNFOn (canonicalFactor R w) univ

Tactic:
intro z hz

Goal state after:
R : ℝ
w : ℂ
h : w ∈ ball 0 R
z : ℂ
hz : z ∈ univ
⊢ MeromorphicNFAt (canonicalFactor R w) z
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 : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ ContinuousAt f x

Tactic:
continuousAt_iff_punctured_nhds,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ Tendsto f (𝓝[≠] x) (𝓝 (f x))
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁶ : NormedRing R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : Module R E
inst✝³ : IsBoundedSMul R E
inst✝² : Module.IsTorsionFree R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0

Tactic:
filter_upwards [h₂f] with z hz using by simp [hz]

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 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ z ∈ U, meromorphicOrderAt φ⁻¹ z ≠ ⊤

Tactic:
intro z hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt φ⁻¹ z ≠ ⊤
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 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : (divisor f U) a = 0 a
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
⊢ ↑((divisor f U) a) = 0

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

Tactic:
h₂a,

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

case h₁d
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : (divisor f U) a = 0 a
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
⊢ HasFiniteSupport ⇑(divisor f U)
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)

Tactic:
intro z hz

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
z : ℂ
hz : z ∈ η₀.toFinset
⊢ MeromorphicOn (canonicalFactor R z ^ (divisor f (ball 0 R)) z) (ball 0 R)
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)
t✝ : ↑I
a✝ : A
N : Set A
haN : N ∈ 𝓝 a✝
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.univ ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x✝¹ : ↑I × A
t : ↑I
a : A
x✝ : (t, a) ∈ Set.univ ×ˢ N
left✝ : (t, a).1 ∈ Set.univ
ha : (t, a).2 ∈ N
⊢ (p ∘ fun x ↦ g (x, a)) = p ∘ g' ∘ fun x ↦ (x, a)

Tactic:
ext t

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)
t✝¹ : ↑I
a✝ : A
N : Set A
haN : N ∈ 𝓝 a✝
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.univ ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x✝¹ : ↑I × A
t✝ : ↑I
a : A
x✝ : (t✝, a) ∈ Set.univ ×ˢ N
left✝ : (t✝, a).1 ∈ Set.univ
ha : (t✝, a).2 ∈ N
t : ↑I
⊢ (p ∘ fun x ↦ g (x, a)) t = (p ∘ g' ∘ fun x ↦ (x, a)) t
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 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : ¬D.support.Finite
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] 0 + fun x ↦ log ‖g x‖

Tactic:
finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)

Goal state after:
𝕜 : 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] 1 • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : ¬D.support.Finite
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] 0 + fun x ↦ log ‖g x‖
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ u ∈ ball 0 R, g u ≠ 0

Tactic:
intro z hz

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ ball 0 R
⊢ g z ≠ 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ ∀ x ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ,
    ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t

Tactic:
intro z hz

Goal state after:
case left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
have : x ∉ sphere (0 : ℂ) R := by aesop

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
this : x ∉ sphere 0 R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x
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
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ∃ t, (∀ y ∈ t, y ∈ {↑w}ᶜ → ¬f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑w ∈ t

Tactic:
use t' \ {z.1}, fun y h₁y h₂y ↦ h₁t' y h₁y.1 h₁y.2, h₂t'.sdiff isClosed_singleton, hw,
            mem_singleton_iff.not.2 (Subtype.coe_ne_coe.mpr h₁w)

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

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

Tactic:
intro z hz

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
this : meromorphicOrderAt (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
rw [divisor_apply (D.meromorphicOn.mono_set sphere_subset_closedBall) (by aesop),
      divisor_apply D.meromorphicNFOn.meromorphicOn (by aesop), meromorphicOrderAt_congr η₀,
      meromorphicOrderAt_smul η₁.meromorphicAt (D.meromorphicNFOn (by aesop)).meromorphicAt]

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
this : meromorphicOrderAt (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0
⊢ (meromorphicOrderAt g x).untop₀ =
    (meromorphicOrderAt (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x +
        meromorphicOrderAt g x).untop₀
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
have : x ∉ sphere (0 : ℂ) R := by aesop

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
this : x ∉ sphere 0 R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
v : 𝕜
hv : v ∈ U
⊢ ∃ u, meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
use ⟨v, hv⟩, h₂f ⟨v, hv⟩

Goal state after:
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)
e : E
γ_0 : γ 0 = p e
⊢ ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

Tactic:
by
  let U x := (cov x).2.choose
  choose mem_base U_open _ H _ using fun x ↦ (cov x).2.choose_spec
  obtain ⟨t, t_0, t_mono, ⟨n_max, h_max⟩, t_sub⟩ :=
    exists_monotone_Icc_subset_open_cover_unitInterval
    (fun x ↦ (U_open x).preimage γ.continuous) fun t _ ↦ Set.mem_iUnion.2 ⟨γ t, mem_base _⟩
  suffices ∀ n, ∃ Γ : I → E, ContinuousOn Γ (Set.Icc 0 (t n)) ∧
      (Set.Icc 0 (t n)).EqOn (p ∘ Γ) γ ∧ Γ 0 = e by
    obtain ⟨Γ, cont, eqOn, Γ_0⟩ := this n_max
    rw [h_max _ le_rfl] at cont eqOn
    exact ⟨⟨Γ, continuousOn_univ.mp
      (by convert! cont; rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩)⟩,
      funext fun _ ↦ eqOn ⟨bot_le, le_top⟩, Γ_0⟩
  intro n
  induction n with
  | zero =>
    refine ⟨fun _ ↦ e, continuous_const.continuousOn, fun t ht ↦ ?_, rfl⟩
    rw [t_0, Set.Icc_self, Set.mem_singleton_iff] at ht; subst ht; exact γ_0.symm
  | succ n ih => ?_
  obtain ⟨Γ, cont, eqOn, Γ_0⟩ := ih
  obtain ⟨x, t_sub⟩ := t_sub n
  have pΓtn : p (Γ (t n)) = γ (t n) := eqOn ⟨t_0 ▸ t_mono n.zero_le, le_rfl⟩
  have : Nonempty (p ⁻¹' {x}) :=
    ⟨(H x ⟨Γ (t n), Set.mem_preimage.mpr (pΓtn ▸ t_sub ⟨le_rfl, t_mono n.le_succ⟩)⟩).2⟩
  let q := (cov x).toTrivialization
  refine ⟨fun s ↦ if s ≤ t n then Γ s else q.invFun (γ s, (q (Γ (t n))).2),
    .if (fun s hs ↦ ?_) (cont.mono fun _ h ↦ ?_) ?_, fun s hs ↦ ?_, ?_⟩
  · cases frontier_Iic_subset _ hs.2
    rw [← pΓtn]
    refine (q.symm_apply_mk_proj ?_).symm
    rw [q.mem_source, pΓtn]
    exact t_sub ⟨le_rfl, t_mono n.le_succ⟩
  · rw [closure_le_eq continuous_id' continuous_const] at h; exact ⟨h.1.1, h.2⟩
  · apply q.continuousOn_invFun.comp ((Continuous.prodMk_left _).comp γ.2).continuousOn
    simp_rw [not_le, q.target_eq]; intro s h
    exact ⟨t_sub ⟨closure_lt_subset_le continuous_const continuous_subtype_val h.2, h.1.2⟩, ⟨⟩⟩
  · rw [Function.comp_apply]; split_ifs with h
    exacts [eqOn ⟨hs.1, h⟩, q.proj_symm_apply' (t_sub ⟨le_of_not_ge h, hs.2⟩)]
  · dsimp only; rwa [if_pos (t_0 ▸ t_mono n.zero_le)]

Goal state after:
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 : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
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.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hf : meromorphicOrderAt f x = ↑n
hmero : MeromorphicAt f x
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)

Tactic:
meromorphicOrderAt_eq_int_iff hmero

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hf : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
hmero : MeromorphicAt f x
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ sSupNormIm f z.re

Tactic:
refine le_csSup ?_ ?_
  · revert hB; gcongr
    exact preimage_mono (singleton_subset_iff.mpr hD)
  · apply mem_image_of_mem (norm ∘ f)
    simp only [mem_preimage, mem_singleton]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ (z : ℂ), z.re = 0 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ a

Tactic:
intro z hz

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ‖f (↑l + z * (↑u - ↑l))‖ ≤ a
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ (z : ℂ), z.re = 1 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ b

Tactic:
intro z hz

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ‖f (↑l + z * (↑u - ↑l))‖ ≤ b
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0

pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
· norm_cast
        rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
        simp [hz₁]

Goal state after:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ (if sSupNormIm (scale f l u) 0 = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else
      ↑(sSupNormIm (scale f l u) 0) ^ (1 - (z - ↑l) / (↑u - ↑l)) *
        ↑(sSupNormIm (scale f l u) 1) ^ ((z - ↑l) / (↑u - ↑l))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else ↑(sSupNormIm f l) ^ (1 - (z - ↑l) / (↑u - ↑l)) * ↑(sSupNormIm f u) ^ ((z - ↑l) / (↑u - ↑l))

Tactic:
sSupNormIm_scale_left f hul,

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ (if sSupNormIm f l = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else ↑(sSupNormIm f l) ^ (1 - (z - ↑l) / (↑u - ↑l)) * ↑(sSupNormIm (scale f l u) 1) ^ ((z - ↑l) / (↑u - ↑l))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else ↑(sSupNormIm f l) ^ (1 - (z - ↑l) / (↑u - ↑l)) * ↑(sSupNormIm f u) ^ ((z - ↑l) / (↑u - ↑l))
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case succ
V : Type u_5
E : Type u_6
inst✝³ : LineDeriv V E E
inst✝² : AddCommGroup V
inst✝¹ : AddCommGroup E
inst✝ : LineDerivAdd V E E
x y : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
m : Fin (n + 1) → V
⊢ ∂_{m 0} (∂^{tail m} x + ∂^{tail m} y) = ∂_{m 0} (∂^{tail m} x) + ∂_{m 0} (∂^{tail m} y)

Tactic:
lineDerivOp_add

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

Goal state before:
pp: case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ (z.re - l) / (u - l) ≤ 1

Tactic:
div_le_one (by simp [hul]),

Goal state after:
case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re - l ≤ u - l