mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ I (n + 1) θ * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
by
  rw [I]
  let f (x : ℝ) : ℝ := 1 - x ^ 2
  let u₁ (x : ℝ) : ℝ := f x ^ (n + 1)
  let u₁' (x : ℝ) : ℝ := - (2 * (n + 1) * x * f x ^ n)
  let v₁ (x : ℝ) : ℝ := sin (x * θ)
  let v₁' (x : ℝ) : ℝ := cos (x * θ) * θ
  let u₂ (x : ℝ) : ℝ := x * (f x) ^ n
  let u₂' (x : ℝ) : ℝ := (f x) ^ n - 2 * n * x ^ 2 * (f x) ^ (n - 1)
  let v₂ (x : ℝ) : ℝ := cos (x * θ)
  let v₂' (x : ℝ) : ℝ := -sin (x * θ) * θ
  have hfd : Continuous f := by fun_prop
  have hu₁d : Continuous u₁' := by fun_prop
  have hv₁d : Continuous v₁' := by fun_prop
  have hu₂d : Continuous u₂' := by fun_prop
  have hv₂d : Continuous v₂' := by fun_prop
  have hu₁_eval_one : u₁ 1 = 0 := by simp only [u₁, f]; simp
  have hu₁_eval_neg_one : u₁ (-1) = 0 := by simp only [u₁, f]; simp
  have t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ) := by simp [u₂, v₂, f, ← two_mul]
  have hf (x) : HasDerivAt f (- 2 * x) x := by
    convert! (hasDerivAt_pow 2 x).const_sub 1 using 1
    simp
  have hu₁ (x) : HasDerivAt u₁ (u₁' x) x := by
    convert! (hf x).pow _ using 1
    simp only [Nat.add_succ_sub_one, u₁', Nat.cast_add_one]
    ring
  have hv₁ (x) : HasDerivAt v₁ (v₁' x) x := (hasDerivAt_mul_const θ).sin
  have hu₂ (x) : HasDerivAt u₂ (u₂' x) x := by
    convert! (hasDerivAt_id' x).fun_mul ((hf x).fun_pow _) using 1
    simp only [u₂']
    ring
  have hv₂ (x) : HasDerivAt v₂ (v₂' x) x := (hasDerivAt_mul_const θ).cos
  convert_to (∫ (x : ℝ) in (-1)..1, u₁ x * v₁' x) * θ = _ using 1
  · simp_rw [u₁, v₁', f, ← intervalIntegral.integral_mul_const, sq θ, mul_assoc]
  rw [integral_mul_deriv_eq_deriv_mul (fun x _ => hu₁ x) (fun x _ => hv₁ x)
    (hu₁d.intervalIntegrable _ _) (hv₁d.intervalIntegrable _ _), hu₁_eval_one, hu₁_eval_neg_one,
    zero_mul, zero_mul, sub_zero, zero_sub, ← integral_neg, ← integral_mul_const]
  convert_to ((-2 : ℝ) * (n + 1)) * ∫ (x : ℝ) in (-1)..1, (u₂ x * v₂' x) = _ using 1
  · rw [← integral_const_mul]
    congr 1 with x
    dsimp [u₁', v₁, u₂, v₂']
    ring
  rw [integral_mul_deriv_eq_deriv_mul (fun x _ => hu₂ x) (fun x _ => hv₂ x)
    (hu₂d.intervalIntegrable _ _) (hv₂d.intervalIntegrable _ _),
    mul_sub, t, neg_mul, neg_mul, neg_mul, sub_neg_eq_add]
  have (x : _) : u₂' x = (2 * n + 1) * f x ^ n - 2 * n * f x ^ (n - 1) := by
    cases n with
    | zero => simp [u₂']
    | succ n => ring!
  simp_rw [this, sub_mul, mul_assoc _ _ (v₂ _)]
  have : Continuous v₂ := by fun_prop
  rw [mul_mul_mul_comm, integral_sub, mul_sub, add_sub_assoc]
  · congr 1
    simp_rw [integral_const_mul]
    ring!
  all_goals exact Continuous.intervalIntegrable (by fun_prop) _ _

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

Goal state before:
pp: case x
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ p ∈ Ioi 0

pp: case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ (↑q - 1) * (1 - p) < p

Tactic:
· simp_all only [mem_Ioi]
        linarith

Goal state after:
case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ (↑q - 1) * (1 - p) < p
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
simp only [hp, nnrpow_zero]

Goal state after:
case inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
⊢ Monotone fun a ↦ a ^ ↑q

Tactic:
hq

Goal state after:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
⊢ Monotone fun a ↦ a ^ ↑0
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: s : Set ℝ
⊢ s ⊆ Ioi 0 → IsCompact s → TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) s

Tactic:
hs

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
⊢ IsCompact s → TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) s
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (fun x_1 ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)

Tactic:
exact .of_forall fun p ↦ by fun_prop (disch := grind -abstractProof)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
u : ℝ → E := fun x ↦ x⁻¹ • f x
⊢ (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x)

Tactic:
funext x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
u : ℝ → E := fun x ↦ x⁻¹ • f x
x : ℝ
⊢ x⁻¹ • f (c * x) = c • u (c * x)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
this : log (b / a) • V = ∫ (x : ℝ) in a..b, x⁻¹ • V
⊢ (fun x ↦ x⁻¹ • f x - x⁻¹ • V) = fun x ↦ x⁻¹ • (f x - V)

Tactic:
funext x

Goal state after:
case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
this : log (b / a) • V = ∫ (x : ℝ) in a..b, x⁻¹ • V
x : ℝ
⊢ x⁻¹ • f x - x⁻¹ • V = x⁻¹ • (f x - V)
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 • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
have h₁ : (a • 1 + b • z) ^ (-1 : ℝ) = cfc (fun r => (a + b * r) ^ (-1 : ℝ)) z := by
    rw [← cfc_smul_id (R := ℝ) (S := ℝ) b z, ← Algebra.algebraMap_eq_smul_one,
        ← cfc_const_add a (fun r => b • r) z]
    simp only [smul_eq_mul]
    refine cfc_rpow fun r hr => ?_
    by_cases ha' : a = 0
    · have hb' : b = 1 := by grind
      simp only [ha', hb', one_mul, zero_add, gt_iff_lt]
      #adaptation_note /-- Before nightly-2026-06-04, this was just `grind.
      `spectrum_pos` is not activating in `grind` despite the
      ```
      grind_pattern IsStrictlyPositive.spectrum_pos => x ∈ spectrum 𝕜 a, IsStrictlyPositive a
      ```
      rule, because `grind` will not fill in the `𝕜 := ℝ`. -/
      exact zpos.spectrum_pos hr
    · grind [add_pos_of_pos_of_nonneg, mul_nonneg]

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
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
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
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (conjSqrt x⁻¹ʳ) (a • 1 + b • z)⁻¹ʳ = (conjSqrt x⁻¹ʳ) ((a • 1 + b • z) ^ (-1))

Tactic:
← inverse_eq_rpow_neg_one

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
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (conjSqrt x⁻¹ʳ) (a • 1 + b • z)⁻¹ʳ = (conjSqrt x⁻¹ʳ) (a • 1 + b • 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
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (conjSqrt x⁻¹ʳ) (a • 1 + b • z ^ (-1)) = (conjSqrt x⁻¹ʳ) (a • 1 + b • z⁻¹ʳ)

Tactic:
← inverse_eq_rpow_neg_one

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
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (conjSqrt x⁻¹ʳ) (a • 1 + b • z⁻¹ʳ) = (conjSqrt x⁻¹ʳ) (a • 1 + b • z⁻¹ʳ)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: m n r : ℕ
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
rcases eq_zero_or_pos r with rfl | hr

Goal state after:
case inl
m n : ℕ
⊢ eulerMascheroniSeq 0 < eulerMascheroniSeq' 0

case inr
m n r : ℕ
hr : 0 < r
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
by
    simpa using this.add tendsto_eulerMascheroniSeq

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
calc Gammaℝ s / Gammaℝ (1 - s)
  _ = (Gammaℝ s * Gammaℝ (s + 1)) / (Gammaℝ (1 - s) * Gammaℝ (1 + s)) := by
    rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div,
      mul_div_cancel_right₀ _ this]
  _ = (2 * (2 * π) ^ (-s) * Gamma s) / ((cos (π * s / 2))⁻¹) := by
    rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
  _ = _ := by rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ clog b r⁻¹ = -log b r

Tactic:
by
  rcases lt_or_ge 0 r with hrp | hrp
  · obtain hr | hr := le_total 1 r
    · rw [clog_of_right_le_one _ (inv_le_one_of_one_le₀ hr), log_of_one_le_right _ hr, inv_inv]
    · rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]
  · rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]

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

Goal state before:
pp: case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊logb (↑b) 0⌋ = Int.log b 0

Tactic:
rw [logb_zero, Int.log_zero_right, Int.floor_zero]

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

Goal state before:
pp: k n : ℕ
⊢ (if ↑k ∈ Set.Ici (↑n - 1) then ↑(k.descFactorial n) else 0 ↑k) = ↑(k.descFactorial n)

Tactic:
ite_eq_left_iff,

Goal state after:
k n : ℕ
⊢ ↑k ∉ Set.Ici (↑n - 1) → 0 ↑k = ↑(k.descFactorial n)
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr.h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_1

pp: case inr.h'
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) L fun i ↦ ∫ (x : X), f x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_3

Tactic:
· exact bdd_above

Goal state after:
case inr.h'
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) L fun i ↦ ∫ (x : X), f x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_3
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 (0 ^ (b.card + 1 - a.card)))
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)

Tactic:
rw [zero_pow (by grind)] at this

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ * ordinaryHypergeometricCoefficient a b c n =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))

Tactic:
ordinaryHypergeometricCoefficient,

Goal state after:
a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ *
      ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) *
        (Polynomial.eval c (ascPochhammer ℂ n))⁻¹) =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ ℘[L - l₀] (x + ↑l)) (↑L.lattice \ {l₀ - ↑l})ᶜ

Tactic:
refine (L.differentiableOn_weierstrassPExcept l₀).comp (f := (· + l.1)) (by fun_prop) ?_

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.MapsTo (fun x ↦ x + ↑l) (↑L.lattice \ {l₀ - ↑l})ᶜ (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
· refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
      exact Nat.isClosedEmbedding_coe_real.isClosed_range.measurableSet

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sin ((↑n + 1) * θ * I) * -I = sinh ((↑n + 1) * θ)

Tactic:
rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]

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

Goal state before:
pp: ⊢ deriv arcsin = fun x ↦ 1 / √(1 - x ^ 2)

Tactic:
funext x

Goal state after:
x : ℝ
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
    simp only [not_and_or, Ne, Classical.not_not] at h
    rcases h with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : b < a
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a

Tactic:
simp only [uIcc_of_ge hab.le] at h ⊢

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc b a) x = f b - f a
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
have := log_stirlingSeq_bounded_aux n
  rw [stirlingSeq_one, log_div (by positivity), log_exp, log_sqrt] at this <;> grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntervalIntegrable (fun x ↦ f x * √(1 - x ^ 2)⁻¹) volume (-1) 1
⊢ Integrable f measureT

Tactic:
rw [intervalIntegrable_iff, Set.uIoc_of_le (by norm_num)] at this

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f measureT
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: this : √π ≠ 0
⊢ Tendsto ((fun n ↦ ↑n !) / fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 (√π / √π))

