mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ
n✝ : ℕ
⊢ log (stirlingSeq (n✝ + 1)) = log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

Tactic:
rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
      <;> positivity

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

Goal state before:
pp: case f
| fun n ↦ ↑n / (2 * ↑n + 1)

pp: case l₁
| atTop

pp: case l₂
| 𝓝 (1 / 2)

Tactic:
· skip

Goal state after:
case l₁
| atTop

case l₂
| 𝓝 (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case l₁
| atTop

pp: case l₂
| 𝓝 (1 / 2)

Tactic:
· skip

Goal state after:
case l₂
| 𝓝 (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = log (2 * π * ↑n) / 2 + log ((↑n / rexp 1) ^ n)

pp: n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0

Tactic:
log_mul (x := 2 * π),

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = (log (2 * π) + log ↑n) / 2 + log ((↑n / rexp 1) ^ n)

case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ (∑' (l : ↥L.lattice) (i : ℕ),
      if ↑l = l₀ then 0 else ((↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0) * (z - x) ^ i) =
    ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
trans ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ (∑' (l : ↥L.lattice) (i : ℕ),
      if ↑l = l₀ then 0 else ((↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0) * (z - x) ^ i) =
    ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i

L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i =
    ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
this : d - 1 < n - 1
⊢ 2 ^ (d - 1) < 2 ^ (n - 1)

Tactic:
gcongr; norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
by
  have H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 =
    c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2 := by ring
  have H2 : (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2)
    - z.im ^ 2 = (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2 := by ring
  rw [r1, H1, div_le_iff₀ (by positivity), ← sub_nonneg, H2]
  exact add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hd) (sq_nonneg _))

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    eval x ((⇑derivative)^[k] P)

Tactic:
have h₁ : P.degree < (Finset.range (n + 1)).card := by
    rw [Finset.card_range]; grw [hP]; norm_cast; simp

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    eval x ((⇑derivative)^[k] P)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
b : ℤ
⊢ Tendsto (fun d ↦ 1 / (↑b * z - ↑d)) atTop (𝓝 0)

Tactic:
by
  grind [neg_zero, (tendsto_zero_inv_linear z (-b)).neg]

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

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
this : Irrational (cos (↑(Rat.divInt (2 * ↑k + 1) (2 * ↑n)) * π))
⊢ Irrational x

Tactic:
← hk₂

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
this : Irrational (cos (↑(Rat.divInt (2 * ↑k + 1) (2 * ↑n)) * π))
⊢ Irrational (cos ((2 * ↑k + 1) * π / (2 * ↑n)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 - cexp (2 * ↑π * I * ↑z))⁻¹) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
(tsum_geometric_of_norm_lt_one
    (UpperHalfPlane.norm_exp_two_pi_I_lt_one z)).symm,

Goal state after:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn✝ : ¬n = 0
hn : 2 * k + 1 = n
hroot : x ∈ Finset.image (fun k ↦ cos (↑(2 * k + 1) * π / ↑(2 * n))) (Finset.range n)
hk₂ : cos (↑(2 * k + 1) * π / ↑(2 * n)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ x = 0

Tactic:
← hk₂

Goal state after:
n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn✝ : ¬n = 0
hn : 2 * k + 1 = n
hroot : x ∈ Finset.image (fun k ↦ cos (↑(2 * k + 1) * π / ↑(2 * n))) (Finset.range n)
hk₂ : cos (↑(2 * k + 1) * π / ↑(2 * n)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ cos (↑(2 * k + 1) * π / ↑(2 * n)) = 0
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℤ
⊢ fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1)

Tactic:
by
  obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
  · exact fib_natCast_add _ _
  · obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
    · exact fib_add_natCast _ _
    · exact fib_neg_natCast_add_neg_natCast _ _

Goal state after:
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
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), g x = ∫ (x : ℝ) in ↑a..↑b, g x

Tactic:
sum_integral_adjacent_intervals_Ico (a := (↑·)) hab

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
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∫ (x : ℝ) in ↑a..↑b, g x = ∫ (x : ℝ) in ↑a..↑b, g x

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
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∀ k ∈ Ico a b, IntervalIntegrable g volume ↑k ↑(k + 1)
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
· intro
    exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case c0
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
⊢ g (↑b - 1) ≤ g ↑i

Tactic:
apply hg

Goal state after:
case c0.x
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
⊢ ↑i ∈ Icc (↑a - 1) (↑b - 1)

case c0.x
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
⊢ ↑b - 1 ∈ Icc (↑a - 1) (↑b - 1)

case c0.a
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
⊢ ↑i ≤ ↑b - 1
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
⊢ g ↑i ≤ g (x - 1)

Tactic:
apply hg

Goal state after:
case h₂.x
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
⊢ x - 1 ∈ Icc (↑a - 1) (↑b - 1)

case h₂.x
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
⊢ ↑i ∈ Icc (↑a - 1) (↑b - 1)

case h₂.a
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
⊢ x - 1 ≤ ↑i
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: 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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ g (x - 1)) b✝ ≤ (fun x ↦ g (x - 1)) a✝¹

Tactic:
apply hg

Goal state after:
case x
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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ a✝¹ - 1 ∈ Icc (↑a - 1) (↑b - 1)

case x
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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ b✝ - 1 ∈ Icc (↑a - 1) (↑b - 1)

case a
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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ a✝¹ - 1 ≤ b✝ - 1
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case c0
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
⊢ g (↑a - 1) ≤ g (x - 1)

Tactic:
apply hg

Goal state after:
case c0.x
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
⊢ ↑a - 1 ∈ Icc (↑a - 1) (↑b - 1)

case c0.x
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
⊢ x - 1 ∈ Icc (↑a - 1) (↑b - 1)

case c0.a
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
⊢ ↑a - 1 ≤ 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
⊢ g (x - 1) ≤ g ↑i

Tactic:
apply hg

Goal state after:
case h₂.x
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
⊢ x - 1 ∈ Icc (↑a - 1) (↑b - 1)

case h₂.x
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
⊢ ↑i ∈ Icc (↑a - 1) (↑b - 1)

case h₂.a
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
⊢ x - 1 ≤ ↑i
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: 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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ g (x - 1)) a✝¹ ≤ (fun x ↦ g (x - 1)) b✝

Tactic:
apply hg

Goal state after:
case x
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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ a✝¹ - 1 ∈ Icc (↑a - 1) (↑b - 1)

case x
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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ b✝ - 1 ∈ Icc (↑a - 1) (↑b - 1)

case a
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)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ a✝¹ - 1 ≤ b✝ - 1
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)
⊢ IsIndObject (∏ᶜ f)

Tactic:
let F := fun a => (hf a).presentation.F ⋙ yoneda
  suffices (∏ᶜ f ≅ colimit (pointwiseProduct F)) from
    (isIndObject_colimit _ _ (fun i => h _)).map this.inv
  refine Pi.mapIso (fun s => ?_) ≪≫ (asIso (colimitPointwiseProductToProductColimit F)).symm
  exact IsColimit.coconePointUniqueUpToIso (hf s).presentation.isColimit (colimit.isColimit _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
⊢ ∃ a, (hom (colimitPointwiseProductToProductColimit F)) a = x

Tactic:
· have hch : ∀ (s : α), ∃ (i : I s) (xi : (F s).obj i), colimit.ι (F s) i xi =
        Pi.π (fun s => colimit (F s)) s x := fun s => Types.jointly_surjective' _
    choose k p hk using hch
    refine ⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩
    refine Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)
    have := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s)
      ((Types.productIso _).inv p)
    exact this.trans (by simpa [Functor.pi] using hk _)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ (Φ.colon Ψ).ι.app X ≫ Φ.π.app X = 0

Tactic:
by
        rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolutions C).map f ≫ J.iso.hom = I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ

Tactic:
apply HomotopyCategory.eq_of_homotopy
  apply descHomotopy f
  all_goals aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
⊢ pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧ → ⟦a⟧ = ⟦a'⟧

Tactic:
refine fun ha ↦ Quotient.sound ?_

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
⊢ a ≈ a'
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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (g ≫ f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
rw [Cocycle.fromSingleMk_precomp g _ (zero_add _) _ (by lia) (by
      simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_precomp, ← ShiftedHom.mk₀_comp 0 rfl,
    ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) (add_zero (n : ℤ)) (by simp)]

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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)) ⋯).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      (((ShiftedHom.mk₀ 0 ⋯ ((singleFunctor C 0).map g)).map DerivedCategory.Q).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ X' s, ∃ (_ : P.isoModSerre s), s ≫ f = 0

Tactic:
refine ⟨_, kernel.ι f, ?_, by simp⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ P.isoModSerre (kernel.ι f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map (cokernel.π f) = 0

Tactic:
← cancel_epi (L.map f),

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map f ≫ L.map (cokernel.π f) = L.map f ≫ 0
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
x✝¹ : SingleObj M
x✝ : X
⊢ (ConcreteCategory.hom (↾fun x ↦ 𝟙 x✝¹ • x)).toFun x✝ = (ConcreteCategory.hom (𝟙 X)).toFun x✝

Tactic:
exact MulAction.one_smul _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ L.map φ.f ≫ L.map f = 0

Tactic:
by
      rw [← hφ, Category.assoc, Category.assoc, hw, comp_zero, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
⊢ (whiskeringLeft L P E).essImage = fun G ↦ P.isoModSerre.IsInvertedBy G.obj

Tactic:
ext F

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
⊢ (whiskeringLeft L P E).essImage F ↔ P.isoModSerre.IsInvertedBy F.obj