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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
⊢ ‖-2 / (s - ↑l) ^ 3‖ ≤ 16 * ‖l‖ ^ (-3)

Tactic:
have : s ≠ ↑l := by rintro rfl; exfalso; linarith

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this : s ≠ ↑l
⊢ ‖-2 / (s - ↑l) ^ 3‖ ≤ 16 * ‖l‖ ^ (-3)
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 - ↑0] (z + ↑l) + (1 / (z + ↑l - ↑0) ^ 2 - 1 / ↑0 ^ 2) = ℘[L] z

Tactic:
Submodule.coe_zero,

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.Chebyshev.Basic

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

Tactic:
rw [U_complex_cos]

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

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
by
  rcases hab.eq_or_lt with rfl | h'ab
  · simp
  apply integral_eq_sub_of_hasDerivAt_of_le hab h.continuousOn
  · intro x hx
    apply DifferentiableAt.hasDerivAt
    apply ((h x ⟨hx.1.le, hx.2.le⟩).differentiableWithinAt one_ne_zero).differentiableAt
    exact Icc_mem_nhds hx.1 hx.2
  · have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn
    apply (this.intervalIntegrable_of_Icc (μ := volume) hab).congr_ae
    simp only [hab, uIoc_of_le]
    rw [← restrict_Ioo_eq_restrict_Ioc]
    filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
    exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

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

Goal state before:
pp: m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k ↦ f (k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))

Tactic:
hasSum_nat_add_iff

Goal state after:
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

Tactic:
rw [integral_symm, integral_derivWithin_Icc_of_contDiffOn_Icc h hab.le]

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

Goal state before:
pp: n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(k + 1) + 1) ≤ 1

Tactic:
one_div

Goal state after:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(k + 1) + 1)⁻¹ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ (Finset.range i).card * ∏ x ∈ Finset.range i, (node n i - node n x)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
Finset.card_range

Goal state after:
case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ∑ i ≤ n, eval (node n i) P * leadingCoeffC n i = P.coeff n

Tactic:
leadingCoeffC

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ∑ i ≤ n, eval (node n i) P * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ = P.coeff n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(Finset.range (n + 1)).card

Tactic:
Finset.card_range

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(box (n + 1)) = 8 * (n + 1)

Tactic:
simp_rw [Prod.card_box_succ, card_Icc, sub_neg_eq_add]

Goal state after:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n.succ + 1 + ↑n.succ).toNat * (↑n.succ + 1 + ↑n.succ).toNat - (↑n + 1 + ↑n).toNat * (↑n + 1 + ↑n).toNat =
    8 * (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(Finset.range (n + 1)).card

Tactic:
Finset.card_range

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
rw [← Real.mul_rpow (r_pos _).le (norm_nonneg _)]
    exact Real.rpow_le_rpow_of_nonpos (mul_pos (r_pos _) (norm_pos_iff.mpr hx)) (r_mul_max_le z hx)
      (neg_nonpos.mpr hk)

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

Goal state before:
pp: case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z) =o[cofinite] fun n ↦ ↑n

Tactic:
simpa [-Int.cofinite_eq] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real

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

Goal state before:
pp: case ho
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑e) =o[cofinite] fun n ↦ ↑n

Tactic:
simpa [-Int.cofinite_eq] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real

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

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑(Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).card = (U ℝ ↑n).degree

Tactic:
rw [Finset.card_image_of_injOn, Finset.card_range, degree_U_natCast]

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) ↑(Finset.range n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
by
  filter_upwards [L.compl_lattice_sdiff_singleton_mem_nhds _] with z hz
  by_cases hz0 : z = 0
  · simp [hz0, relation]; norm_num
  replace hz : z ∉ L.lattice := by simp_all
  simp only [Pi.mul_apply, Pi.pow_apply, relation, ↓reduceIte, hz,
    ← ZeroMemClass.coe_zero L.lattice, L.derivWeierstrassPExcept_def, L.weierstrassPExcept_def]
  simp
  field

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
by
  cases k.even_or_odd
  case inl hk₂ => exact .inr (isLocalMax_T_real hn hk₀ hk₁ hk₂)
  case inr hk₂ => exact .inl (isLocalMin_T_real hn hk₁ hk₂)

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

Tactic:
refine h.elim (fun h => ?_) (fun h => ?_)

Goal state after:
case mp.refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMinOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ ∑ x ∈ Finset.range (4 + 1),
            ↑(Nat.choose 4 x) *
                (∑ x_1 ∈ Finset.range (x + 1),
                    ↑(x.choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) * ↑(if x - x_1 = 3 then 3! else 0) -
                  if x = 0 then 2 else 0) *
              (∑ x_1 ∈ Finset.range (4 - x + 1),
                  ↑((4 - x).choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) *
                    ↑(if 4 - x - x_1 = 3 then 3! else 0) -
                if 4 - x = 0 then 2 else 0) -
          ∑ x ∈ Finset.range (4 + 1),
            (↑(Nat.choose 4 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ x_2 ∈ Finset.range (x + 1),
                              (↑(x.choose x_2) *
                                  if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                                ↑(if x - x_2 = 2 then 2! else 0) +
                            if x = 0 then 1 else 0) *
                        (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                            (↑((x_1 - x).choose x_2) *
                                if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                              ↑(if x_1 - x - x_2 = 2 then 2! else 0) +
                          if x_1 - x = 0 then 1 else 0)) *
                  (∑ x_2 ∈ Finset.range (4 - x - x_1 + 1),
                      (↑((4 - x - x_1).choose x_2) *
                          if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                        ↑(if 4 - x - x_1 - x_2 = 2 then 2! else 0) +
                    if 4 - x - x_1 = 0 then 1 else 0) +
        ∑ x ∈ Finset.range (4 + 1),
          (↑(Nat.choose 4 x) * if x = 0 then L.g₂ else 0) *
            (∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) * if x_1 = 0 then ℘[L - 0] 0 else ↑(x_1 + 1)! * L.sumInvPow 0 (x_1 + 2)) *
                  ↑(if 4 - x - x_1 = 6 then 6! else 0) +
              ↑(if 4 - x = 4 then 4! else 0)) +
      ∑ x ∈ Finset.range (4 + 1), (↑(Nat.choose 4 x) * if x = 0 then L.g₃ else 0) * ↑(if 4 - x = 6 then 6! else 0) =
    0

Tactic:
simp [Finset.sum_range_succ, show Nat.choose 4 2 = 6 by rfl, g₂]; ring

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)

Tactic:
div_neg,

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)