Tactic:
convert! tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1

Goal state after:
this : √π ≠ 0
⊢ ((fun n ↦ ↑n !) / fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n) = stirlingSeq / fun x ↦ √π
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
this : cos (π - π / 3) = -cos (π / 3)
⊢ cos (π * (2 / 3)) = -1 / 2

Tactic:
have := cos_pi_div_three

Goal state after:
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
this✝ : cos (π - π / 3) = -cos (π / 3)
this : cos (π / 3) = 1 / 2
⊢ cos (π * (2 / 3)) = -1 / 2
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ (-1) ^ ⌊r⌋ * cos (↑r * π) = (-1) ^ ⌊r⌋ * ↑q

Tactic:
hq

Goal state after:
r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ (-1) ^ ⌊r⌋ * ↑q = (-1) ^ ⌊r⌋ * ↑q
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ ↑n)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : ∃ k, ↑k * π = ↑n * arccos x
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case pos
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
iterate_derivative_eq_zero_of_degree_lt (by grw [hPdeg]; simpa),

Goal state after:
case pos
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ eval x 0 ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_1
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀

Tactic:
have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)

Goal state after:
case refine_1
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
this : eval x (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0
⊢ eval x (U ℝ ↑n) = 0

Tactic:
by
      refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
      field_simp
      norm_cast
      grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x

Tactic:
← neg_le_neg_iff,

Goal state after:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ -∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ -∑ i ∈ Finset.range a, f (x₀ + ↑i)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x

Tactic:
← neg_le_neg_iff,

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ -∫ (x : ℝ) in ↑a..↑b, f x ≤ -∑ x ∈ Finset.Ico a b, f ↑x