mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (volume.real (Ioc b a))⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
Real.volume_real_Ioc_of_le h.le,

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case calc_2.calc.step
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
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ I₁ - (↑w.re - ↑z.re) • f z + I • (I₂ - (↑w.im - ↑z.im) • f z) =
    ((fun w ↦ (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - (w - z).re • f z) +
        I • fun w ↦ (∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - (w - z).im • f z)
      w

Tactic:
congr <;> simp

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ0' : μ s ≠ 0
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
obtain ⟨c, hc, heq⟩ := exists_eq_setAverage (isConnected_uIoo h) (hf.mono uIoo_subset_uIcc_self)
    (hint.mono_set hs') (measure_ne_top_of_subset hs' hμfin) hμ0'

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ0' : μ s ≠ 0
c : ℝ
hc : c ∈ uIoo a b
heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..η + 2 * π, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)

Tactic:
add_comm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)

Tactic:
simp only [circleAverage, mul_inv_rev]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ (π⁻¹ * 2⁻¹) • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) =
    (π⁻¹ * 2⁻¹) • ∫ (θ : ℝ) in η..2 * π + η, f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ) = ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)

Tactic:
exact intervalIntegral.integral_congr (fun x ↦ by simp [hf (circleMap_mem_sphere' c R x)])

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
⊢ ∃ F, AnalyticOnNhd ℂ F univ ∧ (fun z ↦ (F z).re) = f

Tactic:
let g := ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I)
  have hg : Differentiable ℂ g :=
    fun x ↦ (HarmonicAt.differentiableAt_complex_partial (hf x (mem_univ x)))
  obtain ⟨F, hF⟩ := hg.isExactOn_univ.with_val_at 0 (f 0)
  have h₁F : ∀ z₁, HasDerivAt F (g z₁) z₁ := by simp_all
  have h₂F : Differentiable ℂ F := fun x ↦ (h₁F x).differentiableAt
  have h₃F : Differentiable ℝ F := h₂F.restrictScalars (𝕜 := ℝ)
  use F, (h₂F.differentiableOn).analyticOnNhd isOpen_univ
  ext x
  rw [← Complex.reCLM_apply, ← Function.comp_apply (f := reCLM)]
  refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
  case hd => exact hf.contDiffOn.differentiableOn two_ne_zero
  case heq =>
    intro y hy
    simp only [fderivWithin_univ]
    rw [fderiv_comp y (by fun_prop) (by fun_prop)]
    ext x
    trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))
    · simp only [map_smul, map_add]
      simp [(h₁F y).hasFDerivAt.restrictScalars ℝ |>.fderiv, g]
    · simp
  all_goals simp_all

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
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
⊢ ‖f (-z)‖ ≤ C

Tactic:
change ‖(f ∘ Neg.neg) z‖ ≤ C

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

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

Tactic:
change ‖(f ∘ Neg.neg) z‖ ≤ C

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

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
h_subst : (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)
this :
  R * R * normSq (cexp (↑θ * I)) + r * r * normSq (cexp (↑φ * I)) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)
⊢ (‖↑R * cexp (↑θ * I)‖ ^ 2 - ‖↑r * cexp (↑φ * I)‖ ^ 2) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2 =
    (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

Tactic:
← this

Goal state after:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
h_subst : (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)
this :
  R * R * normSq (cexp (↑θ * I)) + r * r * normSq (cexp (↑φ * I)) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)
⊢ (‖↑R * cexp (↑θ * I)‖ ^ 2 - ‖↑r * cexp (↑φ * I)‖ ^ 2) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2 =
    (R ^ 2 - r ^ 2) /
      (R * R * normSq (cexp (↑θ * I)) + r * r * normSq (cexp (↑φ * I)) -
        2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)))
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: 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
⊢ (-f) z ≠ 0

Tactic:
simpa

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

Goal state before:
pp: ⊢ sinc = dslope sin 0

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

Goal state after:
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
x : ℝ
hx : x ∈ Ioc 0 (-c)
⊢ (cos (r * π) • fun x ↦ x ^ r) x = (fun x ↦ (-x) ^ r) x

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, log_neg_eq_log, mul_comm,
      rpow_def_of_pos hx.1, rpow_def_of_neg (by linarith [hx.1] : -x < 0)]

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

Goal state before:
pp: R : ℝ
w c : ℂ
hw : w ∈ ball c R
⊢ Disjoint {w} (ball c R)ᶜ

Tactic:
simpa

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

Goal state before:
pp: case hbc
a b x : ℝ
hx✝ : 0 < x
hx : 0 ∉ [[1, x]]
⊢ [[1, x]] ⊆ {0}ᶜ

Tactic:
simpa

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

Goal state before:
pp: case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c ↦ ↑c ^ (r + 1) / (r + 1)) [[0, c]]

pp: case hderiv
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c), HasDerivWithinAt (fun c ↦ ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x

pp: case hint
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y ↦ ↑y ^ r) MeasureTheory.volume 0 c

Tactic:
· refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn
    rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]

Goal state after:
case hderiv
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c), HasDerivWithinAt (fun c ↦ ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x

case hint
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y ↦ ↑y ^ r) MeasureTheory.volume 0 c
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case hg
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 ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ ContinuousOn (fun x ↦ log ‖g x‖) [[a, b]]

Tactic:
apply h₁g.continuousOn.norm.log

Goal state after:
case hg
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 ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ ∀ x ∈ [[a, b]], ‖g x‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) = 2 * ↑r * ↑(sinc r)

Tactic:
rw [integral_exp_mul_I_eq_sin]
  by_cases hr : r = 0
  · simp [hr]
  rw [sinc_of_ne_zero hr]
  norm_cast
  field

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

Goal state before:
pp: 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ t ∈ ball 0 r, gray w t = g z₀
h4 : ‖z - z₀‖ < r
⊢ ↑‖z - z₀‖ ∈ ball 0 r

Tactic:
simpa

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

Goal state before:
pp: q : ℤ[X]
this : q.natDegree = 0
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
⊢ IsUnit (q.coeff 0)

Tactic:
← this

Goal state after:
q : ℤ[X]
this : q.natDegree = 0
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
⊢ IsUnit (q.coeff q.natDegree)
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
⊢ IsSimplyConnected (-a +ᵥ U)

Tactic:
simpa

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 ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), 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 : divisor f CB = 0 := by
      ext x
      by_cases h : x ∈ CB
      <;> simp_all [CB]

Goal state after:
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 ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this : divisor f CB = 0
⊢ 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‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ 0 ≤ (complexRingEquiv h) a

Tactic:
simpa

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
⊢ sqrt a = ↑√(re a)

Tactic:
by
  obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
  · simp [h, sqrt_eq_ite]
  rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, Complex.sqrt_of_nonneg (by simpa)]
  simp

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 : ‖c - u‖ ≤ |R|
h2 : |r| < ‖c - u‖
this : ‖c - u‖ ≠ 0
⊢ 1 ≤ |R * ‖c - u‖⁻¹|

Tactic:
simpa [field]

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
⊢ Real.log M - Real.log ‖f c‖ = Real.log (M / ‖f c‖)

Tactic:
by rw [← log_div (by linarith) (norm_ne_zero_iff.mpr h₂f)]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g).det
hell : g.IsElliptic
this : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → ∀ (hell : g.IsElliptic), 0 < ↑g 1 0 → (g • z = z ↔ z = fixedPt g hell)
hc : ↑g 1 0 < 0
⊢ 0 < ↑(-g) 1 0

Tactic:
simpa

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

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |↑(-↑N * ⌊z.re / ↑N⌋) + z.re| ≤ ↑N

Tactic:
add_comm

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |z.re + ↑(-↑N * ⌊z.re / ↑N⌋)| ≤ ↑N
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f

Tactic:
have hg_dist : ∀ n, dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n := by
    intro n
    calc
      dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖ := by
        rw [g_succ, dist_eq_norm', add_sub_cancel_left]
      _ ≤ ‖f - (g n).compContinuous e‖ / 3 := hF_norm _
      _ = 1 / 3 * dist ((g n).compContinuous e) f := by rw [dist_eq_norm', one_div, div_eq_inv_mul]
      _ ≤ 1 / 3 * ((2 / 3) ^ n * ‖f‖) := mul_le_mul_of_nonneg_left (hgf n) (by norm_num1)
      _ = 1 / 3 * ‖f‖ * (2 / 3) ^ n := by ac_rfl

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
have : (f' M'.det).det = ((M'.map f').comp m m n n R[X]).det := by
      refine sub_eq_zero.mp <| mem_nonZeroDivisors_iff_right.mp
        (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by
          grind [Fintype.card_subtype_compl, Fintype.card_unique])
      rw [polyToMatrix_cornerAddX, ← charpoly]
      exact (Matrix.charpoly_monic _).mem_nonZeroDivisors

Goal state after:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
this : (f' M'.det).det = ((comp m m n n R[X]) (M'.map ⇑f')).det
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑(extChartAt 𝓘(ℂ, ℂ) (g • τ)) ∘ fun τ ↦ g • τ) τ

Tactic:
simpa [glPos_smul_def hg] using! (contMDiff_num g τ).mul (contMDiff_inv_denom g τ)

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (↑(Algebra.leftMulMatrix bS) ((toMatrix bA bA) f).det).det

Tactic:
det_det,

Goal state after:
case inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = ((Matrix.comp ιA ιA ιS ιS R) (((toMatrix bA bA) f).map ⇑↑(Algebra.leftMulMatrix bS))).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : y ∈ (minpoly K x).aroots (AlgebraicClosure ↥F)
this : (aeval y) (Polynomial.map (algebraMap R K) (minpoly R x)) = 0
⊢ eval₂ (algebraMap R (AlgebraicClosure ↥F)) y (minpoly R x) = 0

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
norm_eq_one_of_not_module_finite

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = 1 ^ finrank (↥K⟮x⟯) L

case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite K ↥K⟮x⟯
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
H : Module.Finite K ↥K⟮x⟯
⊢ IsIntegral K x

Tactic:
← isIntegral_gen

Goal state after:
case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
H : Module.Finite K ↥K⟮x⟯
⊢ IsIntegral K (gen K x)