mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (Ioo 0 1 • range Subtype.val) = ↑(dim E) * μ (ball 0 1 \ {0})

Tactic:
Subtype.range_coe,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (Ioo 0 1 • sphere 0 1) = ↑(dim E) * μ (ball 0 1 \ {0})
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Tactic:
by
  nontriviality E
  refine ⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩
  refine prod_eq_generateFrom generateFrom_measurableSet
    ((borel_eq_generateFrom_Iio _).symm.trans BorelSpace.measurable_eq.symm)
    isPiSystem_measurableSet isPiSystem_Iio
    μ.toSphere.toFiniteSpanningSetsIn (finiteSpanningSetsIn_volumeIoiPow_range_Iio _)
    fun s hs ↦ forall_mem_range.2 fun r ↦ ?_
  have : Ioo (0 : ℝ) r = r.1 • Ioo (0 : ℝ) 1 := by simp [LinearOrderedField.smul_Ioo r.2.out]
  have hpos : 0 < dim E := Module.finrank_pos
  rw [(Homeomorph.measurableEmbedding _).map_apply, toSphere_apply' _ hs, volumeIoiPow_apply_Iio,
    comap_subtype_coe_apply (measurableSet_singleton _).compl, toSphere_apply_aux, this,
    smul_assoc, μ.addHaar_smul_of_nonneg r.2.out.le, Nat.sub_add_cancel hpos, Nat.cast_pred hpos,
    sub_add_cancel, mul_right_comm, ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, mul_div_cancel₀]
  exacts [(Nat.cast_pos.2 hpos).ne', Nat.cast_nonneg _]

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

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ a ≤ (a ^ (n + 1) / b ^ n + n * b) / (n + 1)

Tactic:
Nat.le_div_iff_mul_le (by positivity),

Goal state after:
n a b : ℕ
hb : b ≠ 0
⊢ a * (n + 1) ≤ a ^ (n + 1) / b ^ n + n * b
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case h.inr
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ -j.re < ↑n

Tactic:
calc
      -j.re ≤ ⌈-j.re⌉₊ := Nat.le_ceil (-j.re)
      _ ≤ b.toFinset.sup (⌈-re ·⌉₊) := mod_cast Finset.le_sup (by grind) (f := (⌈-re ·⌉₊))
      _ < n := by norm_cast

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
refine
      ⟨univ, MeasurableSet.univ,
        ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ Continuous sigmoid

Tactic:
by
  apply Differentiable.continuous (𝕜 := ℝ)  -- fun_prop can't choose `𝕜`
  fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume ↔
    Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume

Tactic:
rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ support ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) ⊆ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| ℘[L] (i + -z)

Tactic:
rw [← hz]; simp

Goal state after:
L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| ℘[L] i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * - -1 = sinh ((↑n + 1) * θ)

Tactic:
neg_neg,

Goal state after:
θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * 1 = sinh ((↑n + 1) * θ)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))

Tactic:
← pow_mul,

Goal state after:
case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))
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‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv (⇑g ∘ f) x‖ₑ ≤ ‖deriv f x‖ₑ

Tactic:
fderiv_comp_deriv

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 : ℝ
hx : x ∈ Ioo a b
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

case hl
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 : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ (⇑g) (f x)

case hf
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 : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x
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
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ

Tactic:
apply (enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc h hab).trans_eq

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
⊢ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ = ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))

Tactic:
suffices HasSum (fun j ↦ r ^ (j + 1) / 3) ((1 : ℝ) / (12 * (n + 1 : ℕ) * ((n + 1 : ℕ) + 1))) by
    refine hasSum_le (fun j ↦ ?_) (log_stirlingSeq_sdiff_hasSum n) this
    simpa [hr, field] using show (3 : ℝ) ≤ 2 * (j + 1) + 1 by norm_cast; grind

Goal state after:
case succ
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
⊢ HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
x : α
h₁ : IsIntegral ℤ x
⊢ (∃ q, x = ↑q) → ∃ k, x = ↑k

Tactic:
rintro ⟨q, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
q : ℚ
h₁ : IsIntegral ℤ ↑q
⊢ ∃ k, ↑q = ↑k
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ cexp (↑(↑q.num / ↑q.den) * ↑π * I) ^ (2 * q.den) = 1

Tactic:
← exp_nat_mul

Goal state after:
q : ℚ
⊢ cexp (↑(2 * q.den) * (↑(↑q.num / ↑q.den) * ↑π * I)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: 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 : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ (- -1) ^ i

Tactic:
neg_neg,

Goal state after:
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 : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ 1 ^ i
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
h_bnd : r ∈ Set.Icc 0 1
⊢ r ∈ {0, 1 / 3, 1 / 2, 2 / 3, 1}

Tactic:
by
  apply smul_left_injective ℚ pi_ne_zero |>.mem_set_image.mp
  replace h_bnd : (r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π) := by
    obtain ⟨hr, hr'⟩ := h_bnd; constructor <;> gcongr <;> norm_cast
  generalize h : (r : ℝ) * π = θ at *
  have := niven_angle_eq ⟨r, h.symm⟩ hcos (by simpa using h_bnd)
  simp_all [Rat.smul_def]
  grind

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

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

Tactic:
exact disjoint_sdiff_self_left

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

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

Tactic:
rw [r1, H1, div_le_iff₀ (by positivity), ← sub_nonneg, H2]

Goal state after:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
H2 :
  (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
⊢ 0 ≤ (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
by
  by_cases hx : x = 0
  · simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]
    by_cases h : -k = 0
    · rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
    · rw [Real.zero_rpow h, mul_zero]
  · 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.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
    suffices (U ℝ n).eval x * sin ((k + 1) * π / (n + 1)) = 0 by
      refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
      field_simp
      norm_cast
      grind
    rw [← hx, U_real_cos, sin_eq_zero_iff]
    use k + 1
    field_simp
    norm_cast
    ring

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

Goal state before:
pp: ⊢ MeromorphicNFOn tan Set.univ

Tactic:
by
  intro x _
  refine MeromorphicNFOn.div analyticAt_sin analyticAt_cos.meromorphicNFAt ?_
  grind [sin_sq_add_cos_sq]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ Irrational φ

Tactic:
convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)

Goal state after:
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = ↑0.5 * (↑1 + √↑5)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ Irrational ψ

Tactic:
convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)

Goal state after:
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = ↑0.5 * (↑1 - √↑5)
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > sInf ((fun n ↦ u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩

Goal state after:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > sInf ((fun n ↦ u n / ↑n) '' Ici 1)
x : ℝ
hx : x ∈ (fun n ↦ u n / ↑n) '' Ici 1
xL : x < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

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

Tactic:
refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
      forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGrpCat).PreservesEpimorphisms
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Abelian.Projective.Basic

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

Tactic:
by
  rw [projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj]
  have := Functor.preservesHomologyOfExact (preadditiveCoyonedaObj P)
  infer_instance

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
a b : ℕ
anti : AntitoneOn f (Icc ↑a ↑b)
integrable : IntegrableOn f (Ioi ↑a) volume
nonneg : ∀ t ∈ Ioi ↑a, 0 ≤ f t
⊢ ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi ↑a, f x

Tactic:
by_cases! hab : b < a

Goal state after:
case pos
f : ℝ → ℝ
a b : ℕ
anti : AntitoneOn f (Icc ↑a ↑b)
integrable : IntegrableOn f (Ioi ↑a) volume
nonneg : ∀ t ∈ Ioi ↑a, 0 ≤ f t
hab : b < a
⊢ ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi ↑a, f x

case neg
f : ℝ → ℝ
a b : ℕ
anti : AntitoneOn f (Icc ↑a ↑b)
integrable : IntegrableOn f (Ioi ↑a) volume
nonneg : ∀ t ∈ Ioi ↑a, 0 ≤ f t
hab : a ≤ b
⊢ ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi ↑a, f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ |∑' (n : ℕ), f ↑n - ∑ n ∈ Finset.range N, f ↑n| ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x

Tactic:
by
  rw [← (AntitoneOn.summable_of_integrableOn_Ioi (mod_cast anti) (mod_cast integrable)
    (mod_cast nonneg)).sum_add_tsum_nat_add N, add_sub_cancel_left,
    abs_of_nonneg (tsum_nonneg <| by grind)]
  convert! AntitoneOn.tsum_comp_add_le_integral (N - 1) (mod_cast anti) (mod_cast integrable)
      (mod_cast nonneg) using 1
  · congr; ext; congr 2; grind
  · norm_cast

Goal state after:
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
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

Tactic:
have : c ^ 3 = c ^ 2 * c := by ring

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 ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ ∃ j ∈ ⋃ i, (CostructuredArrow.map (colimit.ι F i)).obj '' s i, Nonempty (A ⟶ j)

Tactic:
refine ⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ (CostructuredArrow.map (colimit.ι F i)).obj (j i y') ∈ ⋃ i, (CostructuredArrow.map (colimit.ι F i)).obj '' s i

case refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ A ⟶ (CostructuredArrow.map (colimit.ι F i)).obj (j i y')
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j

Tactic:
dsimp only [yoneda_obj_obj, Functor.const_obj_obj] at this

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j
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
inst✝ : Injective Z
n✝ : ℕ
⊢ Injective (((single₀ C).obj Z).X (n✝ + 1))

Tactic:
apply IsZero.injective
      apply HomologicalComplex.isZero_single_obj_X
      simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ Cone (parallelPair f 0 ⋙ P.ι)

Tactic:
exact (Cone.postcompose (Iso.symm (diagramIsoParallelPair _)).hom).obj
      (Fork.ofι (kernel.ι f.hom) (by simp))

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.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
⊢ ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0

Tactic:
by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_comp_monoModSerre_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    exact ⟨W, f ≫ s, MorphismProperty.comp_mem _ _ _ hf hs, by simpa using! eq⟩

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : X
g : G
h : g • a = b
⊢ P (homOfPair (ActionCategory.back ⟨PUnit.unit, b⟩) ↑⟨g, h⟩) = P ⟨g, h⟩

Tactic:
cases inv_smul_eq_iff.mpr h.symm

Goal state after:
case refl
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
b : X
g : G
h : g • g⁻¹ • b = b
⊢ P (homOfPair (ActionCategory.back ⟨PUnit.unit, b⟩) ↑⟨g, h⟩) = P ⟨g, h⟩