mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z = f w

Tactic:
circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ (2 * ↑π * I)⁻¹ • (2 * ↑π * I) • f w = f w
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
a : ℤ
⊢ x + ↑a ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ

Tactic:
simp only [mem_integerComplement_iff, not_iff_not]
  exact ⟨(Exists.elim · fun n hn ↦ ⟨n - a, by simp [hn]⟩),
    (Exists.elim · fun n hn ↦ ⟨n + a, by simp [hn]⟩)⟩

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

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

Tactic:
filter_upwards with x

Goal state after:
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 : ℂ
⊢ (⇑reCLM ∘ ⇑ofRealCLM ∘ Real.log ∘ ⇑normSq ∘ g) x = (⇑reCLM ∘ log ∘ (⇑conjCLE ∘ g * g)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case neg
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
⊢ x - 1 < x * log x

Tactic:
cases lt_or_eq_of_le h0

Goal state after:
case neg.inl
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h✝ : 0 < x
⊢ x - 1 < x * log x

case neg.inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h✝ : 0 = x
⊢ x - 1 < x * log x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case refine_2
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 t) volume

Tactic:
rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
    exact intervalIntegrable_cpow' h (a := 0) (b := t)

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

Goal state before:
pp: case hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 1

Tactic:
← neg_neg log

Goal state after:
case hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (- -log) volume 0 1
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 * π)))
⊢ ∀ᶠ (x : ℂ) in nhds w,
    AEStronglyMeasurable (fun θ ↦ herglotzRieszKernel 0 x (circleMap 0 R θ) • f (circleMap 0 R θ))
      (volume.restrict (uIoc 0 (2 * π)))

Tactic:
filter_upwards with x

Goal state after:
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 * π)))
x : ℂ
⊢ AEStronglyMeasurable (fun θ ↦ herglotzRieszKernel 0 x (circleMap 0 R θ) • f (circleMap 0 R θ))
    (volume.restrict (uIoc 0 (2 * π)))
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case pos
n : ℕ
x : ℝ
hn : ¬n = 0
hx : |x| ≤ 1
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

Tactic:
simp_all [pow_le_one₀, (posLog_eq_zero_iff _).2]

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

Goal state before:
pp: case insert
α : 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) ≤ ∑ t ∈ insert a s, log⁺ (f t)

Tactic:
| insert a s ha hs =>

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2

Tactic:
norm_add_le,

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log⁺ (‖a‖ + ‖b‖) ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
norm_add_le,

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ (‖circleMap 0 r θ‖ + ‖w‖) / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ (‖circleMap 0 r θ‖ + ‖w‖) / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
← norm_sub_norm_le

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ (‖circleMap 0 r θ‖ + ‖w‖) / (‖circleMap 0 r θ‖ - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)

case hd
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ 0 < ‖circleMap 0 r θ‖ - ‖w‖
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
r : ℂ
hr : r ∈ {0}ᶜ
⊢ (f ∘ invQParam h) r = cuspFunction h f r

Tactic:
rw [cuspFunction, update_of_ne hr]

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : z ∈ (derivative P).rootSet ℂ
⊢ z ∈ (convexHull ℝ) (P.rootSet ℂ)

Tactic:
rw [mem_rootSet, coe_aeval_eq_eval] at hz

Goal state after:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ z ∈ (convexHull ℝ) (P.rootSet ℂ)
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
z : ℂ
hz : z ∈ U
hfz : f z = 0
⊢ False

Tactic:
simpa [hfz, (ne_of_mem_of_not_mem hz hU₀).symm] using hf_inv z

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: a : ℂ
ha : 0 ≤ a
⊢ a.sqrt = ↑√a.re

Tactic:
by
  obtain ⟨α : ℝ, hα, rfl⟩ := RCLike.nonneg_iff_exists_ofReal.mp ha
  simp only [coe_algebraMap, ofReal_re]
  rw [← re_add_im (α : ℂ).sqrt, re_sqrt_ofReal]
  simp [sqrt, cpow_inv_two_im_eq_sqrt, abs_of_nonneg hα]

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

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
have h₂f : ¬∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u ≠ ⊤ := by aesop
    rw [← h₁f.exists_meromorphicOrderAt_ne_top_iff_forall
      ⟨nonempty_closedBall.mpr (abs_nonneg R), (convex_closedBall c |R|).isPreconnected⟩] at h₂f
    push Not at h₂f
    have : divisor f CB = 0 := by
      ext x
      by_cases h : x ∈ CB
      <;> simp_all [CB]
    simp only [CB, this, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, Int.cast_zero,
      zero_mul, finsum_zero, add_zero, zero_add]
    rw [MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top (by aesop), norm_zero, log_zero]
    have : f =ᶠ[codiscreteWithin CB] 0 := by
      filter_upwards [h₁f.meromorphicNFAt_mem_codiscreteWithin, self_mem_codiscreteWithin CB]
        with z h₁z h₂z
      simpa [h₂f ⟨z, h₂z⟩] using (not_iff_not.2 h₁z.meromorphicOrderAt_eq_zero_iff)
    rw [circleAverage_congr_codiscreteWithin (f₂ := 0) _ hR]
    · simp only [circleAverage, mul_inv_rev, Pi.zero_apply, intervalIntegral.integral_zero,
        smul_eq_mul, mul_zero]
    apply Filter.codiscreteWithin_mono (U := CB) sphere_subset_closedBall
    filter_upwards [this] with z hz
    simp_all

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: a : ℂ
ha : 0 ≤ a
⊢ (-a).sqrt = I * a.sqrt

Tactic:
by
  obtain ⟨α, hα, rfl⟩ := RCLike.nonneg_iff_exists_ofReal.mp ha
  rw [Complex.sqrt_of_nonneg ha]
  simp only [coe_algebraMap, ofReal_re]
  rw [← re_add_im (-(α : ℂ)).sqrt]
  simp [sqrt, cpow_inv_two_im_eq_sqrt, abs_of_nonneg hα, cpow_inv_two_re, mul_comm]

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

Goal state before:
pp: 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‖⁻¹)

Tactic:
· -- 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.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom (g * h) z = denom g (num h z / denom h z) * denom h z

Tactic:
by
  change _ = (_ * (_ / _) + _) * _
  field_simp [denom_ne_zero_of_im h hz]
  simp only [denom, Units.val_mul, mul_apply, Fin.sum_univ_succ, Finset.univ_unique,
    Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
    Complex.ofReal_mul, num]
  ring

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

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
⊢ g.IsElliptic

Tactic:
refine lt_of_not_ge fun hge ↦ ?_

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ ((∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x) → ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0

Tactic:
rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩)

Goal state after:
case mpr.inl
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (upperRightHom x) = 1 ∨ det (upperRightHom x) = -1
hg10 : ↑(upperRightHom x) 1 0 = 0
⊢ ↑(upperRightHom x) 0 0 = ↑(upperRightHom x) 1 1 ∧ ↑(upperRightHom x) 0 1 ≠ 0

case mpr.inr
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (-upperRightHom x) = 1 ∨ det (-upperRightHom x) = -1
hg10 : ↑(-upperRightHom x) 1 0 = 0
⊢ ↑(-upperRightHom x) 0 0 = ↑(-upperRightHom x) 1 1 ∧ ↑(-upperRightHom x) 0 1 ≠ 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = (algebraMap L (AlgebraicClosure L)) (∏ σ, σ x)

Tactic:
map_prod (algebraMap L (AlgebraicClosure L))

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    ∏ x_1, (algebraMap L (AlgebraicClosure L)) (x_1 x)
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x

Tactic:
convert!
    sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
      (hasStrictDerivAt_sinh _) using 2

Goal state after:
case e'_9.e'_3
x : ℝ
⊢ √(1 + x ^ 2) = cosh (↑sinhHomeomorph.toOpenPartialHomeomorph.symm x)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0

Tactic:
dist_ne_zero

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ x ≠ c
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c

Tactic:
dist_le_iff_le_sinh,

Goal state after:
a b c : ℍ
⊢ dist ↑a ↑c / (2 * √(a.im * c.im)) ≤ sinh ((dist a b + dist b c) / 2)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist z w ≤ dist ↑z ↑w / √(z.im * w.im)

Tactic:
dist_le_iff_le_sinh,

Goal state after:
z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (dist ↑z ↑w / √(z.im * w.im) / 2)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (dist ↑z ↑w / √(z.im * w.im) / 2)

