mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hg2
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ ((fun x_2 ↦ p.rpowIntegrand₀₁ x_2 x) ∘ fun x_2 ↦ x * x_2) x_1 * x) (Ici 0) volume

Tactic:
· simp only [Function.comp]
      rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]
      exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case neg
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬0 < t
⊢ 0 ≤ p.rpowIntegrand₁₂ t x

Tactic:
have ht' : t = 0 := by grind
    simp [rpowIntegrand₁₂, ht', zero_rpow (by grind : p - 1 ≠ 0)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ cfcₙ (fun x ↦ ↑(x.toNNReal.nnrpow p)) a = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ) a

Tactic:
refine cfcₙ_congr fun r hr => ?_

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
r : ℝ
hr : r ∈ quasispectrum ℝ a
⊢ ↑(r.toNNReal.nnrpow p) = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ logb b (b ^ x) = x

Tactic:
by
  rw [logb, div_eq_iff, log_rpow b_pos]
  exact log_ne_zero_of_pos_of_ne_one b_pos b_ne_one

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ BddAbove (?m.103 '' Set.univ)

Tactic:
by simpa using obs.bddAbove

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ BddAbove (?m.103 '' Set.univ)

Tactic:
by simpa using obs.bddAbove

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

Tactic:
calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast

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

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ ℘[L] (-z) = ℘[L] z

Tactic:
simp only [weierstrassP]
  rw [← (Equiv.neg L.lattice).tsum_eq]
  congr with l
  simp
  ring

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

Goal state before:
pp: n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ ↑n * π ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg (Int.cast_nonpos.mpr <| le_of_lt hn) pi_nonneg

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

Goal state before:
pp: n m : ℤ
this :
  ∫ (x : ℝ), eval x 2 * eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
eval_ofNat,

Goal state after:
n m : ℤ
this :
  ∫ (x : ℝ), 2 * eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
⊢ ↑n ≤ P.degree

Tactic:
lift P.degree to ℕ with d hd

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
⊢ P.degree ≠ ⊥

n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
⊢ ↑n ≤ ↑d
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_1
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ ↑k.factorial * ((-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
exact le_of_lt <| mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
      (negOnePow_mul_leadingCoeffC_pos hi)

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

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

Tactic:
refine .congr ?_
    ((L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept l₀).mono (.trans ?_ hr))
  · have := (L.hasFPowerSeriesOnBall_weierstrassPExcept l₀ x r hr0 hr).fderiv
    convert! (ContinuousLinearMap.apply ℂ ℂ (1 : ℂ)).comp_hasFPowerSeriesOnBall this
    ext n
    simp [weierstrassPExceptSeries, derivWeierstrassPExceptSeries]
    ring
  · simpa using Metric.ball_subset_closedBall

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
⊢ L.weierstrassPExceptSeries l₀ = L.weierstrassPSeries

Tactic:
delta weierstrassPSeries weierstrassPExceptSeries
  congr! with z i f
  · rw [L.weierstrassPExcept_of_notMem _ hl₀]
  · simp [hl₀]

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

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ Summable fun j ↦ ∑' (i : ↑↑(box j)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

Tactic:
suffices Summable fun n : ℕ ↦ ∑' (_ : box (α := ℤ × ℤ) n), (n : ℝ) ^ (-k) by
      refine this.congr fun n ↦ tsum_congr fun p ↦ ?_
      simp only [← Int.mem_box.mp p.2, Nat.cast_max, norm_eq_max_natAbs, Matrix.cons_val_zero,
        Matrix.cons_val_one]

Goal state after:
k : ℝ
hk : 2 < k
⊢ Summable fun n ↦ ∑' (x : ↥(box n)), ↑n ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹

Tactic:
by
  apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simpa [pow_two] using! (linear_inv_isBigO_right c₂ z).mul
      (linear_inv_isBigO_right c₁ z).comp_neg_int

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

Goal state before:
pp: m n : ℤ
⊢ fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1)

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg

Goal state after:
case inl
n : ℤ
m : ℕ
⊢ fib (↑m + n) = fib (↑m - 1) * fib n + fib ↑m * fib (n + 1)

case inr
n : ℤ
m : ℕ
⊢ fib (-↑m + n) = fib (-↑m - 1) * fib n + fib (-↑m) * fib (n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℤ
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg

Goal state after:
case inl
n : ℤ
m : ℕ
⊢ (fib ↑m).gcd (fib n) = Nat.fib ((↑m).gcd n)

case inr
n : ℤ
m : ℕ
⊢ (fib (-↑m)).gcd (fib n) = Nat.fib ((-↑m).gcd n)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℤ
h : m ∣ n
⊢ fib m ∣ fib n

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg

Goal state after:
case inl
n : ℤ
m : ℕ
h : ↑m ∣ n
⊢ fib ↑m ∣ fib n

case inr
n : ℤ
m : ℕ
h : -↑m ∣ n
⊢ fib (-↑m) ∣ fib n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hbc
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k) + (↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k) +
      r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
apply norm_add_le_of_le

Goal state after:
case hbc.h₁
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)
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 + u (k * n + r) ≤ u n + (↑k * u n + u r)

Tactic:
by grw [IH]

Goal state after:
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
⊢ ↑k ! * (c ^ (↑k + 1))⁻¹ = ↑k ! * (c ^ (k + 1))⁻¹

Tactic:
← rpow_natCast

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
⊢ ↑k ! * (c ^ (↑k + 1))⁻¹ = ↑k ! * (c ^ ↑(k + 1))⁻¹
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ unop (Subobject.underlying.obj R) :=
  (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
q₂ : unop (Subobject.underlying.obj R) ⟶ ∏ᶜ fun P ↦ unop (Subobject.underlying.obj P) :=
  section_ (Pi.π (fun P ↦ unop (Subobject.underlying.obj P)) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
⊢ factorThruImage (h ≫ f) ≫ q = 0

Tactic:
← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)),

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ unop (Subobject.underlying.obj R) :=
  (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
q₂ : unop (Subobject.underlying.obj R) ⟶ ∏ᶜ fun P ↦ unop (Subobject.underlying.obj P) :=
  section_ (Pi.π (fun P ↦ unop (Subobject.underlying.obj P)) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
⊢ factorThruImage (h ≫ f) ≫ Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X n)

Tactic:
obtain (_ | _ | _ | n) := n <;> apply Injective.injective_under

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✝ : Mono f
abar : Pseudoelement P
⊢ ∀ ⦃a₂ : Pseudoelement P⦄, pseudoApply f abar = pseudoApply f a₂ → abar = a₂

Tactic:
abar'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'
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 : C
⊢ (∃ X_1, P.isoModSerre 0) → P X

Tactic:
rintro ⟨Y, h⟩

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
h : P.isoModSerre 0
⊢ P X
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f

Tactic:
Monad.right_unit_assoc,

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
x : Fin (n + 1 + 1)
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) x = (g • Fin.partialProd f) x

Tactic:
induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using! congrFun (hn (g * f 0) (Fin.tail f)) i

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

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inl_ A B).map f✝) ≫
      (match (Sum.inl_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inl_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inl_ A B).map f✝)

Tactic:
simpa using! e₁.hom.naturality _

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ end_.π (diagram V F₁ F₃) j =
    ((λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃) ≫ end_.π (diagram V F₁ F₃) j

Tactic:
simp only [homEquiv_apply_π, NatTrans.comp_app, eHomEquiv_comp, assoc,
    enrichedComp_π, Functor.op_obj, tensorHom_comp_tensorHom_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
⊢ Nat.card (F.obj X).obj < Nat.card (F.obj Y).obj

Tactic:
by_contra hlt

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).obj < Nat.card (F.obj Y).obj
⊢ False
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ (autEmbedding F) σ X ∈ u X

Tactic:
suffices h : autEmbedding F σ X = 1 by
      rw [h]
      exact (ho X XinI).right

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ (autEmbedding F) σ X = 1
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
V : Type u_1
inst✝¹ : Quiver V
inst✝ : Nonempty V
inhabited_h : Inhabited V
⊢ Nonempty (Quiver.FreeGroupoid V)

Tactic:
exact ⟨⟨@default V _⟩⟩

Goal state after: