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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
⊢ Tendsto (fun t ↦ ∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) F (𝓝 (log (b / a) • V))

Tactic:
Metric.tendsto_nhds

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < ε
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
h_lim : Tendsto (fun p ↦ intervalIntegral g p.1 p.2 volume) ((𝓝[>] 0).curry atTop) (𝓝 (log (b / a) • (L - R)))
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
Metric.tendsto_nhds

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
h_lim :
  ∀ ε > 0, ∀ᶠ (x : ℝ × ℝ) in (𝓝[>] 0).curry atTop, dist (intervalIntegral g x.1 x.2 volume) (log (b / a) • (L - R)) < ε
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹

Tactic:
deriv_Gamma_add_one s hs0,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (s + 1 / 2)) (1 / 2)

Tactic:
· exact ((h_diff (by simp)).hasDerivAt.comp_add_const).differentiableAt

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

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1))
⊢ Tendsto (fun x ↦ -x - (a * x ^ 2 + b * x)) atTop atTop

Tactic:
rw [this]

Goal state after:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1))
⊢ Tendsto (fun x ↦ x * (-a * x - (b + 1))) atTop atTop
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)

Tactic:
have := HasDerivAt.complex_of_real
    (differentiableAt_Gamma _ ?_) Real.hasDerivAt_Gamma_one_half Gamma_ofReal
  · simpa only [neg_mul, one_div, ofReal_neg, ofReal_mul, ofReal_add, ofReal_ofNat, ofNat_log,
      ofReal_inv] using this
  · intro m
    rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]
    exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

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

Goal state before:
pp: b x : ℝ
⊢ logb b⁻¹ x = -logb b x

Tactic:
simp [logb, div_neg]

Goal state after:
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 : ℕ
r : R
⊢ log b r⁻¹⁻¹⁻¹ = -clog b r⁻¹⁻¹

Tactic:
clog_inv,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ log b r⁻¹⁻¹⁻¹ = - -log b r⁻¹
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 : ℕ
r : R
⊢ -clog b r⁻¹ = log b r

Tactic:
clog_inv,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ - -log b r = log b r
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
apply HasDerivAt.mul (hasDerivAt_id' y)

Goal state after:
ε y : ℝ
⊢ HasDerivAt (fun x ↦ rexp (-(ε * x * x))) (rexp (-(ε * y * y)) * (-2 * ε * y)) y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
· rw [Nat.one_lt_iff_ne_zero_and_ne_one, ← or_iff_not_and_not] at hb
    cases hb
    · simp_all only [CharP.cast_eq_zero, logb_zero_left, Int.floor_zero, Int.log_zero_left]
    · simp_all only [Nat.cast_one, logb_one_left, Int.floor_zero, Int.log_one_left]

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

Goal state before:

Tactic:
(fun x ↦ log (c * x))
      =ᶠ[atTop] (fun x => log c + log x) := by
          filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
      _ =O[atTop] log :=
          isLittleO_const_log_atTop.isBigO.add (Asymptotics.isBigO_refl ..)

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

Goal state before:
pp: case pos
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) ^ (n + 2) ≤ a

pp: case neg
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ guess ^ (n + 2) ≤ a

Tactic:
case pos =>
      grind

Goal state after:
case neg
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ guess ^ (n + 2) ≤ a
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 [[a, b]]
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
rcases le_or_gt a b with hab | hab
  · simp only [uIcc_of_le hab] at h
    exact integral_deriv_of_contDiffOn_Icc h hab
  · simp only [uIcc_of_ge hab.le] at h
    rw [integral_symm, integral_deriv_of_contDiffOn_Icc h hab.le]
    abel

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 : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖∫ (x : ℝ) in a..b, deriv (⇑g ∘ f) x‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_f
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - if ↑l = l₀ then ((l₀ - x) ^ ↑(i + 3))⁻¹ else 0) =
    if ↑l = l₀ then 0 else (↑(i + 1) + 1) * ((↑l - x) ^ ↑(i + 1 + 2))⁻¹ - 0 i

Tactic:
split_ifs with e

Goal state after:
case pos
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - ((l₀ - x) ^ ↑(i + 3))⁻¹) = 0

case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1) + 1) * ((↑l - x) ^ ↑(i + 1 + 2))⁻¹ - 0 i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (node n i - node n j)) :=
    Finset.prod_pos (fun j hj => mul_pos_of_neg_of_neg neg_one_lt_zero <| sub_neg.mpr <|
    node_lt hi (Finset.mem_range.mp hj))

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

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = 1
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Even k

Tactic:
eval_T_real_cos_int_mul_pi_div hn,

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : ↑↑(↑k).negOnePow = 1
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Even k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos (↑k * π / ↑n)
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = 1

Tactic:
eval_T_real_cos_int_mul_pi_div hn,

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos (↑k * π / ↑n)
⊢ ↑↑(↑k).negOnePow = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = -1
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Odd k

Tactic:
eval_T_real_cos_int_mul_pi_div hn,

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : ↑↑(↑k).negOnePow = -1
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Odd k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos (↑k * π / ↑n)
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = -1

Tactic:
eval_T_real_cos_int_mul_pi_div hn,

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos (↑k * π / ↑n)
⊢ ↑↑(↑k).negOnePow = -1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ Summable fun x ↦ ‖x‖ ^ (-k)

Tactic:
← (finTwoArrowEquiv _).symm.summable_iff,

Goal state after:
k : ℝ
hk : 2 < k
⊢ Summable ((fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = a ^ (1 + n) * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k

Tactic:
pow_add,

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b =
    a ^ 1 * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ 1 + sineTerm x n ≠ 0

Tactic:
simp only [sineTerm, ne_eq]
  rw [add_eq_zero_iff_eq_neg, neg_div', eq_div_iff]
  · have := (integerComplement_pow_two_ne_pow_two hx (n + 1 : ℤ))
    aesop
  · simp [Nat.cast_add_one_ne_zero n]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n + 1) * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n - 1) + Nat.fib (n + n))) =
    (-1) ^ (n + n - 1 + 1) * ↑(Nat.fib (n + n - 1))

Tactic:
pow_add,

Goal state after:
case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n) * (-1) ^ 1 * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n - 1) + Nat.fib (n + n))) =
    (-1) ^ (n + n - 1 + 1) * ↑(Nat.fib (n + n - 1))
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = ↑(k + 1) * u n + u r

Tactic:
by simp; ring

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

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z

Tactic:
eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑n + 1)) ^ (-1 - ↑k) + (z - (↑n + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))

Tactic:
refine (hf.mono ?_).intervalIntegrable

Goal state after:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
Module: Mathlib.CategoryTheory.Abelian.Projective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj P)

Tactic:
apply Functor.preservesFiniteColimits_of_preservesHomology

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
⊢ Epi (AddCommGrpCat.ofHom (preadditiveCoyonedaObj G).mapAddHom)

Tactic:
let cm : ShortComplex C := ⟨kernel.ι p, p, by simp⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
⊢ Epi (AddCommGrpCat.ofHom (preadditiveCoyonedaObj G).mapAddHom)
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ colimit.post F (coyoneda.obj (op (yoneda.obj X))) =
    (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (yoneda.op.obj (op X))).inv ≫
      ((yonedaYonedaColimit F).app (op X)).inv

Tactic:
rw [yonedaYonedaColimit_app_inv, Iso.inv_hom_id_assoc]

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

Goal state before:

Tactic:
(1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
    _ ≤ c ^ i - 1 := by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
    _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : Injective J
⊢ PreservesFiniteColimits (preadditiveYonedaObj J)

Tactic:
apply Functor.preservesFiniteColimits_of_preservesHomology

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
B : C
hB : Injective B
⊢ Module.Injective (End G)ᵐᵒᵖ ↑((preadditiveCoyonedaObj G).1 B)

Tactic:
simp only [preadditiveCoyonedaObj_obj_carrier]

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
B : C
hB : Injective B
⊢ Module.Injective (End G)ᵐᵒᵖ (G ⟶ B)
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
n : ℤ
hn : n ≤ 0
⊢ Projective (R.cochainComplex.X n)

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
n : ℤ
hn : ¬n ≤ 0
⊢ Projective (R.cochainComplex.X n)

Tactic:
· obtain ⟨k, rfl⟩ := Int.exists_eq_neg_ofNat hn
    exact Projective.of_iso (R.cochainComplexXIso (-k) k).symm inferInstance

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
n : ℤ
hn : ¬n ≤ 0
⊢ Projective (R.cochainComplex.X n)
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: case mpr.refine_2
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))
inv : (Φ.colon Ψ).r.obj X ⟶ (KernelFork.ofι (Φ.ι.app X) ⋯).pt
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ inv ≫ (Over.Hom.left (Φ.toColon Ψ).hom).app X = 𝟙 ((Φ.colon Ψ).obj.left.obj X)

Tactic:
simp [← cancel_mono ((Φ.colon Ψ).ι.app X), hinv]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ 𝟙 (pullback f q.hom) ≫ ((fun g ↦ app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.snd f q.hom ≫ q.hom

Tactic:
rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f =
    0
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✝ : Mono (L.map f)
⊢ P.monoModSerre f

Tactic:
by
    have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
    simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (𝟙 _) (kernel.ι f)

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
this : ∀ (W : D) (z : W ⟶ L.obj X), z ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = z
s : Fork (L.map f) 0
x✝¹ x✝ : s.pt ⟶ (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L).pt
h₁ : x✝¹ ≫ Fork.ι (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L) = s.ι
h₂ : x✝ ≫ Fork.ι (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L) = s.ι
⊢ x✝¹ = x✝

Tactic:
simpa [cancel_mono] using h₁.trans h₂.symm

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✝ : Group G
A : Action V G
g : G
⊢ A.ρ (g⁻¹ * g) = 𝟙 A.V

Tactic:
by rw [inv_mul_cancel, ρ_one]

Goal state after:
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
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ (a✝ • 0).hom = Hom.hom 0

Tactic:
exact smul_zero _

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_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ ∃ a, (res V f).map a = g

Tactic:
by
    use ⟨g.hom, fun h ↦ ?_⟩
    · ext
      simp
    · obtain ⟨a, rfl⟩ := f_surj h
      have : X.ρ (f a) = ((res V f).obj X).ρ a := rfl
      rw [this, g.comm a]
      simp

Goal state after:
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.ρ h ≫ M.ρ g) = F.map (M.ρ h) ≫ F.map (M.ρ g)

Tactic:
F.map_comp

Goal state after:
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.ρ h) ≫ F.map (M.ρ g) = F.map (M.ρ h) ≫ F.map (M.ρ g)
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
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map (f.hom ≫ Y✝.ρ g) = F.map f.hom ≫ F.map (Y✝.ρ g)

Tactic:
F.map_comp

Goal state after:
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
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map f.hom ≫ F.map (Y✝.ρ g) = F.map f.hom ≫ F.map (Y✝.ρ g)