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

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

Tactic:
by_cases h₁ : (fun u ↦ (· - u) ^ d u).HasFiniteMulSupport

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
⊢ (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x ≠ 0

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : ¬HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
⊢ (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x ≠ 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ 0 • 1

Tactic:
simp only [zpow_zero, smul_eq_mul, mul_one]
      exact eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl

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

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

Tactic:
right

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : z ∈ univ
⊢ ∃ n g,
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧ (fun x ↦ x - z) ^ d z * ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d z 0 u =ᶠ[nhds z] (fun x ↦ x - z) ^ n • g
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
R : ℝ
z : ℂ
hz : z ∈ univ
h : z ∈ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R z) z ∨
    MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0

Tactic:
right

Goal state after:
case inl
R : ℝ
z : ℂ
hz : z ∈ univ
h : z ∈ ball 0 R
⊢ MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
have : meromorphicOrderAt (canonicalFactor R w) z = 0 := by
        rw [(meromorphicNFOn_canonicalFactor hw (Set.mem_univ z)).meromorphicOrderAt_eq_zero_iff]
        exact canonicalFactor_ne_zero hw (ball_subset_closedBall hz) h₂z
      simp [this, h₂z, Function.locallyFinsuppWithin.restrict_apply, hz]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
rw [h₂f, ← LinearOrderedAddCommGroupWithTop.neg_top, neg_neg]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ 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₁ 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:
lift meromorphicOrderAt f₂ x to ℤ using h₁f₂ with n₂ hn₂

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
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add_eq_left_of_lt :
  MeromorphicAt f₂ x → meromorphicOrderAt f₁ x < ↑n₂ → meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
h : meromorphicOrderAt f₁ x < ↑n₂
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
hg : g ∈ Subgroup.center (GL n R)
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar n)