Tactic:
div_neg,

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib n = 0 ↔ n = 0

Tactic:
by
  obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg <;> simp [fib_neg_natCast]

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ -1 - ↑k = -↑(k + 1)

Tactic:
norm_cast; lia

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + ↑n) ^ (k + 1) = ((z + ↑n) ^ (k + 1))⁻¹

Tactic:
one_div

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ ((z + ↑n) ^ (k + 1))⁻¹ = ((z + ↑n) ^ (k + 1))⁻¹
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))

Tactic:
have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos

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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
B : N - 1 + 1 = N
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ι f g ≫ φ f g = 0

Tactic:
by
  dsimp [ι, φ]
  aesop

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

Goal state before:
pp: case hbc
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))

Tactic:
have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos

Goal state after:
case hbc
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
B : N - 1 + 1 = N
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ (Pi.lift fun s ↦ Pi.π f (↑s).as) ≫ Pi.π (fun x ↦ f (↑x).as) v =
    (∑ a ∈ (Opposite.unop S).attach, Pi.π f (↑a).as ≫ Pi.ι (fun a ↦ f (↑a).as) a) ≫ Pi.π (fun x ↦ f (↑x).as) v

Tactic:
simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Preadditive.sum_comp, Category.assoc]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ Pi.π f (↑v).as =
    ∑ x ∈ (Opposite.unop S).attach, Pi.π f (↑x).as ≫ Pi.ι (fun a ↦ f (↑a).as) x ≫ Pi.π (fun x ↦ f (↑x).as) v
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono (I.ι.f (n✝ + 1))

Tactic:
· rw [ι_f_succ]; infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
by
    simpa [id_comp] using descIdHomotopy _ _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) J J) (𝟙 J.cocomplex)

Tactic:
by
    simpa [id_comp] using descIdHomotopy _ _

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g

Tactic:
have w := comm g =≫ f.inv

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
w : (M.ρ g ≫ f.hom) ≫ f.inv = (f.hom ≫ N.ρ g) ≫ f.inv
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
J : Type u_3
inst✝¹ : Category.{v_2, u_3} J
K : J ⥤ Action V G
inst✝ : HasColimit (K ⋙ forget V G)
⊢ PreservesColimit K (forget V G)

Tactic:
by
  change PreservesColimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
  have (k : SingleObj G) :
      HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasColimit (K ⋙ forget V G))
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η → ∀ (c : C), Mono (η.app c)

Tactic:
intro h c
    exact (inferInstance : Mono (((evaluation _ _).obj c).map η))

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
⊢ Function.RightInverse (fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) fun f ↦
    { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ }

Tactic:
intro f
            ext x
            dsimp
            ext g
            simp only [NatTrans.naturality_assoc,
              evaluationRightAdjoint_obj_obj, evaluationRightAdjoint_obj_map, limit.lift_π,
              Fan.mk_pt, Fan.mk_π_app, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a✝ b✝ c✝ : Pith B
f✝ g✝ : a✝ ⟶ b✝
h✝ i✝ : b✝ ⟶ c✝
η : f✝ ⟶ g✝
θ : h✝ ⟶ i✝
⊢ { iso := f✝.of ◁ᵢ θ.iso } ≫ { iso := η.iso ▷ᵢ i✝.of } = { iso := η.iso ▷ᵢ h✝.of } ≫ { iso := g✝.of ◁ᵢ θ.iso }

Tactic:
ext
    simp [whisker_exchange]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToIso ⋯).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
eqToIso.hom,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' f (𝟙 b₁) f ⋯ = (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm

Tactic:
ext
  rw [mapComp']
  dsimp
  rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToIso ⋯).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
eqToIso.hom,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : graphFunctor.map a₁✝ = graphFunctor.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext
    simp [Function.graph_injective congr(($h).rel)]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = f.preimage s ∪ f.Domᶜ

Tactic:
rw [preimage_eq, Set.inter_union_distrib_right, Set.union_comm (Dom f), Set.compl_union_self,
    Set.inter_univ, Set.union_eq_self_of_subset_right (f.compl_dom_subset_core s)]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝¹ : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst✝ : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂ ≫ snd f g = snd f' g' ≫ γ₂

Tactic:
simp only [pullbackMap, lift_snd]

Goal state after: