mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hi : i ∈ Finset.range (n + 1)
hix : node n i = x
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i

Tactic:
replace hi := Finset.mem_Iic.mpr (Finset.mem_range_succ_iff.mp hi)

Goal state after:
case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Icc (-↑(n + 1)) ↑(n + 1) \ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n

Tactic:
simp only [Nat.cast_add_one, Nat.succ_eq_add_one]

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

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)

Goal state after:
case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ ‖(↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖‖

Tactic:
norm_mul,

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ ‖↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖‖ * ‖↑‖x‖‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ 1 ≤ 1 * 1

Tactic:
one_mul

Goal state after:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ 1 ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        1 * (℘'[L - 0] z * z ^ 3 - 2) * (℘'[L - 0] z * z ^ 3 - 2) -
              4 * (1 * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1)) +
            L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0

Tactic:
one_mul

Goal state after:
L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) * (℘'[L - 0] z * z ^ 3 - 2) -
              4 * ((℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1)) +
            L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case h
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹‖ ≤
    ‖r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖

Tactic:
apply le_trans (by simpa [Real.rpow_neg_one, add_assoc] using
    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0)

Goal state after:
case h
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ (r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ })⁻¹ * ‖![m 0 + a, m 1 + b]‖⁻¹ ≤
    ‖r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        1 * (℘'[L - 0] z * z ^ 3 - 2) * (℘'[L - 0] z * z ^ 3 - 2) -
              4 * (1 * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1)) +
            L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0

Tactic:
one_mul

Goal state after:
case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) * (℘'[L - 0] z * z ^ 3 - 2) -
              4 * ((℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1)) +
            L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
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
⊢ Irrational x

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := Finset.mem_image.mp hroot

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
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
nz : √5 ≠ 0
⊢ 1 * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
one_mul

Goal state after:
n : ℕ
nz : √5 ≠ 0
⊢ (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib n) + φ * ↑(Nat.fib (n + 1))) = φ ^ (n + 2)

Tactic:
rw [add_comm, ih]

Goal state after:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * φ ^ (n + 1) = φ ^ (n + 2)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < 1 * (l - ε * (1 + l))

pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ ↑n ≠ 0

Tactic:
one_mul

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < l - ε * (1 + l)

u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ ↑n ≠ 0
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f

Tactic:
by
    obtain ⟨p, _⟩ := hG₂ X
    obtain ⟨f, rfl⟩ := preadditiveCoyonedaObj_map_surjective hG p f
    obtain ⟨f, rfl⟩ := F.map_surjective f
    exact ⟨f, rfl⟩

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / ↑b

pp: case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < d

Tactic:
· obtain ⟨ε, hε, εpos⟩ : ∃ ε : ℝ, d + ε * (1 + l) < l ∧ 0 < ε := by
      have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists
    filter_upwards [B ε εpos, Ioi_mem_atTop 0] with n hn npos
    simp_rw [div_eq_inv_mul]
    calc
      d < (n : ℝ)⁻¹ * n * (l - ε * (1 + l)) := by
        rw [inv_mul_cancel₀, one_mul]
        · linarith only [hε]
        · exact Nat.cast_ne_zero.2 (ne_of_gt npos)
      _ = (n : ℝ)⁻¹ * (n * l - ε * (1 + l) * n) := by ring
      _ ≤ (n : ℝ)⁻¹ * u n := by gcongr; linarith only [hn]

Goal state after:
case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < d
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
⊢ ∑ i ∈ Finset.range M, f ↑(i + (N + 1)) = ∑ n ∈ Finset.Ico N (N + M), f ↑(n + 1)

Tactic:
Finset.sum_Ico_eq_sum_range

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
⊢ ∑ i ∈ Finset.range M, f ↑(i + (N + 1)) = ∑ k ∈ Finset.range (N + M - N), f ↑(N + k + 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Set.Ici ↑N)
integrable : IntegrableOn f (Set.Ioi ↑N) volume
nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t
s : Finset ℕ
t : ℕ
ht : s ⊆ Finset.range t
⊢ ∑ i ∈ Finset.range t, f ↑(i + N + 1) = ∑ i ∈ Finset.Ico N (N + t), f ↑(i + 1)

Tactic:
Finset.sum_Ico_eq_sum_range

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Set.Ici ↑N)
integrable : IntegrableOn f (Set.Ioi ↑N) volume
nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t
s : Finset ℕ
t : ℕ
ht : s ⊆ Finset.range t
⊢ ∑ i ∈ Finset.range t, f ↑(i + N + 1) = ∑ k ∈ Finset.range (N + t - N), f ↑(N + k + 1)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ 1 * c ≤ c ^ 2

Tactic:
one_mul

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∑ n ∈ Finset.Ico N (N + M), f ↑n = ∑ i ∈ Finset.range M, f ↑(i + N)

Tactic:
Finset.sum_Ico_eq_sum_range

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∑ k ∈ Finset.range (N + M - N), f ↑(N + k) = ∑ i ∈ Finset.range M, f ↑(i + N)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
c' : (i : ι) → Cocone (F i)
hc' : (i : ι) → IsColimit (c' i)
h✝ : Nonempty (IsColimit (coconePointwiseProduct c'))
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
let e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
      coconePointwiseProductIso _ fun i ↦ (hc i).uniqueUpToIso (hc' i)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
c' : (i : ι) → Cocone (F i)
hc' : (i : ι) → IsColimit (c' i)
h✝ : Nonempty (IsColimit (coconePointwiseProduct c'))
e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
  coconePointwiseProductIso F fun i ↦ (hc i).uniqueUpToIso (hc' i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
hy₂ :
  ∃ k_1 f g,
    (hom ((F s).map f)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
      (hom ((F s).map g)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
obtain ⟨i₀, f₀, g₀, h₀⟩ := hy₂

Goal state after:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
i₀ : I s
f₀ g₀ : k s ⟶ i₀
h₀ :
  (hom ((F s).map f₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
    (hom ((F s).map g₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
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
⊢ PreservesFiniteLimits (tensorObj G)

Tactic:
have := preservesInjectiveObjects G hG
  have : (tensorObj G).PreservesMonomorphisms :=
    (tensorObj G).preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects
      (tensorObjPreadditiveCoyonedaObjAdjunction G)
  have : PreservesBinaryBiproducts (tensorObj G) :=
    preservesBinaryBiproducts_of_preservesBinaryCoproducts _
  have : (tensorObj G).Additive := Functor.additive_of_preservesBinaryBiproducts _
  have : (tensorObj G).PreservesHomology :=
    (tensorObj G).preservesHomology_of_preservesMonos_and_cokernels
  exact (tensorObj G).preservesFiniteLimits_of_preservesHomology

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ pullback.snd q p' ≫ q' ≫ h.hom = (pullback.snd q p' ≫ q') ≫ h.hom

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ pullback.snd q p' ≫ q' ≫ h.hom = pullback.snd q p' ≫ q' ≫ h.hom
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom
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.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : (f ≫ z) ≫ t = 0
⊢ ∃ l, L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯

Tactic:
Category.assoc

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.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
⊢ ∃ l, L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
M : Action V G
g h : G
⊢ F.map (M.ρ (g * h)) = F.map (M.ρ h) ≫ F.map (M.ρ g)

Tactic:
rw [map_mul, End.mul_def, F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ D) ≫ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (F.map f ⊗ₘ F.map (inv f)ᘁ)

Tactic:
Functor.map_inv,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ D) ≫ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (F.map f ⊗ₘ inv (F.map f)ᘁ)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map (inv f)ᘁ ⊗ₘ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ

Tactic:
Functor.map_inv,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (inv (F.map f)ᘁ ⊗ₘ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