Tactic:
refine Matrix.mem_range_scalar_of_commute_transvectionStruct fun t ↦ ?_

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
hg : g ∈ Subgroup.center (GL n R)
t : TransvectionStruct n R
⊢ Commute t.toMatrix ↑g
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case mpr.inl
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
refine isConformalMap_complex_linear ?_
      contrapose h₂ with w
      simp only [w, restrictScalars_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 : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝ : Set ↑U
| x✝ ⊆ {u | meromorphicOrderAt f ↑u = ⊤}

Tactic:
right

Goal state after:
𝕜 : 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 = ⊤}
x✝ : Set ↑U
| {u | meromorphicOrderAt f ↑u = ⊤}
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), ((cov.liftHomotopy (↑F) f₀' F_0).curry 1) x = f₁' x

Tactic:
refine congr_fun (cov.eq_of_comp_eq
        (ContinuousMap.continuous _) f₁'.continuous ?_ a <| (rel 1 a ha).trans he)

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ p ∘ ⇑((cov.liftHomotopy (↑F) f₀' F_0).curry 1) = p ∘ ⇑f₁'
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
⊢ sSupNormIm f 0 = 0 ∧ ¬1 - z = 0 ∨ ¬z = 0

Tactic:
right

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
⊢ ¬z = 0
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
⊢ z.wedgeIntegral w f + w.wedgeIntegral z f =
    (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)

Tactic:
simp only [wedgeIntegral, intervalIntegral.integral_symm z.re w.re,
    intervalIntegral.integral_symm z.im w.im, smul_neg]
  abel

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

Goal state before:
pp: case hf.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ sSupNormIm f 0 ≠ 0 ∨ 0 ≤ 1 - z.re

Tactic:
right

Goal state after:
case hf.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ 0 ≤ 1 - z.re
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case hg.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ sSupNormIm f 1 ≠ 0 ∨ 0 ≤ z.re

Tactic:
right

Goal state after:
case hg.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ 0 ≤ z.re
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ),
    ↑a + ↑b₁ * I ∈ ball c r → ↑a + ↑b₂ * I ∈ ball c r → IntervalIntegrable (fun y ↦ f (↑a + ↑y * I)) volume b₁ b₂
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
have hI₁ : I₁ = I₃ + I₇ := by
    rw [intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableHoriz
    · exact re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)
    · exact re_add_im_mul_mem_ball hz
    · exact re_add_im_mul_mem_ball hz
    · exact re_add_im_mul_mem_ball w_mem

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ),
    ↑a + ↑b₁ * I ∈ ball c r → ↑a + ↑b₂ * I ∈ ball c r → IntervalIntegrable (fun y ↦ f (↑a + ↑y * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h₁
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
⊢ ∀ b ∈ norm ∘ f '' re ⁻¹' {0}, b ≤ a

Tactic:
simpa [comp_apply, mem_image, forall_exists_index,
        and_imp, forall_apply_eq_imp_iff₂] using ha

Goal state after:
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
⊢ (norm ∘ f '' re ⁻¹' {0}).Nonempty

Tactic:
use ‖(f 0)‖, 0

Goal state after:
case h
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
⊢ 0 ∈ re ⁻¹' {0} ∧ (norm ∘ f) 0 = ‖f 0‖
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
η₁ : IsBounded (range (⇑ℓ ∘ f))
⊢ ‖f z - f w‖ = 0

Tactic:
← h₂ℓ

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
η₁ : IsBounded (range (⇑ℓ ∘ f))
⊢ ℓ (f z) - ℓ (f w) = 0
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst✝ : CompleteSpace E
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ) = f c

Tactic:
simp only [circleMap_zero_radius, Function.const_apply,
    intervalIntegral.integral_const, sub_zero,
    ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ (mul_ne_zero two_ne_zero pi_ne_zero),
    one_smul]

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

Goal state before:
pp: x : ℝ
⊢ deriv (deriv fun x ↦ x * log x) x = x⁻¹

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x ↦ x * log x) x = x⁻¹

case neg
x : ℝ
hx : ¬x = 0
⊢ deriv (deriv fun x ↦ x * log x) x = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x y : ℝ
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x y : ℝ
hx : x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

case neg
x y : ℝ
hx : ¬x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
h : 0 ≤ z.im
⊢ ‖f z‖ ≤ max C C'

Tactic:
refine quadrant_I (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h
      exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

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

Goal state before:
pp: case pos
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun x ↦ Real.log ‖f x‖) = 2⁻¹ • Real.log ∘ ⇑normSq ∘ f
h₃f : f z ∈ slitPlane
⊢ HarmonicAt (Real.log ∘ ⇑normSq ∘ f) z

pp: case neg
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun x ↦ Real.log ‖f x‖) = 2⁻¹ • Real.log ∘ ⇑normSq ∘ f
h₃f : f z ∉ slitPlane
⊢ HarmonicAt (Real.log ∘ ⇑normSq ∘ f) z

Tactic:
· exact analyticAt_harmonicAt_log_normSq h₁f h₂f h₃f

Goal state after:
case neg
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun x ↦ Real.log ‖f x‖) = 2⁻¹ • Real.log ∘ ⇑normSq ∘ f
h₃f : f z ∉ slitPlane
⊢ HarmonicAt (Real.log ∘ ⇑normSq ∘ f) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x : ℝ
⊢ sinc (-x) = sinc x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ sinc (-x) = sinc x

case neg
x : ℝ
hx : ¬x = 0
⊢ sinc (-x) = sinc x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x : ℝ
⊢ |sinc x| ≤ 1

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ |sinc x| ≤ 1

case neg
x : ℝ
hx : ¬x = 0
⊢ |sinc x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ |sin x / x| ≤ 1

Tactic:
abs_div

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ |sin x| / |x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1

Tactic:
right

Goal state after:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Icc 0 c
⊢ 0 ≤ r + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x : ℝ
⊢ ContinuousAt (dslope sin 0) x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ ContinuousAt (dslope sin 0) x

case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt (dslope sin 0) x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg.inr.refine_2.inr.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ‖‖Complex.exp (↑π * Complex.I * r)‖‖ₑ = 0 ∨ μ (Ioo c 0) < ⊤

Tactic:
right

Goal state after:
case neg.inr.refine_2.inr.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ μ (Ioo c 0) < ⊤
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
⊢ IntervalIntegrable (fun θ ↦ herglotzRieszKernel 0 w (circleMap 0 R θ) • f (circleMap 0 R θ)) volume 0 (2 * π)

Tactic:
have h₁ : CircleIntegrable (herglotzRieszKernel 0 w • f) 0 R :=
      hg.continuousOn_smul (continuousOn_herglotzRieszKernel_sphere hw)
    simpa only [CircleIntegrable, Pi.smul_apply'] using h₁

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

Goal state before:
pp: case neg
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : 0 < log x
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
right

Goal state after:
case neg
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : 0 < log x
⊢ 0 ≤ log y ∧ log x ≤ log y
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
⊢ ContinuousAt log⁺ x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ ContinuousAt log⁺ x

case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
right

Goal state after:
case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: | (∫ (x : ℝ) in 0..π / 2, log (sin x)) + ∫ (x : ℝ) in π / 2..π, log (sin x)

Tactic:
right

Goal state after:
| ∫ (x : ℝ) in π / 2..π, log (sin x)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
⊢ π = 0 ∨ ∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖ = 0

Tactic:
right

Goal state after:
a : ℂ
h : ‖a‖ = 1
⊢ ∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖ = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 4 - 4 * cos (x / 2) ^ 2 = 4 * sin (x / 2) ^ 2

Tactic:
nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
let C := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
  have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
  have hu : ∀ x ∈ [[a, b]],
      HasDerivAt (fun y => sin y ^ (n + 1)) ((n + 1 : ℕ) * cos x * sin x ^ n) x :=
    fun x _ => by simpa only [mul_right_comm] using! (hasDerivAt_sin x).pow (n + 1)
  have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by
    simpa only [neg_neg] using! (hasDerivAt_cos x).neg
  have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
  · calc
      (∫ x in a..b, sin x ^ (n + 2)) = ∫ x in a..b, sin x ^ (n + 1) * sin x := by
        simp only [_root_.pow_succ]
      _ = C + (↑n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n := by simp [H, h, sq]; ring
      _ = C + (↑n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) := by
        simp [cos_sq', sub_mul, ← pow_add, add_comm]
      _ = (C + (↑n + 1) * ∫ x in a..b, sin x ^ n) - (↑n + 1) * ∫ x in a..b, sin x ^ (n + 2) := by
        rw [integral_sub, mul_sub, add_sub_assoc] <;>
          apply Continuous.intervalIntegrable <;> fun_prop
  all_goals apply Continuous.intervalIntegrable; fun_prop

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

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ¬∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
right

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := ⋯
gray : E → ℂ → ℂ := ⋯
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ¬∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)