mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : 2 ≤ n
x : ℝ
k : ℕ
hk : k ∈ Finset.Ioo 0 n
hx : x = cos (↑k * π / ↑n)
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x

Tactic:
hx

Goal state after:
case mpr
n : ℕ
hn : 2 ≤ n
x : ℝ
k : ℕ
hk : k ∈ Finset.Ioo 0 n
hx : x = cos (↑k * π / ↑n)
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x✝ : ℂ
hx : x✝ ∉ L.lattice
this : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x✝
x : ℂ
⊢ x ∈ (↑L.lattice)ᶜ → ℘'[L] x ^ 2 - 4 * ℘[L] x ^ 3 + L.g₂ * ℘[L] x + L.g₃ = L.relation x

Tactic:
hx

Goal state after:
L : PeriodPair
x✝ : ℂ
hx✝ : x✝ ∉ L.lattice
this : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x✝
x : ℂ
hx : x ∈ (↑L.lattice)ᶜ
⊢ ℘'[L] x ^ 2 - 4 * ℘[L] x ^ 3 + L.g₂ * ℘[L] x + L.g₃ = L.relation x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Set.Icc (-1) 1
k : ℕ
hk : k ≤ n
hx : x = cos (↑k * π / ↑n)
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x

Tactic:
hx

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Set.Icc (-1) 1
k : ℕ
hk : k ≤ n
hx : x = cos (↑k * π / ↑n)
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (cos (↑k * π / ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (fun x ↦ ‖x‖ ^ 2) Z
hs : ∀ a ∈ Z, ‖a‖ ^ 2 ≤ s
n : ℕ
x : ℂ
⊢ x ∈ Z → ‖x‖ ^ 2 / ‖↑n + 1‖ ^ 2 ≤ |s| / ‖↑n + 1‖ ^ 2

Tactic:
hx

Goal state after:
case refine_2
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (fun x ↦ ‖x‖ ^ 2) Z
hs : ∀ a ∈ Z, ‖a‖ ^ 2 ≤ s
n : ℕ
x : ℂ
hx : x ∈ Z
⊢ ‖x‖ ^ 2 / ‖↑n + 1‖ ^ 2 ≤ |s| / ‖↑n + 1‖ ^ 2
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
have := fib_add (n + 1) n

Goal state after:
n : ℤ
this : fib (n + 1 + n) = fib (n + 1 - 1) * fib n + fib (n + 1) * fib (n + 1)
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ↑π * (↑π * x).cot - 1 / x = ∑' (n : ℕ), (1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1)))

Tactic:
rw [HasSum.tsum_eq]

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ HasSum (fun n ↦ 1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1))) (↑π * (↑π * x).cot - 1 / x)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ ψ = (-φ)⁻¹

Tactic:
← neg_inv,

Goal state after:
⊢ ψ = -φ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: 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
⊢ ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ ↑a‖ ≤ cotTermUpperBound k A B hB n

Tactic:
simp only [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n a.im_pos, Complex.norm_mul,
    norm_pow, norm_neg, norm_one, one_pow, Complex.norm_natCast, one_mul, cotTermUpperBound,
    Int.reduceNeg, norm_zpow, Real.norm_eq_abs, two_mul, add_mul]

Goal state after:
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
⊢ ↑k ! * ‖(↑a + (↑n + 1)) ^ (-1 - ↑k) + (↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤
    ↑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))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ Summable fun n ↦ (x - (↑n + 1)) ^ (-1 - ↑k)

Tactic:
by
  apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by lia))).2).congr
  simp [← zpow_neg, sub_eq_add_neg]

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
x : ℝ
⊢ x ∈ Ioi 0 → 0 x ≤ x ^ (↑k + 1 - 1) * rexp (-(c * x))

Tactic:
hx

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 x ≤ x ^ (↑k + 1 - 1) * rexp (-(c * x))
Module: Mathlib.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:
by
  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.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hf
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
⊢ x ∈ Icc ↑0 ↑M → ∀ ⦃b : ℝ⦄, b ∈ Icc ↑0 ↑M → x ≤ b → (fun x ↦ x ^ k) x ≤ (fun x ↦ x ^ k) b

Tactic:
hx

Goal state after:
case hf
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc ↑0 ↑M
⊢ ∀ ⦃b : ℝ⦄, b ∈ Icc ↑0 ↑M → x ≤ b → (fun x ↦ x ^ k) x ≤ (fun x ↦ x ^ k) b
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hg
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
⊢ x ∈ Icc (↑0 - 1) (↑M - 1) →
    ∀ ⦃b : ℝ⦄, b ∈ Icc (↑0 - 1) (↑M - 1) → x ≤ b → (fun x ↦ rexp (-(c * x))) b ≤ (fun x ↦ rexp (-(c * x))) x

Tactic:
hx

Goal state after:
case hg
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc (↑0 - 1) (↑M - 1)
⊢ ∀ ⦃b : ℝ⦄, b ∈ Icc (↑0 - 1) (↑M - 1) → x ≤ b → (fun x ↦ rexp (-(c * x))) b ≤ (fun x ↦ rexp (-(c * x))) x
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
h : ∀ x ∈ S.commutant, e * (x * e) = x * e
x : H →L[ℂ] H
⊢ x ∈ S.commutant → e * (x * e) = e * x

Tactic:
hx

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
h : ∀ x ∈ S.commutant, e * (x * e) = x * e
x : H →L[ℂ] H
hx : x ∈ S.commutant
⊢ e * (x * e) = e * x
Module: Mathlib.CategoryTheory.Generator.Preadditive

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

Tactic:
by simpa only [Limits.comp_zero] using hf

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

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

Tactic:
by simpa only [Limits.comp_zero] using hf

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
⊢ x ∈ Ico ↑i ↑(i + 1) → f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
hx

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
⊢ x ∈ Ico ↑i ↑(i + 1) → f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
hx

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i
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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2

Tactic:
have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring

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

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc
  have A : (0 : ℝ) < c⁻¹ ^ 2 := sq_pos_of_pos (inv_pos.2 cpos)
  have B : c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹ := by
    rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]
    swap
    · exact sub_pos.2 (pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero)
    have : c ^ 3 = c ^ 2 * c := by ring
    simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]
    rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel₀ (sq_pos_of_pos cpos).ne', one_mul]
    simpa using pow_right_mono₀ hc.le one_le_two
  have C : c⁻¹ ^ 2 < 1 := pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero
  calc
    (∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
        ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 := by
      gcongr
      intro i hi
      simp only [mem_filter, mem_range] at hi
      simp only [hi.1, mem_Ico, and_true]
      apply Nat.floor_le_of_le
      apply le_of_lt
      rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
      exact Real.log_lt_log hj hi.2
    _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by
      simp [← pow_mul, mul_comm]
    _ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) :=
      geom_sum_Ico_le_of_lt_one (sq_nonneg _) C
    _ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) := by
      gcongr
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
    _ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 := by
      have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr

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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
this : EssentiallySmall.{max ?u.32 u, u, u} (CostructuredArrow yoneda A)
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
apply finallySmall_of_essentiallySmall

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ ((singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).symm ≪≫
          isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm).hom ≫
      Fork.ι (KernelFork.ofι (iCycles I.cocomplex 0) ⋯) =
    Fork.ι I.kernelFork

Tactic:
← cancel_epi (singleObjHomologySelfIso (ComplexShape.up ℕ) _ _).hom,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ (singleObjHomologySelfIso (ComplexShape.up ℕ) ?m.123 I.kernelFork.pt).hom ≫
      ((singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).symm ≪≫
            isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm).hom ≫
        Fork.ι (KernelFork.ofι (iCycles I.cocomplex 0) ⋯) =
    (singleObjHomologySelfIso (ComplexShape.up ℕ) ?m.123 I.kernelFork.pt).hom ≫ Fork.ι I.kernelFork

C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ ℕ
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

Tactic:
by
      have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb
      -- By exactness, `b` factors through `im f = ker g` via some `c`.
      obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'
      -- We compute the pullback of the map into the image and `c`.
      -- The pseudoelement induced by the first pullback map will be our preimage.
      use pullback.fst (Abelian.factorThruImage S.f) c
      -- It remains to show that the image of this element under `f` is pseudo-equal to `b`.
      apply Quotient.sound
      refine ⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩
      -- Now we can verify that the diagram commutes.
      calc
        𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫ pullback.fst _ _ ≫ S.f =
          pullback.fst _ _ ≫ S.f :=
          Category.id_comp _
        _ = pullback.fst _ _ ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f) := by
          rw [Abelian.image.fac]
        _ = (pullback.snd _ _ ≫ c) ≫ kernel.ι (cokernel.π S.f) := by
          rw [← Category.assoc, pullback.condition]
        _ = pullback.snd _ _ ≫ b.hom := by
          rw [Category.assoc]
          congr

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
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
⊢ pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g ⟦a⟧

Tactic:
obtain ⟨X, p', q', ep', _, comm'⟩ := Quotient.exact hh
          have : a'.hom ≫ g = 0 := by
            apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
            simpa using comm'
          apply Quotient.sound
          -- Can we prevent quotient.sound from giving us this weird `coe_b` thingy?
          change app g (a'' : Over P) ≈ app g a
          exact ⟨R, 𝟙 R, p, inferInstance, ep, by simp [a'', sub_eq_add_neg, this]⟩

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (NatTrans.rightDerived α n).app X =
    (P.isoRightDerivedObj F n).hom ≫
      (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedObj G n).inv

Tactic:
dsimp [NatTrans.rightDerived, isoRightDerivedObj]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.rightDerivedToHomotopyCategory α).app X) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b), ⋯.hom ≫ ⋯.hom = s.inl

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b), ⋯.hom ≫ ⋯.hom = s.inr

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b) (m : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s.pt),
    ⋯.hom ≫ m = s.inl → ⋯.hom ≫ m = s.inr → m = ⋯.hom

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)

Tactic:
apply IsReflexivePair.mk' _ _ _
  · apply (free T).map (T.η.app X.A)
  · ext
    dsimp
    rw [← Functor.map_comp, X.unit, Functor.map_id]
  · ext
    apply Monad.right_unit

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.adj₂.unit.app (F.obj X))

Tactic:
by
  rw [← leftToRight_app_map_adj₁_unit_app, mono_comp_iff_of_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a' ⟶ F.obj a
g : a ⟶ b
⊢ f ◁ Γ.app a ▷ G.map g ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ F.map g ◁ Γ.app b

Tactic:
by
  simp_rw [← whiskerLeft_comp, naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_have 1 → 2
  | h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift
  tfae_have 2 → 3
  | h => ⟨inferInstance, inferInstance⟩
  tfae_have 3 → 1
  | ⟨h, h'⟩ => .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u
  tfae_finish

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝ : Cat
⊢ ↾(𝟙 x✝).toFunctor.mapConnectedComponents = 𝟙 (ConnectedComponents ↑x✝)

Tactic:
by ext x; simpa using (Quotient.exists_rep x).elim (fun _ h ↦ by subst h; rfl)

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
xcc : (typeToCat ⋙ connectedComponents).obj x✝²
⊢ (ConcreteCategory.hom
          ((typeToCat ⋙ connectedComponents).map x✝ ≫
            ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝¹)) (𝟙 typeToCat.obj x✝¹).toFunctor)).toFun
      xcc =
    (ConcreteCategory.hom
          (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝²)) (𝟙 typeToCat.obj x✝²).toFunctor ≫
            (𝟭 (Type u)).map x✝)).toFun
      xcc

Tactic:
obtain ⟨x, h⟩ := Quotient.exists_rep xcc

Goal state after:
X : Type u
C : Cat
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
xcc : (typeToCat ⋙ connectedComponents).obj x✝²
x : ↑(typeToCat.obj x✝²)
h : ⟦x⟧ = xcc
⊢ (ConcreteCategory.hom
          ((typeToCat ⋙ connectedComponents).map x✝ ≫
            ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝¹)) (𝟙 typeToCat.obj x✝¹).toFunctor)).toFun
      xcc =
    (ConcreteCategory.hom
          (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝²)) (𝟙 typeToCat.obj x✝²).toFunctor ≫
            (𝟭 (Type u)).map x✝)).toFun
      xcc
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ F₁ = F₂

Tactic:
apply Functor.curry_obj_injective

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ curry.obj F₁ = curry.obj F₂
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
i : X₂ ≅ Y₂
⊢ (X₁ ◁ i.hom) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom ≫ X₁ ◁ i.inv ▷ X₃ = (α_ X₁ X₂ X₃).hom

Tactic:
by
  simp only [associator_naturality₂_assoc, ← whiskerLeft_comp, ← whiskerRight_comp,
    Iso.hom_inv_id, whiskerRight_id, whiskerLeft_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
⊢ g = χ'.base

Tactic:
by simpa using IsHomLift.fac (forget F) g χ'

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ (X Y : Grothendieck F), ∃ Z x x, True

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
· rintro ⟨c, f⟩ ⟨d, g⟩
    exact ⟨⟨max c d, max ((F.map (leftToMax c d)).toFunctor.obj f)
      ((F.map (rightToMax c d)).toFunctor.obj g)⟩,
      ⟨leftToMax c d, leftToMax _ _⟩, ⟨rightToMax c d, rightToMax _ _⟩, trivial⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h