Tactic:
← div_mul_eq_div_div_swap,

Goal state after:
z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist ↑z ↑(w.center |log z.im - log w.im|) = w.im * Real.sinh |log z.im - log w.im|

Tactic:
← abs_sinh,

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist ↑z ↑(w.center |log z.im - log w.im|) = w.im * |Real.sinh (log z.im - log w.im)|
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
⊢ T2Space (Quotient (MulAction.orbitRel G X))

Tactic:
rw [t2_iff_isClosed_diagonal]
  set R := MulAction.orbitRel G X
  let π : X → Quotient R := Quotient.mk'
  have : IsOpenQuotientMap (Prod.map π π) :=
    MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
  rw [← this.isQuotientMap.isClosed_preimage]
  convert! ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range
  · ext ⟨x₁, x₂⟩
    simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,
      exists_eq_right]
    rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
  all_goals infer_instance

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MulAction G X
inst✝³ : CompactlyGeneratedSpace (X × X)
inst✝² : T2Space X
inst✝¹ : DiscreteTopology G
inst✝ : ContinuousConstSMul G X
this : ContinuousSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

Tactic:
simp only [MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty, isCompact_iff_finite]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MulAction G X
inst✝³ : CompactlyGeneratedSpace (X × X)
inst✝² : T2Space X
inst✝¹ : DiscreteTopology G
inst✝ : ContinuousConstSMul G X
this : ContinuousSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → {g | (g • U ∩ V).Nonempty}.Finite
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
⊢ {h | ↑(Matrix.GeneralLinearGroup.det h) < 0} ∈ 𝓝 g

Tactic:
exact isOpen_Iio (a := (0 : ℝ)) |>.preimage (by fun_prop) |>.mem_nhds hg

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤

Tactic:
by
  calc proximity (f₁ * f₂) ⊤
    _ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 := by
      simp [proximity]
    _ ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 := by
      intro r
      apply circleAverage_mono
      · simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop
      · apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))
      · exact fun _ _ ↦ posLog_mul
    _ = circleAverage (log⁺ ‖f₁ ·‖) 0 + circleAverage (log⁺ ‖f₂ ·‖) 0 := by
      ext r
      apply circleAverage_add
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)
    _ = proximity f₁ ⊤ + proximity f₂ ⊤ := by simp [proximity]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)

Tactic:
unfold characteristic

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
⊢ proximity f ⊤ + logCounting f ⊤ - (proximity f⁻¹ ⊤ + logCounting f⁻¹ ⊤) =
    proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
h : Meromorphic f
R : ℝ
⊢ ‖(characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤) R‖ ≤ (log⁺ ‖a₀‖ + log 2) * ‖1 R‖

Tactic:
by simpa using abs_characteristic_sub_characteristic_shift_le h

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Measurable f
⊢ Measurable fun p ↦ cartanKernel f R p.1 p.2

Tactic:
by
  unfold cartanKernel; fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
he : ¬0 = e
⊢ ↑((single e n) e) * log (r * ‖e‖⁻¹) + ↑((single e n) 0) * log r = ↑n * (log r - log ‖e‖)

Tactic:
simp only [single_apply, he, reduceIte, Int.cast_zero, zero_mul, add_zero,
      log_mul (ne_of_lt (lt_of_lt_of_le (norm_pos_iff.mpr (he ·.symm)) hr)).symm
      (inv_ne_zero (norm_ne_zero_iff.mpr (he ·.symm))), log_inv]

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
he : ¬0 = e
⊢ ↑n * (log r + -log ‖e‖) = ↑n * (log r - log ‖e‖)
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ

Tactic:
rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono <;>
  apply connectedComponentIn_mono

Goal state after:
case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : (convexHull ℝ) (connectedComponentIn s x) = univ
⊢ s ⊆ s ∪ t

case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : (convexHull ℝ) (connectedComponentIn t x) = univ
⊢ t ⊆ s ∪ t
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case pos.refine_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : a ∈ closedBall 0 |r|
⊢ 0 ≤ ↑(((toClosedBall r) f) a)

Tactic:
simpa [h₂a] using h a

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs : (∀ a ∈ s, Meromorphic (f a)) → logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting (∑ a ∈ insert a s, f a) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r

Tactic:
| insert a s ha hs =>

Goal state after: