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

Goal state before:
pp: case e_a.e_f
b : ℕ
a : ℕ → Fin b
n i : ℕ
⊢ ofDigitsTerm a (i + n) = (↑b ^ n)⁻¹ * ofDigitsTerm (fun i ↦ a (i + n)) i

Tactic:
simp only [ofDigitsTerm]

Goal state after:
case e_a.e_f
b : ℕ
a : ℕ → Fin b
n i : ℕ
⊢ ↑↑(a (i + n)) * (↑b ^ (i + n + 1))⁻¹ = (↑b ^ n)⁻¹ * (↑↑(a (i + n)) * (↑b ^ (i + 1))⁻¹)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊

Tactic:
by
  have := NeZero.ne b
  induction n with
  | zero => simp [Nat.floor_eq_zero.mpr hx.right]
  | succ n ih =>
    rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
    set y := (b : ℝ) ^ n * x
    norm_cast
    rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case refine_1
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ ∀ (i : ℕ), Continuous fun x ↦ ofDigitsTerm x i

Tactic:
simp only [ofDigitsTerm]

Goal state after:
case refine_1
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ ∀ (i : ℕ), Continuous fun x ↦ ↑↑(x i) * (↑b ^ (i + 1))⁻¹
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0

Tactic:
· assumption_mod_cast

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

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k

Tactic:
rw [← le_div_iff₀ pi_div_two_pos, div_eq_inv_mul (W k) _]

Goal state after:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| cos z + -(sin z * I)

Tactic:
← neg_mul,

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| cos z + -sin z * I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
⊢ ↑(Real.arctan x) = (↑(Real.tan (Real.arctan x))).arctan

Tactic:
rw [ofReal_tan, arctan_tan]

Goal state after:
case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ) * θ ^ 2 =
    ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * (cos (x * θ) * θ) * θ

Tactic:
sq θ,

Goal state after:
case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ) * (θ * θ) =
    ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * (cos (x * θ) * θ) * θ
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ ↑n * Real.log |z.im| ≤ |z.re|

Tactic:
← Real.log_pow,

Goal state after:
case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ Real.log (|z.im| ^ n) ≤ |z.re|
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
xne0✝ : p ≠ 0
xne1 : p ≠ 1
y : ℝ
xne0 : y ≠ 0
⊢ y ≠ 1 → deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y

Tactic:
h2

Goal state after:
q : ℕ
p : ℝ
xne0✝ : p ≠ 0
xne1 : p ≠ 1
y : ℝ
xne0 : y ≠ 0
h2 : y ≠ 1
⊢ deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: 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
qpos : 0 < ↑q
h1 : (1 - (↑q)⁻¹) * ↑q < p * ↑q
h2 : (1 - (↑q)⁻¹) * ↑q = ↑q - 1
⊢ ↑q - 1 < p * ↑q

Tactic:
h2

Goal state after:
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
qpos : 0 < ↑q
h1 : ↑q - 1 < p * ↑q
h2 : (1 - (↑q)⁻¹) * ↑q = ↑q - 1
⊢ ↑q - 1 < p * ↑q
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Tactic:
lhs; rw [← sum_monomial_eq p]

Goal state after:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (p.sum fun n a ↦ (monomial n) a) * ↑b ^ k
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ x ^ 2 ≤ 1

Tactic:
sq_le_one_iff_abs_le_one,

Goal state after:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ |x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
⊢ Tendsto (fun r ↦ ∫ (x : ℝ) in a * r..b * r, x⁻¹ • f x) atTop (𝓝 (log (b / a) • R))

Tactic:
apply tendsto_integral_inv_smul_of_tendsto_uniform hf ha hb
    (eventually_atTop.2 ⟨1, fun r hr ↦ zero_lt_one.trans_le hr⟩)
  intro δ hδ
  have hev : ∀ᶠ x in atTop, dist (f x) R < δ :=
    hR.eventually (ball_mem_nhds R hδ)
  rw [Filter.eventually_atTop] at hev
  obtain ⟨N, hN⟩ := hev
  have hm : 0 < min a b := lt_min ha hb
  filter_upwards [eventually_atTop.2 ⟨max 1 (N / min a b), fun r hr ↦ hr⟩] with t ht
  intro x hx
  have ht_pos : 0 < t := lt_of_lt_of_le one_pos ((le_max_left 1 _).trans ht)
  have hNx : N ≤ x :=
    calc N
      _ = min a b * (N / min a b) := by field_simp
      _ ≤ min a b * t :=
        mul_le_mul_of_nonneg_left ((le_max_right _ _).trans ht) hm.le
      _ = min (a * t) (b * t) := by rw [min_mul_of_nonneg _ _ ht_pos.le]
      _ ≤ x := (uIoc_subset_uIcc hx).1
  have hdist := hN x hNx
  rw [dist_eq_norm] at hdist
  exact le_of_lt hdist

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)
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
⊢ ∀ x ∈ spectrum ℝ z, x ≠ 0 ∨ 0 ≤ -1

Tactic:
by
            #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/
            intro x h
            have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h
            grind

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

Goal state before:
pp: case refine_1
s : ℂ
⊢ ↑π ≠ 0 ∨ -s / 2 ≠ 0

Tactic:
exact Or.inl (ofReal_ne_zero.mpr pi_ne_zero)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 + log 7 < 49 / 20

Tactic:
← lt_sub_iff_add_lt',

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ log 7 < 49 / 20 - 1 / 2
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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    t ^ (p - 1) • cfcₙ (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
by
          refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_
          refine ContinuousOn.mono ?_ hspec
          have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one
          fun_prop

Goal state after:
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
⊢ -(↑γ + (↑(↑2 * Real.log ↑2) + ↑(Real.log π))) / ↑↑2 = -(↑γ + log (4 * ↑π)) / ↑↑2

Tactic:
← Real.log_pow,

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)) + ↑(Real.log π))) / ↑↑2 = -(↑γ + log (4 * ↑π)) / ↑↑2
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b (-x) = logb b x

Tactic:
← logb_abs b x,

Goal state after:
b x : ℝ
⊢ logb b (-x) = logb b |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log (b ^ x) = x * log b

pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
log_rpow b_pos

Goal state after:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ x * log b = x * log b

b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 ≤ x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
by
  rcases hx.eq_or_lt with (rfl | hx)
  · simp [zero_le_one]
  exact logb_nonpos_iff hb hx

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

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ e

Tactic:
use 1 ⊔ b ^ e

Goal state after:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∀ (a : ℝ), max 1 (b ^ e) ≤ a → logb b a ≤ e
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
simp_all only [Nat.cast_one, logb_one_left, Int.ceil_zero, Int.clog_one_left]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i ↦ ∫ (x : X), f x ∂μs i) i = v
⊢ ‖v‖ ≤ ‖f‖

Tactic:
← hi

Goal state after:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i ↦ ∫ (x : X), f x ∂μs i) i = v
⊢ ‖(fun i ↦ ∫ (x : X), f x ∂μs i) i‖ ≤ ‖f‖
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: 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 → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
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
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
have key := h _ (f.norm_sub_nonneg)

Goal state after:
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 → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
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
key : limsup (fun i ↦ ∫ (x : X), (const X ‖f‖ - f) x ∂μs i) L ≤ ∫ (x : X), (const X ‖f‖ - f) x ∂μ
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsClosed

Tactic:
rw [← innerRegularWRT_isCompact_closure_iff]

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr.hsup
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
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
have key := h _ (f.norm_sub_nonneg)

Goal state after:
case inr.hsup
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
key : ∫ (x : X), (const X ‖f‖ - f) x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), (const X ‖f‖ - f) x ∂μs i) L
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
this : Finset.univ = {0, 1}
⊢ Submodule.span ℤ {L.ω₁, L.ω₂} = Submodule.span ℤ (⇑L.basis '' ↑{0, 1})

Tactic:
simp [Set.image_insert_eq]

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

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
⊢ regularizedHGFunCoeff a b n = 0 ↔ (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m

Tactic:
unfold regularizedHGFunCoeff
  simp
  grind

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

Goal state before:
pp: case pos
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
regularizedHGFunCoeff_add_one hb

Goal state after:
case pos
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b n *
        ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))) /
      regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun x2 ↦ 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l

Tactic:
exact .sub (.div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
⊢ ℘'[L - l₀] (-z) = -℘'[L - -l₀] z

Tactic:
by
  simp only [derivWeierstrassPExcept]
  rw [← (Equiv.neg L.lattice).tsum_eq]
  simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub,
    ← div_neg, ← tsum_neg, apply_ite, neg_zero]
  congr! 3 with l
  · simp [neg_eq_iff_eq_neg]
  ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
← L.weierstrassPExcept_add 0,

Goal state after:
case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - ↑0] (z + ↑l) + (1 / (z + ↑l - ↑0) ^ 2 - 1 / ↑0 ^ 2) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
rcases h₁.lt_or_gt with h₁ | h₁
  · have : 1 - x ^ 2 < 0 := by nlinarith [h₁]
    rw [sqrt_eq_zero'.2 this.le, div_zero]
    have : arcsin =ᶠ[𝓝 x] fun _ => -(π / 2) :=
      (gt_mem_nhds h₁).mono fun y hy => arcsin_of_le_neg_one hy.le
    exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩
  rcases h₂.lt_or_gt with h₂ | h₂
  · have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
    simp only [← cos_arcsin, one_div] at this ⊢
    exact ⟨sinPartialHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
      sinPartialHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _)
        contDiff_sin.contDiffAt⟩
  · have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
    rw [sqrt_eq_zero'.2 this.le, div_zero]
    have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
    exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩

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

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * ∑ x ∈ range n, c • eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P =
    c * (π / ↑n * ∑ i ∈ range n, eval (cos ((2 * ↑i + 1) / (2 * ↑n) * π)) P)

Tactic:
← smul_sum,

Goal state after:
n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * c • ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P =
    c * (π / ↑n * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ x ∈ range n,
      (Complex.exp (↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π) * I) +
        Complex.exp (-(↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π)) * I)) =
    0

Tactic:
← neg_mul,

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ x ∈ range n,
      (Complex.exp (↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π) * I) + Complex.exp (-↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π) * I)) =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)

Tactic:
rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ ¬2 * ↑n ∣ ↑i

Tactic:
refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ ↑i < 2 * ↑n * (0 + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
⊢ ↑‖x‖₊ = ↑↑(max (x 0).natAbs (x 1).natAbs)

Tactic:
NNReal.coe_inj,

Goal state after:
x : Fin 2 → ℤ
⊢ ‖x‖₊ = ↑(max (x 0).natAbs (x 1).natAbs)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
intro hx

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = 1
⊢ ∃ k ≤ n, Even k ∧ x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = -2

Tactic:
trans ↑(-2 : ℤ)

Goal state after:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = ↑(-2)

L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ↑(-2) = -2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
intro hx

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = -1
⊢ ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)