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

Goal state before:
pp: P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x ∈ Ico x₀ (r ^ (⌊logb r (x / x₀)⌋₊ + 1) * x₀)

Tactic:
rw [mem_Ico, ← div_lt_iff₀ hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add,
      Nat.cast_one]

Goal state after:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x₀ ≤ x ∧ logb r (x / x₀) < ↑⌊logb r (x / x₀)⌋₊ + 1
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegular

Tactic:
by
  suffices P.InnerRegularCompactLTTop from inferInstance
  refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
  · exact innerRegularWRT_isCompact_isOpen P
  · exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
⊢ μ.InnerRegularCompactLTTop

Tactic:
constructor
  intro A ⟨hA1, hA2⟩ r hr
  have := Fact.mk hA2.lt_top
  have hA2' : (μ.restrict A) A ≠ ⊤ := by
    rwa [Measure.restrict_apply_self]
  have hr' : r < μ.restrict A A := by
    rwa [Measure.restrict_apply_self]
  obtain ⟨K, ⟨hK1, hK2, hK3⟩⟩ := MeasurableSet.exists_lt_isCompact_of_ne_top hA1 hA2' hr'
  use K, hK1, hK2
  rwa [Measure.restrict_eq_self μ hK1] at hK3

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
⊢ a ∈ Set.Ioi (↑(n + 1) - 1) →
    ∀ ⦃b : ℝ⦄,
      b ∈ Set.Ioi (↑(n + 1) - 1) →
        a ≤ b →
          deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
            deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b

Tactic:
ha

Goal state after:
case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : a ∈ Set.Ioi (↑(n + 1) - 1)
⊢ ∀ ⦃b : ℝ⦄,
    b ∈ Set.Ioi (↑(n + 1) - 1) →
      a ≤ b →
        deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
          deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
have : s ≠ ↑l := by rintro rfl; linarith

Goal state after:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this : s ≠ l
⊢ ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)
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
⊢ ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

Tactic:
have : 0 < ‖l‖ := by linarith

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ a.card = ↑n ^ (b.card + 1) * ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
← zpow_natCast,

Goal state after:
case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ (b.card + 1) * ↑n ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ (b.card + 1) * ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
← zpow_natCast,

Goal state after:
case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ ↑(b.card + 1) * ↑n ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ (↑n ^ (b.card + 1 - a.card))⁻¹ = ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
← zpow_natCast,

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ (↑n ^ ↑(b.card + 1 - a.card))⁻¹ = ↑n ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2) l - 0

Tactic:
← zpow_natCast,

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ ↑3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ ↑2) l - 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ (↑L.lattice \ {l₀ - ↑l}).Countable

Tactic:
exact .mono sdiff_le (countable_of_Lindelof_of_discrete (X := L.lattice))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ 0 < x.sigmoid

Tactic:
change 0 < (1 + exp (-x))⁻¹
  positivity

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L - -(l₀ - ↑l)] (↑l / 2) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)

Tactic:
L.weierstrassPExcept_def ⟨_, neg_mem (sub_mem hl₀ l.2)⟩,

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L] (↑l / 2) + (1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioc a b)] deriv f

Tactic:
rw [← restrict_Ioo_eq_restrict_Ioc]

Goal state after:
case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖((↑l - x) ^ r)⁻¹‖ ≤ ‖↑l - x‖ ^ (-↑r)

Tactic:
← zpow_natCast,

Goal state after:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖((↑l - x) ^ ↑r)⁻¹‖ ≤ ‖↑l - x‖ ^ (-↑r)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioc a b)] deriv f

Tactic:
rw [← restrict_Ioo_eq_restrict_Ioc]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (2 * ↑(n + 1) + 1)⁻¹ ^ 2 < 1

Tactic:
inv_pow

Goal state after:
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ ((2 * ↑(n + 1) + 1) ^ 2)⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: 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

Tactic:
have := (analyticOnNhd_weierstrassPExcept L x x (by simp)).meromorphicAt

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
this : MeromorphicAt ℘[L - x] x
⊢ 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: c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z + ↑d + ↑e) =Θ[cofinite] fun n ↦ ↑n

Tactic:
apply IsTheta.add_isLittleO <;>
  [refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real); skip] <;>
  simpa [-Int.cofinite_eq] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real

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

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

Tactic:
by
  wlog! hn : n ≠ 0
  · simp [hn]
  refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
  · obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
    rw [← hx, T_real_cos, cos_eq_zero_iff]
    use k
    field_simp
    norm_cast
  · rw [Finset.card_image_of_injOn, Finset.card_range, degree_T, Int.natAbs_natCast]
    exact (Finset.range n).nodup_map_iff_injOn.mp (roots_T_real_nodup n)

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

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < cos 0

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

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

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < cos 0

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

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

Goal state before:
pp: Z : Set ℂ
hZC : IsCompact Z
⊢ MultipliableUniformlyOn (fun n z ↦ 1 + sineTerm z n) Z

Tactic:
by
  obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC
  refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_
  · filter_upwards with n z hz using hu2 n z hz
  · fun_prop

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

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

Tactic:
· exact fib_neg_natCast_add_neg_natCast _ _

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j

Tactic:
rw [logDeriv_prod]

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j

case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
· apply exp_nonneg

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
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)

Tactic:
ha

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 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)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (generator F)

Tactic:
by
  apply isSeparator_sigma_of_isSeparator _ Classical.ofNonempty
  apply isSeparator_sigma_of_isSeparator _ 0
  exact isSeparator_projectiveSeparator

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
by
    obtain ⟨h⟩ := nonempty_isColimit fun i : ι ↦ hc (e i)
    constructor
    apply IsColimit.equivOfNatIsoOfIso _ _ _ _ <|
        h.whiskerEquivalence (Pi.equivalenceOfEquiv J e).symm
    · exact (Pi.equivalenceOfEquivCompPointwiseProduct F e)
    · -- Without the double `symm`, one runs into DTT hell
      exact (Cocone.ext (Pi.whiskerEquiv e fun _ ↦ Iso.refl _).symm).symm

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
A B : C
f : (preadditiveCoyonedaObj G).obj A ⟶ (preadditiveCoyonedaObj G).obj B
this : Epi (Sigma.desc fun f ↦ f)
h : (kernel.ι (Sigma.desc fun m ↦ m) ≫ Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) = 0
q : ↑((preadditiveCoyonedaObj G).obj A)
⊢ (ModuleCat.Hom.hom
        ((preadditiveCoyonedaObj G).map
          (epiDesc (Sigma.desc fun m ↦ m) (Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) h)))
      q =
    (ModuleCat.Hom.hom f) q

Tactic:
simpa [-comp_epiDesc] using! Sigma.ι _ q ≫= comp_epiDesc _ _ h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ I.iso.inv ≫ (injectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv

Tactic:
by
  rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]

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

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) (n✝ + 1)

Tactic:
quasiIsoAt_iff_exactAt

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n✝ + 1)

case succ.hK
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj Z) (n✝ + 1)
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) (n✝ + 1)

Tactic:
rw [quasiIsoAt_iff_exactAt]

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n✝ + 1)

case succ.hK
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj Z) (n✝ + 1)
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y Z : C
i : X ⟶ Y
hi : IsIso i
f : Y ⟶ Z
hY : P Y
hZ : Q Z
⊢ ofObjectProperty P Q (i ≫ f)

Tactic:
exact ⟨(P.prop_iff_of_isIso i).mpr hY, hZ⟩

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
X : C
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.toRightDerivedZero.app X =
    I.toRightDerivedZero' F ≫
      (CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom ≫
        (I.isoRightDerivedObj F 0).inv

Tactic:
dsimp [Functor.toRightDerivedZero, 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
X : C
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) =
    I.toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Mono (L.map f)
⊢ L.map (kernel.ι f) = 0

Tactic:
← cancel_mono (L.map f),

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
f : X ⟶ Y
this : L.EssSurj
x✝ : Mono (L.map f)
⊢ L.map (kernel.ι f) ≫ L.map f = 0 ≫ L.map f
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ Function.LeftInverse (fun f ↦ ⇑(ConcreteCategory.hom f)) fun f ↦ ↾f

Tactic:
by intro; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ Function.RightInverse (fun f ↦ ⇑(ConcreteCategory.hom f)) fun f ↦ ↾f

Tactic:
by intro; rfl

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map (X✝.ρ g) ≫ F.map f.hom = F.map f.hom ≫ F.map (Y✝.ρ g)

Tactic:
rw [← F.map_comp, f.comm, F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: case refine_2
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ ↑((h X).desc' s.π ⋯) = s.π

Tactic:
apply ((h X).desc' s.π _).2

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g ≫ η F = η F ≫ (𝟙_ (Action W G)).ρ g

Tactic:
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
        rw [map_id, Category.id_comp, Category.comp_id]

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
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.leftToRight.app X)

Tactic:
mono_leftToRight_app_iff_mono_adj₂_unit_app

Goal state after:
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
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.adj₂.unit.app (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)) ▷ h ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      eqToHom ⋯

Tactic:
comp_whiskerRight

Goal state after:
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      eqToHom ⋯