mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C(↑I, A)) → γ 0 = a₀ → C(↑I, E)
Γ_0 : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), (Γ γ a) 0 = e₀
F : A → E := fun a ↦ (Γ (somePath a₀ a).toContinuousMap ⋯) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph ↑p
he : ↑p e₀ = f a₀
uniq :
  ∀ (γ γ' : C(↑I, A)) (Γ Γ' : C(↑I, E)),
    γ 0 = a₀ →
      γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → ↑p ∘ ⇑Γ = ⇑(f.comp γ) → ↑p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1
Γ_lifts : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), ↑p ∘ ⇑(Γ γ a) = ⇑(f.comp γ)
this : ∀ (a : A), ↑p (F a) = f a
hfap : f a ∈ p.target
U : Set A
haU : U ∈ 𝓝 a
U_conn : IsPathConnected U
hUp : id U ⊆ ⇑f ⁻¹' p.target
x : A
hxU : x ∈ U
γ : Path a x
hγ : ∀ (t : ↑I), γ t ∈ U
Γ' : Path e₀ ((↑p.symm ∘ ⇑f) a) :=
  { toContinuousMap := Γ (somePath a₀ a).toContinuousMap ⋯, source' := ⋯, target' := ⋯ }
t : ↑I
⊢ f (γ t) ∈ p.target

Tactic:
exact hUp (hγ _)

Goal state after:
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 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ meromorphicTrailingCoeffAt f x = (∏ᶠ (u : 𝕜), (x - u) ^ update D x 0 u) • g x

Tactic:
by
  have t₀ : MeromorphicAt (∏ᶠ u, (· - u) ^ D u) x :=
    (FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x
  rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (by fun_prop) h₁x h₂x h),
    t₀.meromorphicTrailingCoeffAt_smul h₁g.meromorphicAt,
    h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g]
  simp [meromorphicTrailingCoeffAt_factorizedRational hD]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case zero
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
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t 0)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t 0)) ∧ Γ 0 = e

Tactic:
refine ⟨fun _ ↦ e, continuous_const.continuousOn, fun t ht ↦ ?_, rfl⟩

Goal state after:
case zero
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
t : ↑I
ht : t ∈ Set.Icc 0 (t✝ 0)
⊢ (p ∘ fun x ↦ e) t = γ t
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ rexp 1 < 0.36787944116⁻¹

pp: ⊢ 0 < 0.36787944116

Tactic:
· refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_
    norm_num

Goal state after:
⊢ 0 < 0.36787944116
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

Tactic:
rw [hf', WithTop.top_mul]
    · rw [meromorphicOrderAt_eq_top_iff] at hf' ⊢
      rw [Function.comp_def, ← eventually_map (P := (f · = 0))]
      exact EventuallyEq.filter_mono hf' (hg.map_nhdsNE hg_nc)
    · simp [(show AnalyticAt 𝕜 (g · - g x) x by fun_prop).analyticOrderAt_eq_zero]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩ = id ⟨e₀, he⟩

Tactic:
Path.map_symm,

Goal state after:
case refine_2
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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.symm.map ⋯))) ⟨e₀, he⟩ = id ⟨e₀, he⟩
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 (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)

Tactic:
refine Real.tendsto_exp_atBot.comp ?_

Goal state after:
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 * R) + B * expR (c * R) + Real.log A) atTop atBot
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
f : E → F
x : E
h : HarmonicAt f x
⊢ ∀ᶠ (y : E) in 𝓝 x, HarmonicAt f y

Tactic:
filter_upwards [h.1.eventually (by simp), h.2.eventually_nhds] with a h₁a h₂a
  exact ⟨h₁a, h₂a⟩

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
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
⊢ ‖f (cexp ζ)‖ ≤ C

Tactic:
change ‖(f ∘ exp) ζ‖ ≤ C

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
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
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
Module: Mathlib.Analysis.Complex.MeanValue

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

Tactic:
simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]
    apply circleIntegral.integral_congr hR.le
    intro z hz
    match_scalars
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    grind

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

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ((↑R * cexp (↑θ * I) + ↑r * cexp (↑φ * I)) / (↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I))).re ≤ (R + r) / (R - r)

Tactic:
rw [div_eq_mul_inv]

Goal state after:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ((↑R * cexp (↑θ * I) + ↑r * cexp (↑φ * I)) * (↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I))⁻¹).re ≤ (R + r) / (R - r)
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x ↦ x * log x) (deriv (fun x ↦ x * log x) x) x

Tactic:
hasDerivAt_deriv_iff

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (fun x ↦ x * log x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

Tactic:
rw [hx, 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: ⊢ StrictConvexOn ℝ (Set.Ici 0) fun x ↦ x * log x

Tactic:
by
  refine strictConvexOn_of_deriv2_pos (convex_Ici 0) (continuous_mul_log.continuousOn) ?_
  intro x hx
  simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
  rw [deriv2_mul_log]
  positivity

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

Goal state before:
pp: x : ℝ
⊢ DifferentiableAt ℝ negMulLog x ↔ x ≠ 0

Tactic:
by
  constructor
  · unfold negMulLog
    intro h eq0
    simp only [neg_mul, differentiableAt_fun_neg_iff, eq0] at h
    exact not_DifferentiableAt_log_mul_zero h
  · intro hx
    have : x ∈ ({0} : Set ℝ)ᶜ := by
      simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]
    have := differentiableOn_negMulLog x this
    apply DifferentiableWithinAt.differentiableAt (s := {0}ᶜ) <;>
    simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
      compl_singleton_mem_nhds_iff]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasDerivAt negMulLog (deriv negMulLog x) x

Tactic:
hasDerivAt_deriv_iff

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog 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
⊢ IntegrableOn (fun x ↦ x ^ r) (Ioc 0 c) volume

Tactic:
apply integrableOn_deriv_of_nonneg _ hderiv

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 ∈ Ioo 0 c, 0 ≤ x ^ r

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
⊢ ContinuousOn (fun x ↦ x ^ (r + 1) / (r + 1)) (Icc 0 c)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

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

Tactic:
rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]

Goal state after:
case inl
x : ℝ
hx : x < 0
⊢ sin x * x⁻¹ * -x ≤ 1

case inl
x : ℝ
hx : x < 0
⊢ 0 < -x
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: ⊢ ¬ContinuousAt (fun x ↦ log (log x)) 1

Tactic:
suffices Tendsto (fun x ↦ log (log x)) (nhdsWithin 1 {1}ᶜ) (cobounded ℝ) from
    not_continuousAt_of_tendsto this nhdsWithin_le_nhds (disjoint_nhds_cobounded _)
  exact (tendsto_log_nhdsNE_zero.mono_right atBot_le_cobounded).comp <| log_one ▸
    HasDerivAt.tendsto_nhdsNE (by simpa using hasDerivAt_log one_ne_zero) one_ne_zero

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

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ (fun x ↦ 0) =ᶠ[nhds x] log⁺

Tactic:
filter_upwards [Metric.ball_mem_nhds _ zero_lt_one] with y hy

Goal state after:
x : ℝ
hx : x = 0
y : ℝ
hy : y ∈ Metric.ball x 1
⊢ 0 = log⁺ y
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t_max|) = log⁺ (↑s.card * |f t_max|)

Tactic:
simp [Finset.sum_const]

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

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

Tactic:
(by push_cast; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))

Goal state after:
case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)) / ↑(r + 1)).re
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ ‖g z‖ ≤ ‖f z‖

Tactic:
rw [hgn]

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖ = ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖

Tactic:
have : Function.Periodic (log ‖circleMap 0 1 · - 1‖) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
this : Function.Periodic (fun x ↦ log ‖circleMap 0 1 x - 1‖) (2 * π)
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖ = ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_a
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ Complex.normSq (circleMap 0 1 x - 1) = 4 * sin (x / 2) ^ 2

Tactic:
calc Complex.normSq (circleMap 0 1 x - 1)
    _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
      simp [circleMap, Complex.normSq_apply]
    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
      ring
    _ = 2 - 2 * cos x := by
      rw [sin_sq_add_cos_sq]
      norm_num
    _ = 2 - 2 * cos (2 * (x / 2)) := by
      rw [← mul_div_assoc]
      simp
    _ = 4 - 4 * cos (x / 2) ^ 2 := by
      rw [cos_two_mul]
      ring
    _ = 4 * sin (x / 2) ^ 2 := by
      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (fun x ↦ expR x.re ^ n * ‖f x‖) =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR ((↑n + max B 0) * ‖z‖ ^ max c 1)

Tactic:
refine ((isBigO_refl (fun z : ℂ => expR z.re ^ n) _).mul hO.norm_left).trans (.of_bound' ?_)

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z | 0 < z.re},
    ‖expR x.re ^ n * expR (B * ‖x‖ ^ c)‖ ≤ ‖expR ((↑n + max B 0) * ‖x‖ ^ max c 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = log R

Tactic:
circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR,

Goal state after:
case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ log R + log⁺ (R⁻¹ * ‖c - a‖) = log R
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (fun x ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (fun x ↦ ‖f x - f z₀‖) (sphere z₀ r) x
⊢ f '' closedBall z₀ r ⊆ f '' closedBall z₀ R

Tactic:
gcongr; exact inf_le_right

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

Goal state before:
pp: case pos
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
⊢ g z = g z₀

Tactic:
let w : E := ‖z - z₀‖⁻¹ • (z - z₀)

Goal state after:
case pos
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₀)
⊢ g z = g z₀
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

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

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

Goal state before:
pp: ⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - sin x ^ 2) * cos x = ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2

Tactic:
refine integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)

Goal state after:
x✝ : ℝ
h : x✝ ∈ Ι (-(π / 2)) (π / 2)
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2
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
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
· refine fun x ↦ Subtype.ext ?_
    have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)
    simp [field, abs_div, abs_of_pos this]

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

Goal state before:
pp: a : ℂ
⊢ a.sqrt = ↑√((‖a‖ + a.re) / 2) + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

Tactic:
by
  rw [← cpow_inv_two_re, sqrt]
  by_cases! h : 0 ≤ a.im
  · simp [← cpow_inv_two_im_eq_sqrt h, h]
  simp only [re_add_im, ↓reduceIte, h.not_ge, neg_one_mul, ← ofReal_neg,
    ← cpow_inv_two_im_eq_neg_sqrt h]

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

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑(-↑α).sqrt.re + ↑(-↑α).sqrt.im * I = I * ↑√α

Tactic:
simp [sqrt, cpow_inv_two_im_eq_sqrt, abs_of_nonneg hα, cpow_inv_two_re, mul_comm]

Goal state after: