mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed ↑(↑f ∘ₗ ↑hf.leftInverse - LinearMap.id).ker

Tactic:
exact ((f.comp hf.leftInverse) - (ContinuousLinearMap.id R F)).isClosed_ker

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ Commute P Q

Tactic:
change P * Q = Q * P

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ P * Q = Q * P
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Tactic:
filter_upwards [h, hu.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi hi' x hx
    using (norm_log_one_add_half_le_self <| (hi x hx).trans hi').trans (by simpa using hi x hx)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : NormedField 𝕜
p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))
⊢ projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q

Tactic:
simp [projectiveSeminormAux]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ ⨅ p, projectiveSeminormAux ↑p ≤ ⨅ i, ‖a‖ * projectiveSeminormAux ↑i

Tactic:
refine le_ciInf fun p ↦ ?_

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
p : ↑x.lifts
⊢ ⨅ p, projectiveSeminormAux ↑p ≤ ‖a‖ * projectiveSeminormAux ↑p
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
hle : ⨅ p, projectiveSeminormAux ↑p ≤ projectiveSeminormAux ↑⟨FreeAddMonoid.of (1, m), ⋯⟩
⊢ projectiveSeminormAux ↑⟨FreeAddMonoid.of (1, m), ⋯⟩ ≤ ∏ i, ‖m i‖

Tactic:
simp [projectiveSeminormAux]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
e : ↥(lp E p)
f : ↥(lp F q)
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
obtain ⟨(rfl | hp), (rfl | hq)⟩ := And.intro p.dichotomy q.dichotomy
    · obtain rfl : r = ⊤ := ENNReal.HolderTriple.unique ∞ ∞ r ∞
      refine norm_le_of_forall_le (by positivity) fun i ↦ ?_
      refine (B i).le_of_opNorm₂_le_of_le (hBK i) ?_ ?_
      all_goals exact norm_apply_le_norm (by simp) ..
    · obtain rfl : r = q := ENNReal.HolderTriple.unique ∞ q r q
      refine norm_le_of_forall_sum_le (zero_lt_one.trans_le hq) (by positivity) fun s ↦ ?_
      rw [Real.mul_rpow (by positivity) (by positivity)]
      refine Memℓp.holder_top_left_bound B hBK
        (by positivity) (by positivity) (norm_apply_le_norm (by simp) _) ?_ s
      exact sum_rpow_le_norm_rpow (zero_lt_one.trans_le hq) f
    · obtain rfl : r = p := ENNReal.HolderTriple.unique p ∞ r p
      refine norm_le_of_forall_sum_le (zero_lt_one.trans_le hp) (by positivity) fun s ↦ ?_
      rw [mul_right_comm, Real.mul_rpow (by positivity) (by positivity)]
      refine Memℓp.holder_top_right_bound B hBK
        (by positivity) (by positivity) ?_ (norm_apply_le_norm (by simp) _) s
      exact sum_rpow_le_norm_rpow (zero_lt_one.trans_le hp) e
    · have hpqr := hpqr.toReal r (zero_lt_one.trans_le hp) (zero_lt_one.trans_le hq)
      have hp := hpqr.pos
      have hq := hpqr.symm.pos
      refine norm_le_of_forall_sum_le hpqr.pos' (by positivity) fun s ↦ ?_
      simp only [holderₗ_apply_apply_coe]
      calc
        _ ≤ K ^ r.toReal * (‖e‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
          (‖f‖ ^ q.toReal) ^ (r.toReal / q.toReal) :=
          Memℓp.holder_gen_bound r hp hq B hBK (by positivity) (by positivity)
            (sum_rpow_le_norm_rpow hp e) (sum_rpow_le_norm_rpow hq f) s
        _ ≤ _ := by
          rw [← Real.rpow_mul, ← Real.rpow_mul]
          · simp only [← mul_div_assoc, ne_eq, hp.ne', not_false_eq_true, mul_div_cancel_left₀,
            hq.ne', fieldLe]
            rw [Real.mul_rpow, Real.mul_rpow]
            all_goals positivity
          all_goals positivity

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
this : dist x y ≤ dist x (f x) + dist y (f y) + ↑K * dist x y
⊢ (1 - ↑K) * dist x y ≤ dist x (f x) + dist y (f y)

Tactic:
_root_.sub_mul,

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
this : dist x y ≤ dist x (f x) + dist y (f y) + ↑K * dist x y
⊢ 1 * dist x y - ↑K * dist x y ≤ dist x (f x) + dist y (f y)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
⊢ 1 ≤ p.cauchyBound

Tactic:
by
  simp [cauchyBound]

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
⊢ cauchyBound 0 = 1

Tactic:
by
  simp [cauchyBound]

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
x : K
⊢ (C x).cauchyBound = 1

Tactic:
by
  simp [cauchyBound]

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
⊢ X.cauchyBound = 1

Tactic:
by
  simp [cauchyBound]

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
x : K
⊢ (X + C x).cauchyBound = ‖x‖₊ + 1

Tactic:
by
  simp [cauchyBound]

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
x : K
⊢ (X - C x).cauchyBound = ‖x‖₊ + 1

Tactic:
by
  simp [cauchyBound]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this
      exact this.symm

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
⊢ (fun x ↦ x ^ P.natDegree) =O[cobounded R] fun x ↦ x ^ Q.natDegree

Tactic:
exact isBigO_pow_pow_cobounded_of_le (natDegree_le_natDegree h)

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmax)

Tactic:
by_cases hlt : tmin < tmax
  · set t₀ := (tmin + tmax) / 2 with h
    have ht₀ : t₀ ∈ Icc tmin tmax := ⟨by linarith, by linarith⟩
    have : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t := by
      intro t ht
      have : uIcc t₀ t ⊆ Icc tmin tmax := uIcc_subset_Icc ht₀ ht
      rw [picard_eq_of_hasDerivAt (hf.continuousOn.mono (prod_subset_prod_left this))
        (fun t' ht' ↦ hα t' (this ht') |>.mono this) (hmem.mono_left this)]
    exact contDiffOn_enat_picard_Icc ht₀ hf (HasDerivWithinAt.continuousOn hα) hmem (α t₀) this
      |>.congr this
  · rw [not_lt, le_iff_lt_or_eq] at hlt
    cases hlt with
    | inl h =>
      intro _ ht
      rw [Icc_eq_empty (not_le.mpr h)] at ht
      exfalso
      exact notMem_empty _ ht
    | inr h =>
      rw [h, Icc_self]
      intro _ ht
      rw [eq_of_mem_singleton ht]
      exact contDiffWithinAt_singleton

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
⊢ ((fun x ↦ Inv.inv ∘ x) fun x ↦ 0) =ᶠ[↑φ] fun x ↦ 0

Tactic:
simp only [Function.comp_def, inv_zero, EventuallyEq.rfl]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inl
q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
irrational_sqrt_ratCast_iff_of_nonneg hq,

Goal state after:
case inl
q : ℚ
hq : 0 ≤ q
⊢ ¬IsSquare q ↔ ¬IsSquare q ∧ 0 ≤ q
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → y < x → sqrt (x * y) < (x + y) / 2
hl : ¬y < x
⊢ sqrt (x * y) < (x + y) / 2

pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
· specialize this h.symm (h.gt_or_lt.resolve_left hl)
    rwa [mul_comm, add_comm]

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < 1 - p
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
have : 0 < log p⁻¹ := log_pos <| (one_lt_inv₀ hp₀).2 hp₁

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝ : 0 < 1 - p
this : 0 < log p⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

Tactic:
apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoBot) nhdsWithin_le_nhds

Goal state after:
q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 1)) atBot

q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ (fun p ↦ log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: q : ℚ
⊢ ∃ a b, 0 < b ∧ ↑q = ↑a / ↑b

Tactic:
exact ⟨q.num, q.den, q.pos, by exact_mod_cast (Rat.num_div_den _).symm⟩

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
⊢ False

Tactic:
have hn' : 0 < a ^ (2 * n + 1) / n ! * I n (π / 2) := mul_pos (k _) I_pos

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → ℝ → ℝ := fun p x ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

Tactic:
exact hmain (spectrum ℝ a) (by grind) (by grind)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
⊢ (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z

Tactic:
← cfc_smul_id (R := ℝ) (S := ℝ) b z,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
⊢ (a • 1 + cfc (fun x ↦ b • x) z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
hcont : ContinuousOn (fun r ↦ r ^ (-1)) (spectrum ℝ z)
⊢ cfc (fun x ↦ a + b • x ^ (-1)) z = cfc (fun r ↦ a + b * r ^ (-1)) z

Tactic:
refine cfc_congr fun r hr => ?_

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
hcont : ContinuousOn (fun r ↦ r ^ (-1)) (spectrum ℝ z)
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ a + b • r ^ (-1) = a + b * r ^ (-1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : 0 < p ∧ p < 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
simp [hx_zero, Real.zero_rpow (by linarith : p - 1 ≠ 0)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
⊢ z ∈ quasispectrum ℝ a → ‖f t z‖ ≤ bound t

Tactic:
hz

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
⊢ ‖f t z‖ ≤ bound t
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
⊢ z ∈ quasispectrum ℝ a → ‖f t z‖ ≤ bound t

Tactic:
hz

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
⊢ ‖f t z‖ ≤ bound t
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + ↑(Real.log (2 ^ 2 * π))) / ↑2 = -(↑γ + log (4 * ↑π)) / ↑2

Tactic:
ofReal_ofNat,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + ↑(Real.log (2 ^ 2 * π))) / 2 = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ -1 ≤ mulExpNegMulSq 1 x

Tactic:
by
  rw [← neg_mulExpNegMulSq_neg, neg_le_neg_iff]
  exact mulExpNegMulSq_one_le_one (-x)

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

Goal state before:
pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
rw [← Nat.cast_inj (R := ℤ), Int.natCast_ceil_eq_ceil, ceil_logb_natCast (by simp),
    Int.clog_natCast]

Goal state after:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)

Tactic:
exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
⊢ Tendsto (fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) (𝓝[>] 0) (𝓝 (∫ (x : E), g x ∂P))

Tactic:
by
  apply tendsto_of_seq_tendsto
  intro u hu
  obtain ⟨N, hupos⟩ := eventually_atTop.mp (tendsto_nhdsWithin_iff.mp hu).2
  apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
  · exact Eventually.of_forall (fun n => g.continuous.mulExpNegMulSq.aestronglyMeasurable)
  · use norm g
    rw [eventually_atTop]
    use N
    intro n hn
    exact Eventually.of_forall
      (fun _ => abs_mulExpNegMulSq_comp_le_norm g (le_of_lt (Set.mem_Ioi.mp (hupos n hn))))
  · exact Eventually.of_forall (fun _ => (tendsto_nhdsWithin_of_tendsto_nhds
        tendsto_mulExpNegMulSq).comp hu)

Goal state after: