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

Goal state before:
pp: p : ℝ
⊢ binEntropy p = log 2 ↔ p = 2⁻¹

Tactic:
by
  rw [← binEntropy_le_log_two.not_lt_iff_eq, binEntropy_lt_log_two, not_ne_iff]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑(b ^ k) / ↑(b ^ i) * ↑(a ^ i)) = ↑(p.coeff i) * ↑(a ^ i) * ↑b ^ (k - i)

Tactic:
← pow_sub_mul_pow b ik,

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑(b ^ (k - i) * b ^ i) / ↑(b ^ i) * ↑(a ^ i)) = ↑(p.coeff i) * ↑(a ^ i) * ↑b ^ (k - i)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ StrictMono eulerMascheroniSeq

Tactic:
refine strictMono_nat_of_lt_succ (fun n ↦ ?_)

Goal state after:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
⊢ x ^ p = (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x

Tactic:
case inr =>
    have : ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 ≠ 0 :=
      ne_of_gt <| integral_rpowIntegrand₀₁_one_pos hp
    rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹

Tactic:
simp_rw [mul_div_assoc, mul_inv]

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * ((s - 1).Gammaℝ⁻¹ * ((s - 1) / 2 / ↑π)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
exact (hμ r hr').2

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ clog b r

Tactic:
clog_of_right_le_zero _ hr,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
cases hb

Goal state after:
case neg.inl
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 0
⊢ ⌊logb (↑b) r⌋ = Int.log b r

case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌊logb (↑b) r⌋ = Int.log b r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
cases hb

Goal state after:
case neg.inl
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 0
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ x ∈ t, w x * ↑((p x).descFactorial n)

Tactic:
exact descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ ε / 4 + dist ((1 - ε / 4) • x) x = ε / 4 + ε / 4

Tactic:
simp [sub_smul, norm_smul, hx, abs_of_pos hε]

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

Goal state before:
pp: case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ eval (cos θ) (U ℂ (-↑n - 1)) * sin θ = sin ((↑(-↑n - 1) + 1) * θ)

Tactic:
simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
    push_cast
    ring_nf

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

Goal state before:
pp: case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
have : 1 - x ^ 2 < 0 := by nlinarith [h₂]

Goal state after:
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Tactic:
rcases eq_or_ne x 1 with (rfl | h')
  · convert! (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _ <;>
      simp +contextual [arcsin_of_one_le]
  · exact (hasDerivAt_arcsin h h').hasDerivWithinAt

Goal state after:
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:
exact inv_lt_one_of_one_lt₀ (one_lt_pow₀ (lt_add_of_pos_left _ <| by positivity) two_ne_zero)

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ (fun n ↦ Icc (-↑n) ↑n) m ⊆ (fun n ↦ Icc (-↑n) ↑n) n

Tactic:
apply Icc_subset_Icc <;> simpa using Nat.mono_cast hmn

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:
simpa [sub_eq_zero] using (norm_nonneg _).trans_lt (hx l h)

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

Goal state before:
pp: case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ Tendsto (fun n ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * ↑r ^ n) atTop (𝓝 0)

Tactic:
convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i

Goal state after:
case e'_3
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
i : ℕ
⊢ ‖L.weierstrassPExceptSeries l₀ x i‖ * ↑r ^ i =
    ((fun a ↦ ‖a‖) ∘ fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + ↑↑r - x) ^ i) i

case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ 0 = ‖0‖

case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖x + ↑↑r - x‖ < ‖↑l - x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z

Tactic:
simpa using (contDiffOn_inv_linear k (d + 1)).contDiffAt
      (isOpen_compl_range_intCast.mem_nhds hz)

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u ((k + 1) * n + r) = u (n + (k * n + r))

Tactic:
by congr 1; ring

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

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)

Tactic:
simp_rw [sub_eq_add_neg]
  rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]
  · simpa [iteratedDerivWithin_fun_neg] using! iteratedDerivWithin_one_div k
      isOpen_upperHalfPlaneSet hz
  · exact ContDiffWithinAt.mul (by fun_prop) (cot_pi_mul_contDiffWithinAt k
      (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))
  · simp only [one_div]
    apply ContDiffWithinAt.neg
    exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩)

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
⊢ 2 ^ (-(c * ↑i)) = rexp (-(log 2 * c) * ↑i)

Tactic:
conv_lhs => rw [← exp_log zero_lt_two, ← exp_mul]

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
⊢ rexp (log 2 * -(c * ↑i)) = rexp (-(log 2 * c) * ↑i)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
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)
c : ℕ → ℕ
left✝ : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ 2 * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
this : Tendsto (fun n ↦ u 0 / ↑(c n)) atTop (𝓝 0)
n : ℕ
⊢ u 0 ≤ u (c n)

Tactic:
exact hmono zero_le

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

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

Tactic:
exact isLimit f g

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
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
L : Tendsto (fun ε ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 l)
⊢ ∃ ε, l + ε * (1 + ε + l) < d ∧ 0 < ε

Tactic:
exact (((tendsto_order.1 L).2 d hd).and self_mem_nhdsWithin).exists

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j

Tactic:
rw [← this]

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
⊢ (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j
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ᵒᵖ
⊢ (ConcreteCategory.hom (limit.π (F.op ⋙ G) i))
      ((ConcreteCategory.hom (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).symm.hom)
          ((ConcreteCategory.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom)
            ((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:
have (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) := congrArg ULift.down
    (ConcreteCategory.congr_hom (preservesLimitIso_inv_π uliftFunctor.{u, v} (F.op ⋙ G) i) a)

Goal state after:
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 (limit.π (F.op ⋙ G) i))
      ((ConcreteCategory.hom (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).symm.hom)
          ((ConcreteCategory.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom)
            ((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))))
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ ((colimitHomIsoLimitYoneda F A).inv ≫ ↾fun g ↦ colimit.ι F i ≫ g) = limit.π (F.op ⋙ yoneda.obj A) (op i)

Tactic:
by
  rw [← dsimp% colimitHomIsoLimitYoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

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
inst✝ : Injective Z
n : ℕ
⊢ Injective (((single₀ C).obj Z).X n)

Tactic:
by
    cases n
    · simpa
    · apply IsZero.injective
      apply HomologicalComplex.isZero_single_obj_X
      simp

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
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach,
      h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun a ↦ G) x ≫ (ModuleCat.Hom.hom f) (↑x).as =
    0

Tactic:
suffices ∑ x ∈ F.attach, r x • f.hom x.1.as = 0 by simpa [End.smul_left, r] using this

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
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach, r x • (ModuleCat.Hom.hom f) (↑x).as = 0
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
this✝ : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
this : (tensorObj G).PreservesMonomorphisms
⊢ PreservesFiniteLimits (tensorObj G)

Tactic:
have : PreservesBinaryBiproducts (tensorObj G) :=
    preservesBinaryBiproducts_of_preservesBinaryCoproducts _

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
this✝¹ : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
this✝ : (tensorObj G).PreservesMonomorphisms
this : PreservesBinaryBiproducts (tensorObj G)
⊢ PreservesFiniteLimits (tensorObj G)
Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Radical C
⊢ IsZero (Φ.obj.quotient ⋙ Φ.obj.r)

Tactic:
rw [← Preradical.isRadical_iff_isZero, Preradical.isRadical_iff_isIso]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Radical C
⊢ IsIso (Φ.obj.toColon Φ.obj)
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)

Tactic:
obtain ⟨inv, hinv⟩ :=
      KernelFork.IsLimit.lift' (Φ.isLimitKernelForkObj X) ((colon Φ Ψ).ι.app X) (by
        rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp])
    dsimp at hinv
    refine ⟨inv, ?_, ?_⟩
    · simp [← cancel_mono (Φ.ι.app X), hinv]
    · simp [← cancel_mono ((Φ.colon Ψ).ι.app X), hinv]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯

Tactic:
simp only [extMk, Preadditive.add_comp]
  rw [Cocycle.fromSingleMk_add _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])]
  simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm (CohomologyClass.mk x)

Tactic:
obtain ⟨f, hf, rfl⟩ := Cocycle.fromSingleMk_surjective x n (by simp) m (by lia)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
f : X ⟶ R.cochainComplex.X ↑n
hf : f ≫ R.cochainComplex.d ↑n ↑m = 0
⊢ ∃ f_1,
    ∃ (hf_1 : f_1 ≫ R.cocomplex.d n m = 0),
      R.extMk f_1 m hm hf_1 = R.extEquivCohomologyClass.symm (CohomologyClass.mk (Cocycle.fromSingleMk f ⋯ ↑m ⋯ hf))
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 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
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
(F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.naturality

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 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
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)