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

Goal state before:
pp: a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ *
      ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) *
        (Polynomial.eval c (ascPochhammer ℂ n))⁻¹) =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))

Tactic:
← Gamma_add_nat_div_Gamma_eq c hc

Goal state after:
a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ *
      ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) *
        (Gamma (c + ↑n) / Gamma c)⁻¹) =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: a b : ℝ
hab : a < b
⊢ a.sigmoid < b.sigmoid

Tactic:
by
  simp only [sigmoid]
  gcongr

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
⊢ dim E • μ.real (ball 0 1) • ∫ (x : ↑(Ioi 0)), (↑x ^ (dim E - 1)).toNNReal • f ↑x ∂Measure.comap Subtype.val volume =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

pp: case f_meas
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
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal

Tactic:
integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,

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
⊢ dim E • μ.real (ball 0 1) • ∫ (x : ℝ) in Ioi 0, (x ^ (dim E - 1)).toNNReal • f x ∂volume =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

case f_meas
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
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0

Tactic:
· exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

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

pp: 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)

pp: 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

Tactic:
rotate_left

Goal state after:
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

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

Tactic:
apply lintegral_congr_ae

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
⊢ (fun a ↦ ‖deriv f a‖ₑ) =ᵐ[volume.restrict (Icc a b)] fun a_1 ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ 1 / (12 * ↑n * (↑n + 1)) ≤ 1 / (4 * ↑n ^ 2)

Tactic:
cases n <;> simp [field]

Goal state after:
case succ
n✝ : ℕ
⊢ (↑n✝ + 1) * 4 ≤ (↑n✝ + 1 + 1) * 12
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)

Tactic:
rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]

Goal state after:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ 2 < 4
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ ((algebraMap ℝ ℂ) (2 * sin (↑q * π)))

Tactic:
by
    simp [Complex.isIntegral_two_mul_sin_rat_mul_pi]

Goal state after:
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‖
l : ↥L.lattice
h : ¬↑l = l₀
⊢ ↑l ≠ x

Tactic:
by simpa [sub_eq_zero] using (norm_nonneg _).trans_lt (hx l h)

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ x = cos (↑k * π / ↑n)

Tactic:
convert! congr(cos ($hk.symm / n))

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ x = cos (↑n * arccos x / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ ↑n)| = 1 → ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
intro hTx
    have hx := (abs_eval_T_real_le_one_iff (Nat.cast_ne_zero.mpr hn) x).mpr (le_of_eq hTx)
    rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx
    obtain ⟨k, hk⟩ := hTx
    have hk' : k = n * (arccos x / π) := by simpa [field]
    lift k to ℕ using (by rw [← Int.cast_nonneg_iff (R := ℝ), hk']; positivity [arccos_nonneg x])
    simp only [Int.cast_natCast] at hk hk'
    have hkn : (k : ℝ) ≤ n := by
      rw [← mul_one (n : ℝ), hk']
      gcongr
      exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)
    refine ⟨k, by simpa using hkn, ?_⟩
    convert! congr(cos ($hk.symm / n))
    rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]

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

Goal state before:
pp: case pos
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : Odd i
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

Tactic:
simpa [← CharZero.eq_neg_self_iff, hi₂, (show Even 6 by decide).neg_pow] using!
      (iteratedDeriv_comp_neg i (L.relation * id ^ 6) 0 :)

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

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

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

Goal state after:
case inl
n : ℕ
⊢ fib ↑n = 0 ↔ ↑n = 0

case inr
n : ℕ
⊢ fib (-↑n) = 0 ↔ -↑n = 0
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
by rw [fib_natCast_add]; grind

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

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

Tactic:
by rw [fib_natCast_add]; grind

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

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

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

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

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

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

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

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

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

Goal state before:
pp: case inr
n : ℤ
m : ℕ
⊢ (fib (-↑m)).gcd (fib n) = Nat.fib ((-↑m).gcd n)

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

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

case inr.inr
m n : ℕ
⊢ (fib (-↑m)).gcd (fib (-↑n)) = Nat.fib ((-↑m).gcd (-↑n))
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ| < φ

Tactic:
abs_lt

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ -φ < ψ ∧ ψ < φ
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑(fib (n + 1)) / ↑(fib n)) atTop (𝓝 φ)

Tactic:
show φ = (φ - ψ * 0) / (1 - 0) by ring,

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑(fib (n + 1)) / ↑(fib n)) atTop (𝓝 ((φ - ψ * 0) / (1 - 0)))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℤ
⊢ ↑(Int.fib n) = (φ ^ n - ψ ^ n) / √5

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

Goal state after:
case inl
n : ℕ
⊢ ↑(Int.fib ↑n) = (φ ^ ↑n - ψ ^ ↑n) / √5

case inr
n : ℕ
⊢ ↑(Int.fib (-↑n)) = (φ ^ (-↑n) - ψ ^ (-↑n)) / √5
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
by
  simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left]
  refine iteratedDerivWithin_congr (fun z hz ↦ ?_) hz
  simpa [cotTerm] using (cot_series_rep' (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z = (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
have h0 := iteratedDerivWithin_cot_pi_mul_sub_inv k hz
  rw [iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum hk hz, add_comm] at h0
  rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0]
  ring

Goal state after:
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
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      colimit.ι (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
rw [ι_preservesColimitIso_inv_assoc]

Goal state after:
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
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j) ≫
        (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

pp: case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

pp: case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2

Tactic:
rotate_left

Goal state after:
case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2

case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)⟩ =
    {
        obj :=
          min (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
            (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case eq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')⟩ =
    { obj := eq g g', property := ⋯ }.obj

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (a : A), IsConnected (StructuredArrow (L.obj a) R)
this✝² : ∀ (a : Aᵒᵖ), IsConnected (CostructuredArrow R.op (L.op.obj a))
this✝¹ : (snd R.op L.op).Initial
this✝ : ((opFunctor L R).leftOp ⋙ snd R.op L.op).Initial
this : (fst L R).op.Initial
⊢ (fst L R).Final

Tactic:
apply final_of_initial_op

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
⊢ IsFiltered (CostructuredArrow yoneda (colimit F))

Tactic:
refine IsFiltered.iff_nonempty_limit.mpr (fun {J _ _} G => ?_)
  -- We begin by remarking that `lim Hom_{Over (colimit F)}(yG·, 𝟙 (colimit F))` is nonempty,
  -- simply because `𝟙 (colimit F)` is the terminal object. Here `y` is the functor
  -- `CostructuredArrow yoneda (colimit F) ⥤ Over (colimit F)` induced by `yoneda`.
  have h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver _ _).op ⋙
      yoneda.obj (Over.mk (𝟙 (colimit F))))) :=
    ⟨Types.Limit.mk _ (fun j => Over.mkIdTerminal.from _) (by simp)⟩
  -- `𝟙 (colimit F)` is the colimit of the diagram in `Over (colimit F)` given by the arrows of
  -- the form `Fi ⟶ colimit F`. Thus, pulling the colimit out of the hom functor and commuting
  -- the finite limit with the filtered colimit, we obtain
  -- `lim_j Hom_{Over (colimit F)}(yGj, 𝟙 (colimit F)) ≅`
  --   `colim_i lim_j Hom_{Over (colimit F)}(yGj, colimit.ι F i)`, and so we find `i` such that
  -- the limit is non-empty.
  obtain ⟨i, hi⟩ := exists_nonempty_limit_obj_of_isColimit F G _
    (colimit.isColimitToOver F) _ (Iso.refl _) h₁
  -- `F.obj i` is a small filtered colimit of representables, say of the functor `H : K ⥤ C`, so
  -- `𝟙 (F.obj i)` is the colimit of the arrows of the form `yHk ⟶ Fi` in `Over Fi`.
  -- Then `colimit.ι F i` is the colimit of the arrows of the form
  -- `H.obj F ⟶ F.obj i ⟶ colimit F` in `Over (colimit F)`.
  obtain ⟨⟨P⟩⟩ := hF i
  let hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
    isColimitOfPreserves (Over.map _) (Over.isColimitToOver P.coconeIsColimit)
  -- Again, we pull the colimit out of the hom functor and commute limit and colimit to obtain
  -- `lim_j Hom_{Over (colimit F)}(yGj, colimit.ι F i) ≅`
  --   `colim_k lim_j Hom_{Over (colimit F)}(yGj, yHk)`, and so we find `k` such that the limit
  -- is non-empty.
  obtain ⟨k, hk⟩ : ∃ k, Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
      yoneda.obj ((CostructuredArrow.toOver yoneda (colimit F)).obj <|
        (CostructuredArrow.pre P.F yoneda (colimit F)).obj <|
          (map (colimit.ι F i)).obj <| mk _))) :=
    exists_nonempty_limit_obj_of_isColimit F G _ hc _ (Iso.refl _) hi
  have htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful := .ofFullyFaithful _
  -- Since the inclusion `y : CostructuredArrow yoneda (colimit F) ⥤ Over (colimit F)` is fully
  -- faithful, `lim_j Hom_{Over (colimit F)}(yGj, yHk) ≅`
  --   `lim_j Hom_{CostructuredArrow yoneda (colimit F)}(Gj, Hk)` and so `Hk` is the object we're
  -- looking for.
  let q := fun X => isoWhiskerLeft _ (uliftYonedaIsoYoneda.symm.app _) ≪≫ htO.homNatIso X
  obtain ⟨t'⟩ := Nonempty.map (limMap (isoWhiskerLeft G.op (q _)).hom) hk
  exact ⟨_, ⟨((preservesLimitIso uliftFunctor.{max u v, v} _).inv t').down⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this✝² : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
this✝¹ : (fst R.op L.op).Initial
this✝ : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial
this : (snd L R).op.Initial
⊢ (snd L R).Final

Tactic:
apply final_of_initial_op

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
⊢ X.right ⟶ ((Comma.map α β).obj { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom }).right

Tactic:
by exact Y.right.hom

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
⊢ Injective ((preadditiveCoyonedaObj G).obj B)

Tactic:
rw [← Module.injective_iff_injective_object]

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)ᵐᵒᵖ ↑((preadditiveCoyonedaObj G).1 B)
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
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:
· exact IsZero.projective (CochainComplex.isZero_of_isStrictlyLE _ 0 _)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ R.cochainComplex.IsGE 0

Tactic:
simp only [HomologicalComplex.isSupported_iff_of_quasiIso R.π']

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ HomologicalComplex.IsSupported ((CochainComplex.singleFunctor C 0).obj X) (ComplexShape.embeddingUpIntGE 0)