mathlib-initiative/mathlib-tactics huggingface dataset:
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
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : w ∈ closedBall z r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
mem_closedBall,

Goal state after:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist w z ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
H : ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0
⊢ EqOn f g (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
simpa [sub_eq_zero] using! H

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

Goal state before:
pp: ⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4

Tactic:
rw [two_mul_arctan, arctan_add] <;> norm_num

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

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ 1 + y ^ 2 < 1 + tan y ^ 2

Tactic:
add_lt_add_iff_left,

Goal state after:
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y ^ 2 < tan y ^ 2
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x - y‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

pp: case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0

Tactic:
one_mul

Goal state after:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)

Tactic:
rw [mem_ball_iff_norm] at hz

Goal state after:
case inr
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

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

Tactic:
have h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2 := by
    rw [h]
    exact sq_abs (‖x‖ - ‖y‖)

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
have hz' : ‖z - c‖ ≠ 0 := by simpa [sub_eq_zero] using hne
    simpa [g', hne, g, div_pow, mul_comm, field] using this

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(sphere 0 1)
x : ↑(sphere 0 r)
⊢ 1 * r = r

Tactic:
one_mul

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(sphere 0 1)
x : ↑(sphere 0 r)
⊢ r = r
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
⊢ ∃ f, ContinuousOn f U ∧ EqOn (cexp ∘ f) g U

Tactic:
by
  classical
  have := hUc.simplyConnectedSpace
  have := hUo.locallyPathConnectedSpace
  rcases hUc.nonempty with ⟨x₀, hx₀U⟩
  have hx₀ : g x₀ ≠ 0 := ne_of_mem_of_not_mem (mem_image_of_mem g hx₀U) hU₀
  lift x₀ to U using hx₀U
  rcases isCoveringMapOn_exp.existsUnique_continuousMap_lifts
    ⟨U.domRestrict g, continuousOn_iff_continuous_domRestrict.mp hgc⟩ (exp_log hx₀)
    (fun x ↦ ne_of_mem_of_not_mem (mem_image_of_mem g x.2) hU₀) with ⟨f, ⟨-, hf⟩, -⟩
  obtain ⟨g, hg⟩ : ∃ g : X → ℂ, ∀ z : U, g z = f z :=
    ⟨fun z ↦ if hz : z ∈ U then f ⟨z, hz⟩ else 0, by simp⟩
  refine ⟨g, ?hg_cont, ?hg_inv⟩
  case hg_cont =>
    rw [continuousOn_iff_continuous_domRestrict]
    convert! map_continuous f
    ext z
    exact hg z
  case hg_inv =>
    intro x hx
    lift x to U using hx
    simpa [hg] using congr($hf x)

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ (min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z)).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
apply WithTop.untop₀_le_untop₀ h₃

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z) ≤ meromorphicOrderAt (f₁ + f₂) z
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr.inl
𝕜 : 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
h₁ : f =ᶠ[𝓝 x] 0
⊢ meromorphicOrderAt f x = 0

Tactic:
have := h₁.eq_of_nhds
      tauto

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
⊢ (divisor (f₁ + f₂) U)⁻ x = (divisor f₁ U)⁻ x

Tactic:
suffices -(meromorphicOrderAt (f₁ + f₂) x).untop₀ ⊔ 0 = -(meromorphicOrderAt f₁ x).untop₀ ⊔ 0 by
      simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:

Tactic:
0
      _ ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) :=
        le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg
      _ ≤ meromorphicOrderAt (f₁ + f₂) x :=
        meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt

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
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g_f) y
⊢ (g • f) y = ((fun x_1 ↦ x_1 - x) ^ n • g • g_f) y

Tactic:
simp only [Pi.smul_apply', hy, Pi.pow_apply]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g_f) y
⊢ g y • (y - x) ^ n • g_f y = (y - x) ^ n • g y • g_f y
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
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
⊢ Tendsto (fun x ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
rcases (meromorphicOrderAt_eq_int_iff hf).1 hm.symm with ⟨g, g_an, gx, hg⟩

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
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
⊢ Tendsto (fun x ↦ ‖f x‖) (𝓝[≠] x) atTop
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt f₂ x

Tactic:
contrapose hf₁

Goal state after:
𝕜 : 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
⊢ MeromorphicAt f₁ x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖↑R ^ 2 - (starRingEnd ℂ) w * z‖ = 1 * ‖↑R * (z - w)‖

Tactic:
one_mul

Goal state after:
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖↑R ^ 2 - (starRingEnd ℂ) w * z‖ = ‖↑R * (z - w)‖
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ meromorphicOrderAt 1 x = 0

Tactic:
← WithTop.coe_zero,

Goal state after:
case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ meromorphicOrderAt 1 x = ↑0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
s : Finset ι
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (fun a ↦ ∏ i ∈ s, f i a) x = ∑ i ∈ s, meromorphicOrderAt (f i) x

Tactic:
convert! meromorphicOrderAt_prod hf
  exact (Finset.prod_apply _ s f).symm

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt 1 x = 0

Tactic:
← WithTop.coe_zero,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt 1 x = ↑0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt 1 x = 0

Tactic:
← WithTop.coe_zero,

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt 1 x = ↑0
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
⊢ ∃ g,
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : ↑U), g ↑u ≠ 0) ∧ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
by
  -- Take `g` as the inverse of the Laurent polynomial defined below, converted to a meromorphic
  -- function in normal form. Then check all the properties.
  let φ := ∏ᶠ u, (· - u) ^ (divisor f U u)
  have hφ : MeromorphicOn φ U := (meromorphicNFOn (divisor f U) U).meromorphicOn
  let g := toMeromorphicNFOn (φ⁻¹ • f) U
  have hg : MeromorphicNFOn g U := by apply meromorphicNFOn_toMeromorphicNFOn
  refine ⟨g, ?_, ?_, ?_⟩
  · -- AnalyticOnNhd 𝕜 g U
    rw [← hg.divisor_nonneg_iff_analyticOnNhd, divisor_of_toMeromorphicNFOn (hφ.inv.smul h₁f),
      divisor_smul hφ.inv h₁f _ (fun z hz ↦ h₂f ⟨z, hz⟩), divisor_inv,
      Function.FactorizedRational.divisor h₃f, neg_add_cancel]
    intro z hz
    simpa [meromorphicOrderAt_inv] using meromorphicOrderAt_ne_top (divisor f U)
  · -- ∀ (u : ↑U), g ↑u ≠ 0
    intro ⟨u, hu⟩
    rw [← (hg hu).meromorphicOrderAt_eq_zero_iff, ← meromorphicOrderAt_congr
        (toMeromorphicNFOn_eq_self_on_nhdsNE (hφ.inv.smul h₁f) hu).symm,
      meromorphicOrderAt_smul (hφ u hu).inv (h₁f u hu), meromorphicOrderAt_inv,
      meromorphicOrderAt_eq _ h₃f]
    simp only [h₁f, hu, divisor_apply]
    lift meromorphicOrderAt f u to ℤ using (h₂f ⟨u, hu⟩) with n hn
    rw [WithTop.untop₀_coe, ← WithTop.LinearOrderedAddCommGroup.coe_neg, ← WithTop.coe_add]
    simp
  · -- f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), fun z ↦ (z - u) ^ (divisor f U) u) * g
    filter_upwards [(divisor f U).eq_zero_codiscreteWithin,
      (hφ.inv.smul h₁f).meromorphicNFAt_mem_codiscreteWithin,
      self_mem_codiscreteWithin U] with a h₂a h₃a h₄a
    unfold g
    simp only [Pi.smul_apply', toMeromorphicNFOn_eq_toMeromorphicNFAt (hφ.inv.smul h₁f) h₄a,
      toMeromorphicNFAt_eq_self.2 h₃a, Pi.inv_apply]
    rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ _, one_smul]
    rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]

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₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₁ + f₂) x

Tactic:
contrapose hf₁

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt (f₁ + f₂) x
⊢ MeromorphicAt f₁ x
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₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
· rw [meromorphicOrderAt_congr]
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₂]
    simp

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ 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 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] (∑ᶠ (u : 𝕜), fun x ↦ ↑(D u) * log ‖x - u‖) + fun x ↦ log ‖g x‖

Tactic:
by
  -- Identify support of the sum in the goal
  have t₁ : (fun u ↦ (D u * log ‖· - u‖)).support = D.support := by
    ext u
    rw [← not_iff_not]
    simp only [ne_eq, not_not, Function.mem_support]
    constructor <;> intro hx
    · obtain ⟨y, hy⟩ := NormedField.exists_one_lt_norm 𝕜
      have := congrFun hx (y + u)
      simp only [add_sub_cancel_right, Pi.zero_apply, mul_eq_zero, Int.cast_eq_zero, log_eq_zero,
        norm_eq_zero] at this
      rcases this with h | h | h | h
      · assumption
      · simp only [h, norm_zero] at hy
        linarith
      · simp only [h, lt_self_iff_false] at hy
      · simp only [h, lt_neg_self_iff] at hy
        linarith
    · simp_all [Pi.zero_def]
  -- Trivial case: the support of D is infinite
  by_cases h₃f : D.support.Finite
  case neg =>
    rw [finsum_of_infinite_support (by simpa [t₁] using h₃f)]
    rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h
    filter_upwards [h] with x hx
    simp [hx]
  -- General case
  filter_upwards [h, D.eq_zero_codiscreteWithin, self_mem_codiscreteWithin U] with z hz h₂z h₃z
  rw [Pi.zero_apply] at h₂z
  rw [hz, finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _
      (by simp_all [FactorizedRational.mulSupport]),
    finsum_eq_sum_of_support_subset (s := h₃f.toFinset) _ (by simp_all)]
  have : ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0 := by
    intro x hx
    rw [Finite.mem_toFinset, Function.mem_support] at hx
    rw [ne_eq, zpow_eq_zero_iff hx, norm_eq_zero, sub_eq_zero, eq_comm]
    apply ne_of_apply_ne D
    rwa [h₂z]
  simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply, norm_smul, norm_prod, norm_zpow]
  rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod this]
  simp [log_zpow]

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

Goal state before:
pp: a : Circle
x : ℂ
⊢ ‖↑a * x‖ = ‖x‖

Tactic:
norm_mul,

Goal state after:
a : Circle
x : ℂ
⊢ ‖↑a‖ * ‖x‖ = ‖x‖
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
x : ℂ
⊢ 1 * ‖x‖ = ‖x‖

Tactic:
one_mul

Goal state after:
a : Circle
x : ℂ
⊢ ‖x‖ = ‖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
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) •
      (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (divisor f (ball 0 R)) i) • f

Tactic:
filter_upwards [codiscreteWithin_mono (by tauto) η₀.compl_mem_codiscrete,
            self_mem_codiscreteWithin (closedBall 0 R)] with a ha h₂a
          simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply]
          rw [← smul_assoc, ← Finset.prod_smul, Finset.prod_eq_one, one_smul]
          intro x hx
          rw [smul_eq_mul, ← zpow_add', neg_add_cancel, zpow_zero]
          simp_all only [ne_eq, Subtype.forall, mem_closedBall, dist_zero_right,
            locallyFinsuppWithin.support_neg, mem_compl_iff, mem_support, Decidable.not_not,
            Finite.mem_toFinset, neg_add_cancel, not_true_eq_false, neg_eq_zero, and_self, or_self,
            or_false]
          apply canonicalFactor_ne_zero _ (by simp_all) (by grind)
          by_contra h
          simp_all

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

Goal state before:
pp: case right.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
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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t' \ {↑z})

Tactic:
exact h₂t'.sdiff isClosed_singleton

Goal state after:
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:
by
  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: