mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * (t ^ (p - 1) / t ^ 1) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
Real.rpow_one

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
this : -deriv f 1 = γ
⊢ deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)

Tactic:
by rw [hder_nat n, ← this, neg_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)

Tactic:
let f : ℝ → ℂ := fun x ↦ cexp (-π * a * x ^ 2 + 2 * π * b * x)
  have hFf : 𝓕 f = fun x : ℝ ↦ 1 / a ^ (1 / 2 : ℂ) * cexp (-π / a * (x + I * b) ^ 2) :=
    fourier_gaussian_pi' ha b
  have h1 : 0 < (π * a).re := by
    rw [re_ofReal_mul]
    exact mul_pos pi_pos ha
  have h2 : 0 < (π / a).re := by
    rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
    refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
    contrapose! ha
    rw [ha, zero_re]
  have f_bd : f =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
    convert! (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO
    rwa [neg_mul, neg_re, neg_lt_zero]
  have Ff_bd : (𝓕 f) =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
    rw [hFf]
    have : ∀ (x : ℝ), -π / a * (x + I * b) ^ 2 =
        -π / a * x ^ 2 + (-2 * π * I * b) / a * x + π * b ^ 2 / a := by
      intro x; ring_nf; rw [I_sq]; ring
    simp_rw [this]
    conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
    refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
      ?_ (-2 * π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _
    rwa [neg_div, neg_re, neg_lt_zero]
  convert! Real.tsum_eq_tsum_fourier_of_rpow_decay (by fun_prop) one_lt_two f_bd Ff_bd 0 using 1
  · simp only [f, zero_add, ofReal_intCast]
  · simp [← tsum_mul_left, hFf]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (log b r + 1)

Tactic:
rw [log_of_right_le_one _ hr1.le]

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: ⊢ logb 1 = 0

Tactic:
by ext; rw [logb_one_left, Pi.zero_apply]

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

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x ∈ Ioi 0

Tactic:
simp only [Set.mem_Ioi]

Goal state after:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ 0 < b ^ logb b x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ logb b y = x ↔ b ^ x = y

Tactic:
constructor <;> rintro rfl

Goal state after:
case mp
b y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ logb b y = y

case mpr
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x
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 : ℕ
hb : 1 < b
z : ℤ
⊢ -log b (↑b ^ z)⁻¹ = z

Tactic:
← zpow_neg,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ -log b (↑b ^ (-z)) = z
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 →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
by
  rcases eq_or_neBot L with rfl | hL
  · simp only [tendsto_bot]
  have obs := BoundedContinuousFunction.isBounded_range_integral μs f
  have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)
  have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)
  apply tendsto_of_le_liminf_of_limsup_le _ _ bdd_above bdd_below
  · have key := h _ (f.norm_sub_nonneg)
    simp_rw [f.integral_const_sub ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := limsup_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
    rwa [this, _root_.sub_le_sub_iff_left ‖f‖] at key
  · have key := h _ (f.add_norm_nonneg)
    simp_rw [f.integral_add_const ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := limsup_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
    rwa [this, add_le_add_iff_right] at key

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (f ω ^ p / p)) μ

Tactic:
have aux := (measurable_const (a := p)).aemeasurable (μ := μ)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
aux : AEMeasurable (fun x ↦ p) μ
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (f ω ^ p / p)) μ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ = ‖(l ^ 2 - (s - l) ^ 2) / ((s - l) ^ 2 * l ^ 2)‖

Tactic:
rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa

Goal state after:
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)
n : ℕ
⊢ (↑n ^ ↑(b.card + 1 - a.card))⁻¹ = ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
← zpow_neg,

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)
n : ℕ
⊢ ↑n ^ (-↑(b.card + 1 - a.card)) = ↑n ^ (↑a.card - ↑b.card - 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
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ ↑3 = deriv (fun x2 ↦ ((x2 - ↑x) ^ ↑2)⁻¹) l - 0

Tactic:
← zpow_neg,

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ ↑3 = deriv (fun x2 ↦ (x2 - ↑x) ^ (-↑2)) l - 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ∀ {a b : ℂ},
    a ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]} →
      b ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]} → a + b ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}

Tactic:
by simp_all [funext_iff, ← add_assoc]

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

Goal state before:
pp: L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖((↑l - x) ^ ↑r)⁻¹‖ ≤ ‖↑l - x‖ ^ (-↑r)

Tactic:
← zpow_neg,

Goal state after:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖(↑l - x) ^ (-↑r)‖ ≤ ‖↑l - x‖ ^ (-↑r)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : 1 ≤ n
⊢ (2 + 1 / ↑n)⁻¹ = (fun n ↦ ↑n / (2 * ↑n + 1)) n

Tactic:
rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]

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

Goal state before:
pp: n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ -∫ (x : ℝ) in ↑n * π..0, deriv sin x = 0

Tactic:
integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn

Goal state after:
n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ -(sin 0 - sin (↑n * π)) = 0

n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ ↑n * π ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n m : ℤ
⊢ ∫ (x : ℝ), eval x (2 * T ℝ n * T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT

Tactic:
simp_rw [T_mul_T, eval_add]

Goal state after:
n m : ℤ
⊢ ∫ (x : ℝ), eval x (T ℝ (n + m)) + eval x (T ℝ (n - m)) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
congr! 1 with i hi

Goal state after:
case e'_2.a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
i : ℕ
hi : i ∈ range n
⊢ Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    Complex.exp (↑k / ↑n * ↑π * I) ^ i * (Complex.exp (↑k / ↑n * ↑π * I) - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : ¬l₀ = 0
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀

Tactic:
· fun_prop (disch := simpa)

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

Goal state before:
pp: L : PeriodPair
⊢ Meromorphic L.relation

Tactic:
have : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃ := by fun_prop

Goal state after:
L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
⊢ Meromorphic L.relation
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
a b : ℤ
⊢ (fun m ↦ ((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹) =O[cofinite] fun m ↦ ‖![m 0 + a, m 1 + b]‖⁻¹

Tactic:
Asymptotics.isBigO_iff

Goal state after:
z : ℍ
a b : ℤ
⊢ ∃ c, ∀ᶠ (x : Fin 2 → ℤ) in cofinite, ‖((↑(x 0) + ↑a) * ↑z + ↑(x 1) + ↑b)⁻¹‖ ≤ c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x ↔ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
by
  constructor
  · intro h
    apply (abs_eval_T_real_eq_one_iff hn x).mp
    apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))
    refine h.elim (fun h => ?_) (fun h => ?_)
    · refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))
      have := isMinOn_iff.mp h (cos (1 * π / n)) (by grind [abs_cos_le_one])
      rw [(eval_T_real_eq_neg_one_iff hn (cos (1 * π / n))).mpr ⟨1, Nat.one_le_iff_ne_zero.mpr hn,
        by simp⟩] at this
      assumption
    · refine le_abs.mpr (.inl ?_)
      have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
      rw [(eval_T_real_eq_one_iff hn _).mpr ⟨0, by simp, by simp⟩] at this
      assumption
  · rintro ⟨k, hk, hx⟩
    rw [hx]
    exact isExtrOn_T_real hn hk

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ n.minFac % 2 = 0

Tactic:
← h2,

Goal state after:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ k.succ % 2 = 0
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : a ≤ i ∧ i + 1 ≤ b
⊢ IntegrableOn g (Ico ↑i ↑(i + 1)) volume

Tactic:
rify at hi

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ IntegrableOn g (Ico ↑i ↑(i + 1)) volume
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i + 1 ≤ b
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
rify at hi

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i + 1 ≤ b
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
rify at hi

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c < ↑i

Tactic:
rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
P : IndObjectPresentation X.obj
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
obtain ⟨⟨Q⟩⟩ := Y.2

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
P : IndObjectPresentation X.obj
Q : IndObjectPresentation Y.obj
⊢ Small.{v, max u v} (X ⟶ Y)
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ (ConcreteCategory.hom (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i))
      ((ConcreteCategory.hom (colimitYonedaHomIsoLimit D F).hom) f) =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
change ((colimitYonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ (ConcreteCategory.hom ((colimitYonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i)) f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }
Module: Mathlib.CategoryTheory.Limits.Indization.Products

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a ↦ ⋯.presentation.F ⋙ yoneda
s : α
⊢ f s ≅ colimit (F s)

Tactic:
exact IsColimit.coconePointUniqueUpToIso (hf s).presentation.isColimit (colimit.isColimit _)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator C

Tactic:
suffices HasCoseparator (ShrinkHoms C) from
    HasCoseparator.of_equivalence (ShrinkHoms.equivalence.{w} C).symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator (ShrinkHoms.{u} C)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
⊢ g ≫ f = h ≫ f

Tactic:
refine (hc.pushoutOfHasExactLimitsOfShape f).hom_ext (fun j => ?_)

Goal state after:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
j : J
⊢ (g ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j =
    (h ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ Mono (F.whiskerLeft Φ.ι)

Tactic:
by
  rw [NatTrans.mono_iff_mono_app]
  intro
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
this : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
⊢ PreservesFiniteLimits (tensorObj G)

Tactic:
have : (tensorObj G).PreservesMonomorphisms :=
    (tensorObj G).preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects
      (tensorObjPreadditiveCoyonedaObjAdjunction G)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
this✝ : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
this : (tensorObj G).PreservesMonomorphisms
⊢ PreservesFiniteLimits (tensorObj G)
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ ((HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯).hom ≫
        R.π.f 0 ≫
          (HomologicalComplex.extendXIso ((ChainComplex.single₀ C).obj X) ComplexShape.embeddingDownNat ⋯).inv) ≫
      (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1).hom.f 0 =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv

Tactic:
HomologicalComplex.extendSingleIso_hom_f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ ((HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯).hom ≫
        R.π.f 0 ≫
          (HomologicalComplex.extendXIso ((ChainComplex.single₀ C).obj X) ComplexShape.embeddingDownNat ⋯).inv) ≫
      (((HomologicalComplex.single C (ComplexShape.down ℕ) 0).obj X).extendXIso ComplexShape.embeddingDownNat
            π'._proof_1).hom ≫
        (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X).hom ≫
          (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯

Tactic:
simp only [extMk, Preadditive.add_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv + g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯
          ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X n)

Tactic:
by
  obtain (_ | _ | _ | n) := n <;> apply Injective.injective_under

Goal state after: