mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : (fun w ↦ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) - f z) =o[𝓝 z] fun w ↦ w - z
⊢ (fun w ↦ (∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - (w - z).im • f z) =o[𝓝 z] fun w ↦ w - z

Tactic:
by
    calc
      _ = fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (∫ _ in z.im..w.im, f z) := by simp
      _ =ᶠ[𝓝 z] fun w ↦ ∫ y in z.im..w.im, f (w.re + y * I) - f z := ?_
      _ =o[𝓝 z] fun w ↦ w - z := this
    refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w hw ↦ ?_⟩
    exact (intervalIntegral.integral_sub
      ((f_cont.mono (mem_ball_of_map_im_aux₂ hw)).comp (by fun_prop)
        (mapsTo_image _ _)).intervalIntegrable intervalIntegrable_const).symm

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ (log z).im ∈ Icc 0 (π / 2)

Tactic:
rw [log_im]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ z.arg ∈ Icc 0 (π / 2)
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x✝ y : ℂ
hy : y ∈ univ
x : ℂ
⊢ (fderiv ℝ (⇑reCLM) (F y) ∘SL fderiv ℝ F y) x = x.re • (fderiv ℝ f y) 1 + x.im • (fderiv ℝ f y) I

Tactic:
simp [(h₁F y).hasFDerivAt.restrictScalars ℝ |>.fderiv, g]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
rw [circleAverage, circleAverage, circleAverage, ← smul_sub]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    (2 * π)⁻¹ • ((∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

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

Tactic:
simp only [Function.comp_apply, Pi.add_apply, conjCLE_apply]

Goal state after:
case right
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
⊢ reCLM (log ((starRingEnd ℂ) (g x)) + log (g x)) = reCLM ((starRingEnd ℂ) (log (g x)) + log (g x))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x✝ : ℝ
⊢ sinc x✝ = dslope sin 0 x✝

Tactic:
simp [dslope, Function.update_apply, sinc, slope, div_eq_inv_mul]

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

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

Tactic:
by_cases hx : x = 0
  · simp [hx]
  · simp [sinc_of_ne_zero hx, sinc_of_ne_zero (neg_ne_zero.mpr hx)]

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

Goal state before:
pp: case inl
x : ℝ
hx : x < 0
⊢ sin x / x ≤ |x|⁻¹

Tactic:
abs_of_nonpos hx.le,

Goal state after:
case inl
x : ℝ
hx : x < 0
⊢ sin x / x ≤ (-x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)

Tactic:
rw [Finset.prod_insert ha]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ log ‖f x‖ = 0 x

Tactic:
simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ ContinuousOn (fun x ↦ ‖g (circleMap c R x)‖) [[0, 2 * π]]

Tactic:
apply ContinuousOn.norm
        apply h₁g.continuousOn.comp (t := sphere c |R|) (continuous_circleMap c R).continuousOn
        intro x hx
        simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ log ‖f x‖ = 0 x

Tactic:
simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
have : t + 1 ≠ 0 := by contrapose ht; rwa [add_eq_zero_iff_eq_neg] at ht
  apply integral_eq_sub_of_hasDerivAt
  · intro x _
    have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x := by
      convert! (hasDerivAt_pow 2 (x : ℂ)).const_add 1
      simp
    have g :
      ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z := by
      intro z hz
      convert!
        (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const
          (2 * (t + 1)) using 1
      simp [field]
    convert! (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1
    · ring
    · exact mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)
  · apply Continuous.intervalIntegrable
    refine continuous_ofReal.mul ?_
    apply Continuous.cpow (by fun_prop) continuous_const
    intro a
    norm_cast
    exact ofReal_mem_slitPlane.2 <| add_pos_of_pos_of_nonneg one_pos <| sq_nonneg a

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

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
⊢ ∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R

Tactic:
obtain ⟨ρ, hρ, h3, h4⟩ :
    ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by
    simpa only [ofPred_and, subset_inter_iff] using!
      nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1))

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h3 : AnalyticOnNhd ℂ f (closedBall z₀ ρ)
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
⊢ ∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖

Tactic:
have h_cos_law (r₁ : ℝ) :
      ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - Complex.arg ρ) := by
    rw [← ofReal_inj, ← normSq_eq_norm_sq, normSq_sub ]
    suffices (circleMap 0 r₁ θ * (conj) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]
    conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]
  have : (r₀ / R) * ‖circleMap 0 R θ - ρ‖ ^ 2 ≤ ‖circleMap 0 r θ - ρ‖ ^ 2 := by
    rw [div_mul_eq_mul_div, div_le_iff₀ hR]
    nlinarith [h_cos_law r, h_cos_law R, mul_le_mul_of_nonneg_left hr₀r hR.le,
      mul_le_mul_of_nonneg_left hrR hR.le, neg_one_le_cos, cos_le_one]
  grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Goal state after:
case inl
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a : ℂ
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) 0 =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0

case inr
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f + g) = cuspFunction h f + cuspFunction h g

Tactic:
by
  simp only [cuspFunction]
  ext y
  obtain hy | rfl := ne_or_eq y 0
  · simp [hy]
  · simpa using! (tendsto_nhds_limUnder ⟨_, tendsto_nhds_zero hfcts⟩).add
      (tendsto_nhds_limUnder ⟨_, tendsto_nhds_zero hgcts⟩) |>.limUnder_eq

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ},
    IsOpen U → IsSimplyConnected U → U ≠ univ → 0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
⊢ 0 ∉ -a +ᵥ U

Tactic:
by simpa [mem_vadd_set_iff_neg_vadd_mem]

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
⊢ circleAverage (∑ᶠ (u : ℂ), fun x ↦ ↑(D u) * log ‖x - u‖) c R = ∑ᶠ (u : ℂ), ↑(D u) * log R

Tactic:
have h := D.finiteSupport (isCompact_closedBall c |R|)
  calc circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
  _ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop
  _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R := by
    rw [circleAverage_sum]
    intro u hu
    apply IntervalIntegrable.const_mul
    apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm
  _ = ∑ u ∈ h.toFinset, D u * log R := by
    apply Finset.sum_congr rfl
    intro u hu
    simp_rw [← smul_eq_mul, circleAverage_fun_smul]
    congr
    rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
    apply D.supportWithinDomain
    simp_all
  _ = ∑ᶠ u, D u * log R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ k ≃o ↑(Ioo (-1) 1)

Tactic:
refine StrictMono.orderIsoOfRightInverse ?_ ?_ (fun x ↦ x / (1 - |↑x|)) ?_
  · refine codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 ?_
    have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)
    calc
      |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
      _ < 1 := (div_lt_one H).2 (lt_one_add _)
  · refine (strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _
    · intro x
      simp only [abs_neg, neg_div]
    · rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy
      simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff₀, hx.trans_lt (lt_one_add _),
        hy.trans_lt (lt_one_add _), *]
  · refine fun x ↦ Subtype.ext ?_
    have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)
    simp [field, abs_div, abs_of_pos this]

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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_

Goal state after:
case refine_1
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r)

case refine_2
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

case refine_3
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case refine_1
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : E
⊢ (Metric.closedBall 0 1).piecewise id g x ∈ Metric.closedBall 0 1

Tactic:
by_cases hx : x ∈ Metric.closedBall 0 1

Goal state after:
case pos
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : E
hx : x ∈ Metric.closedBall 0 1
⊢ (Metric.closedBall 0 1).piecewise id g x ∈ Metric.closedBall 0 1

case neg
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : E
hx : x ∉ Metric.closedBall 0 1
⊢ (Metric.closedBall 0 1).piecewise id g x ∈ Metric.closedBall 0 1
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
⊢ ∃ g, ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g, hg⟩ := (ι.comp f).exists_restrict_eq hs
    use r.comp g
    ext1 x
    have := congr(r.comp $(hg))
    rw [← r.comp_assoc ι, h, f.id_comp] at this
    congrm($this x)

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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ g • x

Tactic:
by
    simp_rw [continuous_induced_rng (f := UpperHalfPlane.coe), Function.comp_def,
      UpperHalfPlane.coe_smul, UpperHalfPlane.σ]
    refine .comp ?_ ?_
    · split_ifs
      exacts [continuous_id, continuous_conj]
    · refine .div ?_ ?_ (fun x ↦ denom_ne_zero g x) <;>
      exact (continuous_const.mul continuous_coe).add continuous_const

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: ⊢ Tendsto (↑ofComplex) (comap Complex.im atTop) atImInfty

Tactic:
by
  simp only [atImInfty, tendsto_comap_iff, Function.comp_def]
  refine tendsto_comap.congr' ?_
  filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz
  simp [ofComplex_apply_of_im_pos hz]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
hay : a < (g + dg) y
x : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : g y ≤ c
⊢ (g + dg) y ≤ b

Tactic:
calc
        g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2
        _ = b := by rw [hsub, add_sub_cancel]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases hne with ⟨c, hc⟩

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
he : IsClosedEmbedding e
h✝ : IsEmpty X
c : ℝ
hc : c ∈ t
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ (norm R) (LinearMap.det ((lmul S A) a)) = (norm R) a

Tactic:
norm_apply R a,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ (norm R) (LinearMap.det ((lmul S A) a)) = LinearMap.det ((lmul R A) a)