mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

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

Tactic:
intro x hx

Goal state after:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
⊢ HasDerivAt (fun x ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
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 ∈ Ioo 0 c, 0 ≤ x ^ r

Tactic:
intro x hx

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 : ℝ
hx : x ∈ Ioo 0 c
⊢ 0 ≤ x ^ r
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x ↦ x ^ r) (Ι 0 (-c)) volume
⊢ EqOn (cos (r * π) • fun x ↦ x ^ r) (fun x ↦ (-x) ^ r) (Ι 0 (-c))

Tactic:
intro x hx

Goal state after:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x ↦ x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ (cos (r * π) • fun x ↦ x ^ r) x = (fun x ↦ (-x) ^ r) x
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:

Tactic:
‖q * x‖ = q * ‖x‖ := by simp [abs_of_pos h₁q]
      _ ≤ q * R := by gcongr
      _ < 1 * R := by gcongr
      _ = ‖W‖ := by simp [W, abs_of_pos hR]

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

Goal state before:
pp: case neg.inr.refine_1
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ AEStronglyMeasurable (fun x ↦ ↑x ^ r) (μ.restrict (Ι a b))

Tactic:
refine (measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable

Goal state after:
case neg.inr.refine_1
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ ContinuousOn (fun x ↦ ↑x ^ r) {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

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

Tactic:
intro x hx

Goal state after:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ EqOn (fun x ↦ x ^ r.re) (fun t ↦ ‖↑t ^ r‖) (Ι 0 c)

Tactic:
intro x hx

Goal state after:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ (fun x ↦ x ^ r.re) x = (fun t ↦ ‖↑t ^ r‖) x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
⊢ ∀ (x : ℝ), 0 < x → IntervalIntegrable log volume 0 x

Tactic:
intro x hx

Goal state after:
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 x
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x y : ℝ
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
by_cases ha : x = 0
  · simp [ha, posLog]
  by_cases hb : y = 0
  · simp [hb, posLog]
  unfold posLog
  nth_rw 1 [← add_zero 0, log_mul ha hb]
  exact max_add_add_le_max_add_max

Goal state after:
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 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : ‖2‖ = 2
⊢ ‖(2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)‖ ≤ 2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖

Tactic:
rw [norm_smul, norm_div, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_pow,
      div_eq_mul_inv, h₁]

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 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : ‖2‖ = 2
⊢ 2 * R * (‖circleMap 0 R θ - x‖ ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖ ≤ 2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)

Tactic:
by
  rw [sub_div]
  have hr : r + 1 ≠ 0 := by
    rcases h with h | h
    · apply_fun Complex.re
      rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne, add_eq_zero_iff_eq_neg]
      exact h.ne'
    · rw [Ne, ← add_eq_zero_iff_eq_neg] at h; exact h.1
  by_cases hab : (0 : ℝ) ∉ [[a, b]]
  · apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_)
      (intervalIntegrable_cpow (r := r) <| Or.inr hab)
    refine hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_
    contrapose hr; rwa [add_eq_zero_iff_eq_neg]
  replace h : -1 < r.re := by tauto
  suffices ∀ c : ℝ, (∫ x : ℝ in 0..c, (x : ℂ) ^ r) =
      (c : ℂ) ^ (r + 1) / (r + 1) - (0 : ℂ) ^ (r + 1) / (r + 1) by
    rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
      (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]
    ring
  intro c
  apply integral_eq_sub_of_hasDeriv_right
  · refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn
    rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]
  · refine fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt
    · rcases le_total c 0 with (hc | hc)
      · rw [max_eq_left hc] at hx; exact hx.2.ne
      · rw [min_eq_left hc] at hx; exact hx.1.ne'
    · contrapose hr; rw [hr]; ring
  · exact intervalIntegrable_cpow' h

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

Goal state before:
pp: a b : ℝ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
by
  replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := mod_cast h
  exact mod_cast integral_rpow h

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

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2

Tactic:
have := @integral_pow a b 1
  norm_num at this
  exact this

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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖1 - x * a‖) (closedBall 0 |1|)

Tactic:
intro x hx

Goal state after:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : x ∈ closedBall 0 |1|
⊢ InnerProductSpace.HarmonicAt (fun x ↦ log ‖1 - x * a‖) x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inl
b : ℝ
h : b < 0
⊢ -∫ (x : ℝ) in -0..-b, log x = b * log b - b

Tactic:
neg_zero,

Goal state after:
case inl
b : ℝ
h : b < 0
⊢ -∫ (x : ℝ) in 0..-b, log x = b * log b - b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hcont
a b : ℝ
⊢ ContinuousOn cos [[a, b]]

Tactic:
· exact continuousOn_cos

Goal state after:
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‖
⊢ Set.MapsTo (circleMap c R) [[0, 2 * π]] (sphere c |R|)

Tactic:
intro x hx

Goal state after:
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‖
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ circleMap c R x ∈ sphere c |R|
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Set.EqOn (fun x ↦ log ‖circleMap 0 1 x - 1‖) (fun x ↦ log (4 * sin (x / 2) ^ 2) / 2) [[0, 2 * π]]

Tactic:
intro x hx

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ (fun x ↦ log ‖circleMap 0 1 x - 1‖) x = (fun x ↦ log (4 * sin (x / 2) ^ 2) / 2) x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case h₀
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‖
⊢ ∀ x ∈ [[0, 2 * π]], ‖g (circleMap c R x)‖ ≠ 0

Tactic:
intro x hx

Goal state after:
case h₀
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‖
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ ‖g (circleMap c R x)‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖x - a‖) (closedBall 0 |1|)

Tactic:
intro x hx

Goal state after:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : x ∈ closedBall 0 |1|
⊢ InnerProductSpace.HarmonicAt (fun x ↦ log ‖x - a‖) x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
by
  simp [field, integral_sin_pow, add_sub_assoc]

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

Goal state before:
pp: c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
g : ℂ → ℝ
x : ℂ
⊢ (x ∈ Function.support fun u ↦ ↑(D u) * g u) → x ∈ ↑(Finite.toFinset hD)

Tactic:
simp +contextual

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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ |x / (1 + |x|)| < 1

Tactic:
calc
      |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
      _ < 1 := (div_lt_one H).2 (lt_one_add _)

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

Goal state before:
pp: 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 ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
⊢ (divisor f CB) x = 0 x

Tactic:
by_cases h : x ∈ CB
      <;> simp_all [CB]

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

Goal state before:
pp: case neg
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 : ℂ
h1 : u ∉ closedBall c |R|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
have : u ∉ closedBall c |r| := by
          simp_all
          linarith

Goal state after:
case neg
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 : ℂ
h1 : u ∉ closedBall c |R|
this : u ∉ closedBall c |r|
⊢ ↑((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.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
hge : 0 ≤ (↑g).discr
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑(↑g).discr

Tactic:
simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]

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
⊢ (↑(↑g 1 1) - ↑(↑g 0 0)) ^ 2 + 4 * ↑(↑g 1 0) * ↑(↑g 0 1) =
    (↑(↑g 0 0) + ↑(↑g 1 1)) ^ 2 - 4 * (↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = Complex.I ^ 2 * ↑(-(↑g).discr)

Tactic:
simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ (↑(↑g 1 1) - ↑(↑g 0 0)) ^ 2 + 4 * ↑(↑g 1 0) * ↑(↑g 0 1) =
    (↑(↑g 0 0) + ↑(↑g 1 1)) ^ 2 - 4 * (↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: this : Continuous fun t ↦ Complex.I * ↑t
⊢ ∀ (x : { x // x ∈ Ioi 0 }),
    ((fun t ↦ Complex.I * ↑t) ∘ Subtype.val) x =
      (UpperHalfPlane.coe ∘
          (Ioi 0).domRestrict fun t ↦
            if hw : 0 < (↑I * ↑t).im then { coe := ↑I * ↑t, coe_im_pos := hw } else Classical.choice ⋯)
        x

Tactic:
simp +contextual

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

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ ↑ofComplex) ↑τ

Tactic:
rw [← mdifferentiableAt_iff_differentiableAt]

Goal state after:
f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ ↑ofComplex) ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
⊢ ∏ i ∈ s, f i = 0 ↔ ∃ i ∈ s, f i = 0

Tactic:
refine ⟨fun h0 ↦ ?_, fun ⟨i, hi, hi'⟩ ↦ Finset.prod_eq_zero hi hi'⟩

Goal state after:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
⊢ ∃ i ∈ s, f i = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) (gen K x) ^ Fintype.card (Free.ChooseBasisIndex (↥F) L) = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
finrank_eq_card_chooseBasisIndex

Goal state after:
case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) (gen K x) ^ Fintype.card (Free.ChooseBasisIndex (↥F) L) =
    (norm K) (gen K x) ^ Fintype.card (Free.ChooseBasisIndex (↥K⟮x⟯) L)
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]

Goal state after:
x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (x + √(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case inr
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ

Tactic:
convert! Complex.conjCLE.hasStrictFDerivAt.neg.comp _ (this (J * g) (by simpa))

Goal state after:
case e'_11
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
x✝ : ℂ
⊢ ↑(g • ↑ofComplex x✝) = (-⇑Complex.conjCLE) ↑((J * g) • ↑ofComplex x✝)

case e'_12
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
e_4✝ : Complex.addCommGroup = Complex.instNormedAddCommGroup.toAddCommGroup
e_5✝ : instInnerProductSpaceRealComplex.toModule ≍ instInnerProductSpaceRealComplex.toModule
⊢ smulFDeriv g ↑τ = (-↑Complex.conjCLE) ∘SL smulFDeriv (J * g) ↑τ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) sinh)

Tactic:
by simp [differentiable_iteratedDeriv_sinh]

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

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) sinh)

Tactic:
by simp [differentiable_iteratedDeriv_sinh]

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

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

Tactic:
by
  rw [← div_le_iff₀' w.im_pos, ← exp_log z.im_pos, ← exp_log w.im_pos, ← Real.exp_sub, exp_le_exp]
  exact (le_abs_self _).trans (dist_log_im_le z w)

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c

Tactic:
let b' : Ultrafilter (Ultrafilter α) := b.map pure
     have t : ↑b' ≤ 𝓝 b := ultrafilter_converges_iff.mpr (bind_pure _).symm
     rw [← h]
     have := (continuous_ultrafilter_extend f).tendsto b
     refine le_trans ?_ (le_trans (map_mono t) this)
     change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b
     rw [ultrafilter_extend_extends]
     exact le_rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X : TopCat
Y : CompHaus
f : ↑(stoneCechObj X).toTop → ↑Y.toTop
hf : Continuous f
x : ↑(of (fun x ↦ True) (StoneCech ↑X)).toTop
⊢ Set.EqOn (stoneCechExtend ⋯) f (Set.range stoneCechUnit)

Tactic:
rintro _ ⟨y, rfl⟩

Goal state after:
X : TopCat
Y : CompHaus
f : ↑(stoneCechObj X).toTop → ↑Y.toTop
hf : Continuous f
x : ↑(of (fun x ↦ True) (StoneCech ↑X)).toTop
y : ↑X
⊢ stoneCechExtend ⋯ (stoneCechUnit y) = f (stoneCechUnit y)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact {g | (g • U ∩ V).Nonempty}

Tactic:
convert!
    ((ProperSMul.isProperMap_smul_pair (G := G)).isCompact_preimage (hV.prod hU)).image
      continuous_fst
  ext g
  suffices (∃ v, v ∈ g • U ∧ v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U by simpa
  rw [← (MulAction.toPerm g).exists_congr_right]
  simp [and_comm]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
· rw [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, specializes_coe]
    apply specializes_or_disjoint_nhds

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)

Tactic:
· exact h (CompHaus.of (ULift.{u} (OnePoint ℕ))) ⟨g, by fun_prop⟩

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

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ ∀ (a : GL (Fin 2) ℝ × ℍ),
    σ a.1 = σ g → (σ g) (num a.1 ↑a.2 / denom a.1 ↑a.2) = (σ a.1) (num a.1 ↑a.2 / denom a.1 ↑a.2)

Tactic:
simp +contextual

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
intro x hx

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
hx : x ∈ sphere 0 |r|
⊢ log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r ≤ ∑ c ∈ s, circleAverage (fun x ↦ log⁺ ‖f c x‖) 0 r + log ↑s.card

Tactic:
calc circleAverage (log⁺ ‖∑ c ∈ s, f c ·‖) 0 r
    _ ≤ circleAverage (∑ c ∈ s, log⁺ ‖f c ·‖ + log s.card) 0 r := by
      apply circleAverage_mono
      · apply (Meromorphic.fun_sum hf).meromorphicOn.circleIntegrable_posLog_norm
      · fun_prop
      · intro x hx
        rw [add_comm]
        apply posLog_norm_sum_le
    _ = ∑ c ∈ s, circleAverage (log⁺ ‖f c ·‖) 0 r + log s.card := by
      nth_rw 2 [← circleAverage_const (log s.card) 0 r]
      rw [← circleAverage_sum h₂f, ← circleAverage_add (CircleIntegrable.sum s h₂f)
        (circleIntegrable_const (log s.card) 0 r)]
      congr 1
      ext x
      simp

Goal state after: