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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
x : 𝕜
hx : D x ≠ 0
⊢ ‖z - x‖ ^ D x ≠ 0

Tactic:
rw [ne_eq, zpow_eq_zero_iff hx, norm_eq_zero, sub_eq_zero, eq_comm]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
x : 𝕜
hx : D x ≠ 0
⊢ ¬x = z
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
⊢ toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (SpecialLinearGroup n R)

Tactic:
if hn : IsEmpty n then simp [Subgroup.center_eq_top] else
  replace hn : Nonempty n := by simpa using hn
  obtain ⟨i⟩ := hn
  simp only [GeneralLinearGroup.center_eq_range_scalar, MonoidHom.mem_range,
    mem_center_iff, scalar_apply]
  refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, by simpa [Units.ext_iff] using congr(GeneralLinearGroup.det $hr),
    by simpa [Units.ext_iff] using hr⟩, fun ⟨r, hr1, hr⟩ ↦ ⟨⟨r, g⁻¹.1 i i, ?_, ?_⟩,
      by simp [Units.ext_iff, hr]⟩⟩
  · simpa [-mul_inv_cancel, ← hr, ← pow_succ',
      Nat.sub_one_add_one Fintype.card_pos.ne.symm] using
        Matrix.ext_iff.2 (Subtype.ext_iff.1 (mul_inv_cancel g)) i i
  · simpa [-inv_mul_cancel, ← hr] using Matrix.ext_iff.2 (Subtype.ext_iff.1 (inv_mul_cancel g)) i i

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
⊢ Preperfect (closedBall 0 R)

Tactic:
← closure_ball 0 hR.ne'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
⊢ Preperfect (closure (ball 0 R))
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := ⋯
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯
⊢ Set.MapsTo ((fun x_1 ↦ (x_1, (↑q (Γ (t n))).2)) ∘ γ.toFun) (Set.Icc 0 (t (n + 1)) ∩ closure {a | ¬a ≤ t n}) q.target

Tactic:
not_le,

Goal state after:
case succ.refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
⊢ Set.MapsTo ((fun x_1 ↦ (x_1, (↑q (Γ (t n))).2)) ∘ γ.toFun) (Set.Icc 0 (t (n + 1)) ∩ closure {a | t n < a}) q.target
Module: Mathlib.Topology.Homotopy.Lifting

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

Tactic:
rw [h₁, Function.comp_apply, ContinuousMap.curry_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
⊢ z ∈ {x}ᶜ →
    deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z → deriv f z = (z - x) ^ (n - 1) • (↑n • g z + (z - x) • deriv g z)

Tactic:
hmem

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
⊢ deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z → deriv f z = (z - x) ^ (n - 1) • (↑n • g z + (z - x) • deriv g z)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

Tactic:
by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1
    -- `1 ≤ sSupNormIm f 1`
    · apply le_trans _ (le_max_left _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_one_of_one_le_of_nonpos
        hM1_one (Right.neg_nonpos_iff.mpr hset.1)]
    -- `0 < sSupNormIm f 1 < 1`
    · rw [not_le] at hM1_one; apply le_trans _ (le_max_right _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 1)
        (le_of_lt hM1_one) (neg_le_neg_iff.mpr hset.2)]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

Tactic:
refine hB.mono ?_
  rintro _ ⟨z, hz, rfl⟩
  exact ⟨l + z * (u - l), scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hz, rfl⟩

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 : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
⊢ ∃ R, |z.re| < R ∧ ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
refine ((eventually_gt_atTop _).and ?_).exists
    rcases hO.exists_pos with ⟨A, hA₀, hA⟩
    simp only [isBigOWith_iff, eventually_inf_principal, eventually_comap, mem_Ioo,
      mem_preimage, (· ∘ ·), Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at hA
    suffices
        Tendsto (fun R => expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0) by
      filter_upwards [this.eventually (ge_mem_nhds hC₀), hA] with R hR Hle w hre him
      calc
        ‖g ε w • f w‖ ≤ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) := ?_
        _ ≤ C := hR
      rw [norm_smul, Real.exp_add, ← hre, Real.exp_add, Real.exp_log hA₀, mul_assoc, mul_comm _ A]
      gcongr
      exacts [hδ <| Ioo_subset_Icc_self him, Hle _ hre him]
    refine Real.tendsto_exp_atBot.comp ?_
    suffices H : Tendsto (fun R => δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0)) by
      rw [mul_zero, add_zero] at H
      refine Tendsto.atBot_add ?_ tendsto_const_nhds
      simpa only [id, (· ∘ ·), add_mul, mul_assoc, ← div_eq_inv_mul, ← Real.exp_sub, ← sub_mul,
        sub_sub_cancel]
        using H.neg_mul_atTop δ₀ <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop hd₀
    refine tendsto_const_nhds.add (tendsto_const_nhds.mul ?_)
    exact tendsto_inv_atTop_zero.comp <| Real.tendsto_exp_atTop.comp <|
      tendsto_id.const_mul_atTop (sub_pos.2 hcd)

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 (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ 0 ∈ closure (Ioi 0 ×ℂ Ioi 0)

Tactic:
simp [closure_reProdIm, mem_reProdIm]

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

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
⊢ circleAverage f c R = f c

Tactic:
have h : CircleIntegrable f c R :=
    (hf.continuousOn_ball.mono sphere_subset_closedBall).circleIntegrable'

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
⊢ circleAverage f c R = f c
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
obtain ⟨e, h₁e, h₂e⟩ := (isCompact_closedBall c R).exists_thickening_subset_open
    (isOpen_setOfPred_harmonicAt f) (by aesop)

Goal state after:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : thickening e (closedBall c R) ⊆ {x | HarmonicAt f x}
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

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

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x : ℂ) ^ r‖) μ 0 c from
    (this a).symm.trans (this b)

Goal state after:
case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x ↦ ‖↑x ^ r‖) μ 0 c
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)

pp: case hs
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)

Tactic:
· intro x hx
        rw [uIoc_of_le hc] at hx
        dsimp only
        rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]

Goal state after:
case hs
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)
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₁ : circleMap 0 R θ - x ≠ 0
h₃ :
  HasDerivAt ((fun x ↦ circleMap 0 R θ + x) / fun x ↦ circleMap 0 R θ - x)
    ((1 * (circleMap 0 R θ - x) - (circleMap 0 R θ + x) * -1) / (circleMap 0 R θ - x) ^ 2) x
⊢ HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ)) (2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) x

Tactic:
simpa [herglotzRieszKernel_def, sub_zero, sub_sub, ← two_mul, Pi.div_def] using h₃

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

Goal state before:
pp: case pos.hf
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‖
i : ℝ
⊢ IntervalIntegrable (fun x ↦ log ‖x - i‖) volume a b

Tactic:
(by ring : a = ((a - i) + i)),

Goal state after:
case pos.hf
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‖
i : ℝ
⊢ IntervalIntegrable (fun x ↦ log ‖x - i‖) volume (a - i + i) b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0..b - a, x ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
by simp [abs_of_nonneg (sub_nonneg.2 hab)]

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

Goal state before:
pp: case pos.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‖
⊢ CircleIntegrable (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) c R

Tactic:
apply CircleIntegrable.finsum
      intro i
      apply IntervalIntegrable.const_mul
      apply MeromorphicOn.intervalIntegrable_log_norm
      apply AnalyticOnNhd.meromorphicOn
      apply AnalyticOnNhd.sub _ analyticOnNhd_const
      apply (analyticOnNhd_circleMap c R).mono (by tauto)

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

Goal state before:
pp: case neg
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 = ⊤
this : (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
apply CircleIntegrable.congr_codiscreteWithin this.symm (circleIntegrable_const 0 c R)

Goal state after:
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₁ : ℝ
⊢ ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)

Tactic:
← ofReal_inj,

Goal state after:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
⊢ ↑(‖circleMap 0 r₁ θ - ρ‖ ^ 2) = ↑(r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg))
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z w : ℂ
⊢ 0 ≤ P.derivRootWeight z w

Tactic:
simp only [derivRootWeight, Pi.single, Function.update_apply]
  split_ifs <;> first | positivity | simp

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

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
hc : DifferentiableOn ℂ g s
⊢ ∀ x ∈ s, ∑' (n : ι), f n x = g x

Tactic:
apply hg.tsum_eqOn

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁹ : TopologicalSpace X₁
X : Type u
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormalSpace X
s : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TietzeExtension Y✝
Y : Type v
inst✝⁴ : TopologicalSpace Y
inst✝³ : Nonempty Y
inst✝² : Subsingleton Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
x✝¹ : Set X✝
x✝ : IsClosed[inst✝¹] x✝¹
f : C(↑x✝¹, Y)
y : Y
⊢ ContinuousMap.restrict x✝¹ (ContinuousMap.const X✝ y) = f

Tactic:
ext; subsingleton

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Nonempty n
h : Function.Surjective ⇑toPGL
r : Rˣ
A : GL n R
hA : GeneralLinearGroup.det A = r
X : SpecialLinearGroup n R
hX : toPGL ↑X = mk A
u : Rˣ
hu : toGL X * (GeneralLinearGroup.scalar n) u = A
⊢ u ^ Fintype.card n = r

Tactic:
simpa [hA] using congr(Matrix.GeneralLinearGroup.det $hu)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Nonempty n
⊢ Function.Surjective ⇑toPGL ↔ ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r

Tactic:
refine ⟨fun h r ↦ ?_, ProjectiveSpecialLinearGroup.toPGL_surj_of_roots⟩
  obtain ⟨A, hA⟩ := GeneralLinearGroup.det_surjective (n := n) r
  obtain ⟨X, hX⟩ := h (.mk A)
  induction X using QuotientGroup.induction_on with | H X =>
  obtain ⟨u, hu⟩ : ∃ u, toGL X * (GeneralLinearGroup.scalar n) u = A := by
    simpa [mk_eq_mk_iff] using hX
  exact ⟨u, by simpa [hA] using congr(Matrix.GeneralLinearGroup.det $hu)⟩

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 ≠ 0
⊢ (↑g).det < 0

Tactic:
simp [Matrix.det_fin_two, *]

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

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
⊢ -g • z = g • z

Tactic:
by
  rw [sl_moeb, ← z.neg_smul]
  congr 1 with i j
  simp [toGL]

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

Goal state before:
pp: s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ volume s = ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2)

Tactic:
volume_def,

Goal state after:
s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ ((Measure.comap UpperHalfPlane.coe volume).withDensity fun z ↦ ↑((1 / NNReal.mk z.im ⋯) ^ 2)) s =
    ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0

Tactic:
mdifferentiable_iff

Goal state after:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 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:
rw [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.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist z w = dist w z

Tactic:
by
  simp only [dist_eq, dist_comm (z : ℂ), mul_comm]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝[≠] c) (𝓝 0) ∧ ∀ᶠ (n : P) in 𝓝[≠] c, dist c n ∈ Ioi 0

Tactic:
refine ⟨tendsto_nhdsWithin_of_tendsto_nhds ?_, eventually_nhdsWithin_of_forall ?_⟩

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝 c) (𝓝 0)

case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ ∀ x ∈ {c}ᶜ, dist c x ∈ Ioi 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
⊢ z.center 0 = z

Tactic:
by
  apply ext_re_im <;> simp

Goal state after: