mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ MonotoneOn g {a | IsStrictlyPositive a}

Tactic:
refine isClosed_monotoneOn.mem_of_tendsto (f := f) (b := (𝓝[>] 0))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, f x ∈ {f | MonotoneOn f {a | IsStrictlyPositive a}}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2)

Tactic:
push _ ∈ _ at hp
        rw [integral_const_mul, integral_Ioi_rpow_of_lt (by linarith) zero_lt_one]
        ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
harmonic_succ

Goal state after:
case succ
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f 1 + ↑(harmonic n) + 1 / (↑n + 1) = deriv f 1 + ↑(harmonic n + (↑(n + 1))⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case pos
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ (p - 1).rpowIntegrand₀₁ t x

Tactic:
exact rpowIntegrand₀₁_nonneg (by grind) (by grind) hx

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_1
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
⊢ HasDerivAt (fun s ↦ s / 2) (1 / 2) 1

Tactic:
· exact (hasDerivAt_id _).div_const _

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₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
⊢ clog b r₁ ≤ clog b r₂

Tactic:
rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

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

Tactic:
← one_mul (exp (-(ε * y * y)))

Goal state after:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
· calc (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.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ∫⁻ (x : ℝ) in Subtype.val '' Iio x, ENNReal.ofReal (x ^ n) ∂volume = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
image_subtype_val_Ioi_Iio,

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ∫⁻ (x : ℝ) in Ioo 0 ↑x, ENNReal.ofReal (x ^ n) ∂volume = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] (z - ↑l) = ℘[L] z

Tactic:
← L.weierstrassP_add_coe _ l,

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] (z - ↑l + ↑l) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inr
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : -1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
rcases h₂.lt_or_gt with h₂ | h₂

Goal state after:
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
rw [← Filter.tendsto_add_atTop_iff_nat 1]

Goal state after:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
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‖
κ : ℝ
hκ : κ > 0
hκ' : Metric.ball 1 κ ⊆ (fun x_1 ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' (↑L.lattice \ {l₀}))))ᶜ
l : ↥L.lattice
hl : ↑l ≠ l₀
this : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l
⊢ ‖z - x‖ * (κ / 2 + 1) < ‖↑l - x‖

Tactic:
simpa only [Complex.dist_eq, norm_sub_rev x, mul_comm] using this _ l.2 hl

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ sin θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
by
  convert! ← niven (θ := θ - π / 2) ?_ ?_ using 1
  · exact cos_sub_pi_div_two θ
  · exact hθ.imp' (· - 1 / 2) (by intros; push_cast; linarith)
  · simpa [cos_sub_pi_div_two]

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

Goal state before:
pp: case refine_1
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x ↑r
⊢ HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x ↑r

Tactic:
convert! (ContinuousLinearMap.apply ℂ ℂ (1 : ℂ)).comp_hasFPowerSeriesOnBall this

Goal state after:
case e'_10
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x ↑r
⊢ L.derivWeierstrassPExceptSeries l₀ x =
    ((ContinuousLinearMap.apply ℂ ℂ) 1).compFormalMultilinearSeries (L.weierstrassPExceptSeries l₀ x).derivSeries
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
use k

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

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

Tactic:
use k

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = -2

Tactic:
trans ↑(-2 : ℤ)
  · rw [meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)]
    refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
    · have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)
      suffices AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀ by fun_prop
      by_cases hl₀ : l₀ = 0
      · simpa [hl₀] using analyticAt_const
      · fun_prop (disch := simpa)
    · simp
    · filter_upwards [self_mem_nhdsWithin] with z (hz : _ ≠ _)
      have : (z - l₀) ^ 2 ≠ 0 := by simpa [sub_eq_zero]
      simp [← L.ite_eq_one_sub_sq_mul_weierstrassP l₀ h,
        if_neg hz, inv_mul_cancel_left₀ this, zpow_ofNat]
  · norm_num

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

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
⊢ ∃ k_1, ↑↑n * ((2 * ↑k + 1) * π / (2 * ↑n)) = (2 * ↑k_1 + 1) * π / 2

Tactic:
use k

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
⊢ ↑↑n * ((2 * ↑k + 1) * π / (2 * ↑n)) = (2 * ↑↑k + 1) * π / 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ↑(8 * n) * ↑n ^ (-k) ≤ 8 * (↑n * ↑n ^ (-k))

Tactic:
Nat.cast_mul,

Goal state after:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ↑8 * ↑n * ↑n ^ (-k) ≤ 8 * (↑n * ↑n ^ (-k))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: 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)|

Tactic:
refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))

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
⊢ eval x (T ℝ ↑n) ≤ -1
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (HPow.hPow a) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt ha

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun n ↦ (fun n ↦ 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))) n

Tactic:
apply Summable.mul_left

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun i ↦ (x - ↑i)⁻¹ * (x + ↑i)⁻¹

Tactic:
suffices Summable fun i : ℤ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    apply this.comp_injective CharZero.cast_injective

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun i ↦ (x - ↑i)⁻¹ * (x + ↑i)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun a ↦
    ↑k ! * 2 * EisensteinSeries.r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * ‖(↑a + 1) ^ (-1 - ↑k)‖

Tactic:
apply Summable.mul_left

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun i ↦ ‖(↑i + 1) ^ (-1 - ↑k)‖
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L

Tactic:
have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
    (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
      (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <| by simpa

Goal state after:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ 0 ≤ᵐ[volume.restrict (Ioi 0)] fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 x ≤ x ^ (↑k + 1 - 1) * rexp (-(c * x))
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : ObjectProperty C
h𝒢 : P.IsCoseparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h

Tactic:
simpa only [Limits.zero_comp] using hf

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsCoseparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h

Tactic:
simpa only [Limits.zero_comp] using hf

Goal state after:
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
p : G ⟶ F.obj X
h✝ : Epi p
f : F.obj X ⟶ F.obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map f

Tactic:
obtain ⟨f, rfl⟩ := F.map_surjective f

Goal state after:
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
p : G ⟶ F.obj X
h✝ : Epi p
f : X ⟶ Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map (F.map f)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))

Tactic:
refine Tendsto.div (Tendsto.mul ?_ tendsto_const_nhds) ?_ one_ne_zero

Goal state after:
case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1)) atTop (𝓝 1)

case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ n⌋₊ / c k ^ n) atTop (𝓝 1)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasLimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (piObjIso f d).hom ≫ Pi.π (fun s ↦ (f s).obj d) s = (Pi.π f s).app d

Tactic:
by
  simp [piObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasLimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s ↦ (f s).obj d) s

Tactic:
by
  simp [piObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ RepresentablyCoflat Ind.yoneda

Tactic:
refine ⟨fun X => ?_⟩
  suffices IsFiltered (CostructuredArrow yoneda ((Ind.inclusion C).obj X)) from
    IsFiltered.of_equivalence
      ((CostructuredArrow.post Ind.yoneda (Ind.inclusion C) X).asEquivalence.trans
      (CostructuredArrow.mapNatIso Ind.yonedaCompInclusion)).symm
  exact ((isIndObject_iff _).1 (Ind.isIndObject_inclusion_obj X)).1

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
⊢ pseudoApply f 0 = 0

Tactic:
rw [pseudoZero_def, pseudoApply_mk']
  simp

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
a : Pseudoelement P
a' : Over P
⊢ pseudoApply 0 ⟦a'⟧ = 0

Tactic:
by
    rw [pseudoZero_def, pseudoApply_mk']
    simp

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:
Category.id_comp,

Goal state after:
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
⊢ ((fun g ↦ app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.snd f q.hom ≫ q.hom
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ P.isoModSerre.IsStableUnderBaseChange

Tactic:
dsimp [isoModSerre]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderBaseChange
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ P.isoModSerre.IsStableUnderCobaseChange

Tactic:
dsimp [isoModSerre]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderCobaseChange
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 ⊗ₘ inv (F.map f)ᘁ)

Tactic:
Category.id_comp,

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
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (F.map f ⊗ₘ inv (F.map f)ᘁ)
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ 𝟙 (𝟙_ W) ≫ ε F = ε F ≫ F.map (𝟙 (𝟙_ V))

Tactic:
Category.id_comp,

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ ε F = ε F ≫ F.map (𝟙 (𝟙_ V))
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ 𝟙 (F.obj (𝟙_ V)) ≫ η F = η F ≫ 𝟙 (𝟙_ W)

Tactic:
Category.id_comp,

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ η F = η F ≫ 𝟙 (𝟙_ W)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
⊢ B ⥤ C

Tactic:
refine Adjunction.rightAdjointOfEquiv
    (fun X Y => (constructRightAdjointEquiv L _ adj₁ adj₂ h X Y).symm) ?_

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
⊢ ∀ (X' X : C) (Y : B) (f : X' ⟶ X) (g : L.obj X ⟶ Y),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X' Y).symm (L.map f ≫ g) =
      f ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y).symm g
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).inv = α.app a ◁ G.map₂ η.inv ≫ (α.naturality f).inv ≫ F.map₂ η.hom ▷ α.app b

Tactic:
by
  simp [naturality_naturality_iso α η]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).inv =
    α.app a ◁ (G.mapComp f g).hom ≫
      (α_ (α.app a) (G.map f) (G.map g)).inv ≫
        (α.naturality f).inv ▷ G.map g ≫
          (α_ (F.map f) (α.app b) (G.map g)).hom ≫
            F.map f ◁ (α.naturality g).inv ≫ (α_ (F.map f) (F.map g) (α.app c)).inv ≫ (F.mapComp f g).inv ▷ α.app c

Tactic:
by
  simp [naturality_comp_iso α f g]

Goal state after: