mathlib-initiative/mathlib-tactics huggingface dataset:
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‖
⊢ ∃ κ, 1 < κ ∧ ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖

Tactic:
obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_const ‖z - x‖).isOpen_preimage _
      (isClosedMap_dist x _
      (L.isClosed_of_subset_lattice (Set.sdiff_subset (t := {l₀})))).upperClosure.isOpen_compl) 1
      (by simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx)

Goal state after:
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₀}))))ᶜ
⊢ ∃ κ, 1 < κ ∧ ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ rexp (4 * ↑n) * ((2 * ↑n) ^ (2 * n)) ^ 2 = (↑n ^ n) ^ 4 * rexp (2 * (2 * ↑n)) * 2 ^ (4 * n)

Tactic:
ring_nf

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ sin (↑n * π) - sin 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp [Nat.le_zero.mp hi]
  have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (node n i - node n j)) :=
    Finset.prod_pos (fun j hj => mul_pos_of_neg_of_neg neg_one_lt_zero <| sub_neg.mpr <|
    node_lt hi (Finset.mem_range.mp hj))
  rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range] at h₁
  have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j) :=
    Finset.prod_pos (fun j hj => sub_pos.mpr <|
      node_lt (Finset.mem_Ioc.mp hj).2 (Finset.mem_Ioc.mp hj).1)
  have union : (Finset.range (n + 1)).erase i = (Finset.range i) ∪ Finset.Ioc i n := by grind
  have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n) := by grind [Finset.disjoint_iff_ne]
  rw [union, Finset.prod_union disjoint, ← mul_assoc]
  exact mul_pos h₁ h₂

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
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 : ℂ
κ : ℝ
hκ : 1 < κ
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - ↑p.2‖ < ‖↑l - ↑p.2‖
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - ↑p.2‖ * κ < ‖↑l - ↑p.2‖
H₂ : Summable fun l ↦ ‖↑l - ↑p.2‖ ^ (-3) * ‖z - ↑p.2‖
h : ‖↑p.2 - ↑p.2‖ = 0
⊢ False

Tactic:
simpa [(norm_nonneg _).not_gt] using hx p.2 hp

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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 1 + 1‖ * ‖↑p.2 - x‖ ^ (-2 + (-1 + -↑p.1)) = ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) ∨ z - x = 0

Tactic:
ring_nf

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ True ∨ -x + z = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ≤ n
this : 0 < ((-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i

Tactic:
rwa [mul_inv, ← inv_pow, inv_neg_one] at this

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

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ MeromorphicAt ℘[L] x

Tactic:
simp_rw [← funext <| L.weierstrassPExcept_add ⟨x, hx⟩]

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ MeromorphicAt (fun x_1 ↦ ℘[L - x] x_1 + (1 / (x_1 - x) ^ 2 - 1 / x ^ 2)) x
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ (fun n ↦ ((↑n * z + ↑d) ^ k)⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ ↑k)⁻¹

Tactic:
lift k to ℕ using (by lia)

Goal state after:
z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : 2 ≤ ↑k
⊢ (fun n ↦ ((↑n * z + ↑d) ^ ↑k)⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ ↑↑k)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1

Tactic:
ring_nf

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

Goal state before:
pp: z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))

Tactic:
ring_nf

Goal state after:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * I * 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I) + z * (I * 2))

Tactic:
ring_nf

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

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
unfold arithGeom; grind

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

Goal state before:
pp: z : ℂ
⊢ (cexp (2 * I * (↑π * z)) + 1) / (I * (1 - cexp (2 * I * (↑π * z)))) =
    (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))

Tactic:
ring_nf

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ logDeriv (Complex.sin ∘ fun t ↦ ↑π * t) x - logDeriv (HMul.hMul ↑π) x = ↑π * (↑π * x).cot - 1 / x

pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0

Tactic:
logDeriv_comp (Complex.differentiableAt_sin) (by fun_prop),

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ logDeriv Complex.sin (↑π * x) * deriv (fun t ↦ ↑π * t) x - logDeriv (HMul.hMul ↑π) x = ↑π * (↑π * x).cot - 1 / x

x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = ∑ i ∈ f.support, eval y (f i • i)

Tactic:
simp_rw [Polynomial.eval_smul]

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

Goal state before:
pp: x✝ : ℕ
⊢ fib (-↑x✝ + -↑1) = fib (-↑x✝ - 1) * fib (-↑1) + fib (-↑x✝) * fib (-↑1 + 1)

Tactic:
simp [sub_eq_neg_add, add_comm]

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

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

Tactic:
ring_nf

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

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

Tactic:
rw [abs_div, div_lt_one <| by positivity, abs_of_pos goldenRatio_pos, abs_lt]
    ring_nf
    bound

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

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖((↑n + 1) ^ ↑(1 + k))⁻¹‖

Tactic:
zpow_natCast

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖((↑n + 1) ^ (1 + k))⁻¹‖
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n

Tactic:
ring_nf

Goal state after:
n : ℕ
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
nz : √5 ≠ 0
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
rw [← (mul_inv_cancel₀ nz).symm, one_mul]

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

Goal state before:
pp: case succ
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * ↑(Nat.fib (n + 1 + 1)) + ↑(Nat.fib (n + 1)) = φ ^ (n + 1 + 1)

Tactic:
calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

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

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) +
      (-1) ^ k * ↑k ! * (∑' (b : ℕ), (z + (↑b + 1)) ^ (-1 - ↑k) + ∑' (b : ℕ), (z - (↑b + 1)) ^ (-1 - ↑k)) =
    (-1) ^ k * ↑k ! *
      (∑' (n : ℕ), (z + (↑n + 1)) ^ (-1 - ↑k) + (z + 0) ^ (-1 - ↑k) + ∑' (n : ℕ), (z + -(↑n + 1)) ^ (-1 - ↑k))

Tactic:
ring_nf

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
h : N < a + 1
⊢ N ∈ range (a + 1)

Tactic:
exact mem_range.2 h

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

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

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

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

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ X ⊞ Y
hk : k ≫ φ f g = 0
⊢ (k ≫ biprod.fst) ≫ f ≫ g = 0

Tactic:
obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_to k
      simp only [biprod.ext_to_iff, add_comp, assoc, inl_φ, BinaryBicone.inl_fst,
        comp_id, inr_φ_fst, comp_neg, zero_comp, BinaryBicone.inl_snd, comp_zero, φ_snd,
        BinaryBicone.inr_snd_assoc, zero_add, add_neg_eq_zero] at hk
      obtain ⟨rfl, hk⟩ := hk
      aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ X ⊞ Y
hk : k ≫ φ f g = 0
⊢ kernel.lift (f ≫ g) (k ≫ biprod.fst) ⋯ ≫ ι f g = k

Tactic:
obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_to k
      simp only [biprod.ext_to_iff, add_comp, assoc, inl_φ, BinaryBicone.inl_fst,
        comp_id, inr_φ_fst, comp_neg, zero_comp, BinaryBicone.inl_snd, comp_zero, φ_snd,
        BinaryBicone.inr_snd_assoc, zero_add, add_neg_eq_zero] at hk
      obtain ⟨rfl, hk⟩ := hk
      aesop

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x

Tactic:
suffices ∑ i ∈ .Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ x in a..a + ↑(b - a), f x by simp_all
  simp_rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range, add_assoc]
  suffices ∑ x ∈ .range (b - a), f (a + ↑(x + 1)) ≤ ∫ x in a..a + ↑(b - a), f x by simp_all
  exact AntitoneOn.sum_le_integral (by simp [hf, hab])

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
h : N < a + 1
⊢ N ∈ range (a + 1)

Tactic:
exact mem_range.2 h

Goal state after:
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
hh : factorThruImage (h ≫ f) = 0
⊢ h ≫ f = 0

Tactic:
rw [← Limits.image.fac (h ≫ f), hh, zero_comp]

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
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f

Tactic:
obtain ⟨p, _⟩ := hG₂ X

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
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
p : G ⟶ F.obj X
h✝ : Epi p
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f
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
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
refine exists_nonempty_limit_obj_of_colimit F G H ?_
  suffices T ≅ colimit H from Nonempty.map (lim.map (whiskerLeft 𝒢 (yoneda.map this.hom))) h
  refine hT.symm ≪≫ IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ ((ConcreteCategory.hom (𝟙 (ULift.{u, v} (G.obj (op (F.obj (unop i)))))))
        ((ConcreteCategory.hom (limit.π (F.op ⋙ G ⋙ uliftFunctor.{u, v}) i))
          ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))

Tactic:
erw [colimitYonedaHomIsoLimitOp_π_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
i₀ : I s
f₀ g₀ : k s ⟶ i₀
h₀ :
  (hom ((F s).map f₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
    (hom ((F s).map g₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ (hom ((F s).map (f₀ ≫ IsFiltered.coeqHom f₀ g₀))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
    (hom ((F s).map (f₀ ≫ IsFiltered.coeqHom f₀ g₀))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
conv_rhs => rw [IsFiltered.coeq_condition]

Goal state after:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
i₀ : I s
f₀ g₀ : k s ⟶ i₀
h₀ :
  (hom ((F s).map f₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
    (hom ((F s).map g₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ (hom ((F s).map (f₀ ≫ IsFiltered.coeqHom f₀ g₀))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
    (hom ((F s).map (g₀ ≫ IsFiltered.coeqHom f₀ g₀))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ ∀ b ∈ (Opposite.unop S).attach, b ≠ v → Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

Tactic:
intro b hb hb₁
    rw [Pi.ι_π_of_ne _ hb₁, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
x✝³ x✝² x✝¹ : C
f : x✝³ ⟶ x✝¹
g : x✝² ⟶ x✝¹
x✝ : Limits.HasPullback f g
hf : epimorphisms C g
⊢ epimorphisms C (Limits.pullback.fst f g)

Tactic:
simp only [epimorphisms.iff] at hf ⊢
    infer_instance

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
⊢ Function.Surjective (pseudoApply f) → Epi f

Tactic:
intro h
  have ⟨pbar, hpbar⟩ := h (𝟙 Q)
  have ⟨p, hp⟩ := Quotient.exists_rep pbar
  have : (⟦(p.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(𝟙 Q)⟧ := by
    rw [← hp] at hpbar
    exact hpbar
  have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this
  apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey
  dsimp at comm
  rw [Category.assoc, comm]
  apply Category.comp_id

Goal state after: