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

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt 𝕜 (fun x ↦ 0) x
⊢ AnalyticAt 𝕜 f x

Tactic:
apply this.congr

Goal state after:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt 𝕜 (fun x ↦ 0) x
⊢ (fun x ↦ 0) =ᶠ[𝓝 x] f
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = ⊤

Tactic:
simp [he, meromorphicOrderAt_eq_top_iff]

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

Goal state before:
pp: case pos.inl
R : ℝ
z : ℂ
hz hw : z ∈ ball 0 R
⊢ (meromorphicOrderAt (canonicalFactor R z) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single z 1) ⋯) z

pp: case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
· rw [meromorphicOrderAt_canonicalFactor hz]
      simp_all [Function.locallyFinsuppWithin.restrict_apply]

Goal state after:
case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case right.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z

Tactic:
filter_upwards [h₃g]
    intro y hy
    rw [Pi.pow_apply, hy, Algebra.smul_def, Algebra.smul_def, mul_zpow, ← map_zpow₀]
    congr 1
    rw [mul_comm, zpow_mul]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ meromorphicOrderAt (f / g) x = meromorphicOrderAt f x - meromorphicOrderAt g x

Tactic:
div_eq_mul_inv,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ meromorphicOrderAt (f * g⁻¹) x = meromorphicOrderAt f x - meromorphicOrderAt g x
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
⊢ Subgroup.center (GL n R) = (scalar n).range

Tactic:
by
  ext g
  constructor
  · -- previous lemma shows the underlying matrix is scalar, but now need to show
    -- the scalar is a unit; so we apply argument both to `g` and `g⁻¹`
    intro hg
    cases isEmpty_or_nonempty n with
    | inl hn => simp [nontriviality]
    | inr hn =>
      obtain ⟨a, ha⟩ := mem_center_iff_val_mem_range_scalar.mp hg
      obtain ⟨b, hb⟩ := mem_center_iff_val_mem_range_scalar.mp (Subgroup.inv_mem _ hg)
      have hab : a * b = 1 := by
        simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g
      refine ⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩
      simp [Units.ext_iff, ← ha]
  · rintro ⟨a, rfl⟩
    exact mem_center_iff_val_mem_range_scalar.mpr ⟨a, rfl⟩

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

Goal state before:
pp: a b : Circle
⊢ (rotation a).trans (rotation b) = rotation (b * a)

Tactic:
by
  ext1
  simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
⊢ ℓ (a • b) = a • ℓ b

Tactic:
rw [← re_add_im a, ← re_add_im b, ← smul_eq_mul _ I, ← smul_eq_mul _ I]
  have t₀ : ((a.im : ℂ) • I) • (b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I := by
    simp only [smul_eq_mul, ofReal_mul, ← mul_assoc, mul_comm _ I]
  have t₁ : ((a.im : ℂ) • I) • (b.im : ℂ) • I = (↑(- a.im * b.im) : ℂ) • (1 : ℂ) := by
    simp [mul_mul_mul_comm _ I]
  simp only [add_smul, smul_add, ℓ.map_add, t₀, t₁]
  repeat rw [Complex.coe_smul, ℓ.map_smul]
  have t₂ {r : ℝ} : ℓ (r : ℂ) = r • ℓ (1 : ℂ) := by simp [← ℓ.map_smul]
  simp only [t₂, h]
  match_scalars
  simp [mul_mul_mul_comm _ I]
  ring

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt f w =
    ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
        (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f B₀R) u)) * ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f S₀R) v) •
          h)
        w

Tactic:
rw [meromorphicTrailingCoeffAt_congr_nhdsNE
        ((D.meromorphicOn w hw).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
        (by fun_prop) hw ?η₁ D.eventuallyEq)]
      case η₁ =>
        rw [← closure_ball _ hR.ne']
        exact isOpen_ball.perfect_closure.2

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

Goal state before:
pp: ⊢ |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)

Tactic:
iterate 21 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Goal state after:
⊢ |rexp 1 -
        expNear 21 1
          ((((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                    7 -
                                                                  1) *
                                                                8 -
                                                              1) *
                                                            9 -
                                                          1) *
                                                        10 -
                                                      1) *
                                                    11 -
                                                  1) *
                                                12 -
                                              1) *
                                            13 -
                                          1) *
                                        14 -
                                      1) *
                                    15 -
                                  1) *
                                16 -
                              1) *
                            17 -
                          1) *
                        18 -
                      1) *
                    19 -
                  1) *
                20 -
              1) *
            21)| ≤
    |1| ^ 21 / ↑(Nat.factorial 21) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20 * 21)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ Tendsto (fun x ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))

Tactic:
apply Tendsto.mul
        · apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 0)]
            exact Tendsto.add_const (sSupNormIm f 0) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [sub_nonneg, le_of_lt hz.2]
        · apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 1)]
            exact Tendsto.add_const (sSupNormIm f 1) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [le_of_lt hz.1]

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
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
⊢ Tendsto (fun R ↦ (expR ((d - c) * R))⁻¹) atTop (𝓝 0)

Tactic:
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.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] 0

Tactic:
· filter_upwards [h₁.1.laplacian_add_nhds h₂.1, h₁.2, h₂.2]
    simp_all

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ (Δ[s] f) e = iteratedDerivWithin 2 f s e

Tactic:
by
  simp only [laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he
        (OrthonormalBasis.singleton (Fin 1) ℝ),
    Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, OrthonormalBasis.singleton_apply,
    Finset.sum_const, Finset.card_singleton, one_smul, iteratedDerivWithin_eq_iteratedFDerivWithin]
  congr with i
  fin_cases i <;> simp

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x ↔ HarmonicAt f x

Tactic:
by
  constructor <;> intro h
  · simpa [Function.comp_def] using h.comp_CLM l.symm.toContinuousLinearMap
  · exact h.comp_CLM l.toContinuousLinearMap

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
this : ‖f (z * I * -I)‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
by simpa [mul_assoc] using this

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

Goal state before:
pp: case inl
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f (closedBall x 0)

Tactic:
rw [closedBall_zero]
    exact continuousOn_singleton f x

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 : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ circleAverage (⇑g ∘ f) c R = g (f c)

Tactic:
← circleAverage_congr_sphere h₄F,

Goal state after:
F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ circleAverage (⇑Complex.reCLM ∘ F) c R = g (f c)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w : ℂ
⊢ herglotzRieszKernel c w = fun z ↦ (z - c + (w - c)) / (z - c - (w - c))

Tactic:
by
  ext z
  exact herglotzRieszKernel_def c w z

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

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x ↦ x * log x) 0 = 0⁻¹

Tactic:
inv_zero

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x ↦ x * log x) 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ deriv negMulLog x = -log x - 1

Tactic:
by
  rw [negMulLog_eq_neg, deriv.fun_neg, deriv_mul_log hx]
  ring

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

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

Tactic:
div_eq_mul_inv,

Goal state after:
case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x * x⁻¹ ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case hab.hpos
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : min 0 1 < s
hs₂ : s < max 0 1
⊢ 0 ≤ (-log) s

Tactic:
grind [Pi.neg_apply, log_nonpos_iff]

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‖ * R / ‖circleMap 0 R θ - x‖ ^ 2 * ‖f (circleMap 0 R θ)‖ ≤ 2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖

Tactic:
div_eq_mul_inv,

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.LogTrigonometric

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..π, log (sin x) = -log 2 * π

Tactic:
rw [integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two,
    integral_log_sin_zero_pi_div_two]
  ring

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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖1 - x⁻¹ * a‖) 0 1 = 0

Tactic:
by
    rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      InnerProductSpace.HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
    intro x hx
    have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
    apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
    rw [sub_ne_zero]
    by_contra! hCon
    rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this

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

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
⊢ ball (f z₀) (ε / 2) ⊆ f '' closedBall z₀ r

Tactic:
rintro v hv

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
⊢ v ∈ f '' closedBall z₀ r
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = ↑c + ↑c₀ * I

Tactic:
by
  obtain ⟨cc, hcc⟩ := AnalyticOnNhd.eq_const_of_im_eq_const h₁f h₂f h₁U h₂U
  use cc.re
  simp_rw [Complex.ext_iff]
  aesop

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

Goal state before:
pp: case hF_meas
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (fun x ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) (volume.restrict (uIoc 0 (2 * π)))

Tactic:
filter_upwards [hr_tendsto.eventually (lt_mem_nhds hw)] with n hn
    exact continuous_herglotzLogIntegrand_circle hρ (hr_lt n) hn |>.aestronglyMeasurable

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

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

Tactic:
by
  field_simp
  convert! eq_sub_iff_add_eq.mp (integral_cos_pow_aux n) using 1
  ring

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

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

Tactic:
by
  have := @integral_sin_pow_odd_mul_cos_pow a b 0 2
  norm_num at this; exact this

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

Goal state before:
pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : ↑(Ioo (-1) 1)
⊢ ↑(codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯ ((fun x ↦ ↑x / (1 - |↑x|)) x)) = ↑x

Tactic:
have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)

Goal state after:
case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : ↑(Ioo (-1) 1)
this : 0 < 1 - |↑x|
⊢ ↑(codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯ ((fun x ↦ ↑x / (1 - |↑x|)) x)) = ↑x
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑r ≠ 0

Tactic:
exact_mod_cast hr.ne'

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 : ProjectiveSpecialLinearGroup n R
hX : toPGL X = mk A
⊢ ∃ k, k ^ Fintype.card n = r

Tactic:
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: case pos
g : GL (Fin 2) ℝ
h : (↑g).det < 0
hadd : (↑g).trace = 0
hc : ↑g 1 0 = 0
⊢ ∃ z, g • z = z

Tactic:
use ⟨⟨g 0 1 / (2 * g 1 1), 1⟩, one_pos⟩

Goal state after:
case h
g : GL (Fin 2) ℝ
h : (↑g).det < 0
hadd : (↑g).trace = 0
hc : ↑g 1 0 = 0
⊢ g • { coe := { re := ↑g 0 1 / (2 * ↑g 1 1), im := 1 }, coe_im_pos := ⋯ } =
    { coe := { re := ↑g 0 1 / (2 * ↑g 1 1), im := 1 }, coe_im_pos := ⋯ }
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) ^ 2

Tactic:
← Complex.ofReal_pow,

Goal state after:
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) ^ 2)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
⊢ (-m).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simp [IsHyperbolic, discr_fin_two, det_neg]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z)
    else -↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z)) =
    |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

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

Tactic:
simp [dg0 (Or.inr hc), hxl]

Goal state after: