mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
h_bnd : r ∈ Set.Icc 0 1
⊢ r ∈ {0, 1 / 3, 1 / 2, 2 / 3, 1}

Tactic:
apply smul_left_injective ℚ pi_ne_zero |>.mem_set_image.mp
  replace h_bnd : (r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π) := by
    obtain ⟨hr, hr'⟩ := h_bnd; constructor <;> gcongr <;> norm_cast
  generalize h : (r : ℝ) * π = θ at *
  have := niven_angle_eq ⟨r, h.symm⟩ hcos (by simpa using h_bnd)
  simp_all [Rat.smul_def]
  grind

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

Tactic:
simp [hP]

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P = T ℝ ↑n
⊢ P.leadingCoeff = 2 ^ (n - 1)

Tactic:
simp [hP]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
⊢ ↑‖x‖₊ = ↑(max (x 0).natAbs (x 1).natAbs)

Tactic:
← NNReal.coe_natCast,

Goal state after:
x : Fin 2 → ℤ
⊢ ↑‖x‖₊ = ↑↑(max (x 0).natAbs (x 1).natAbs)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

pp: case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
· simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]
    by_cases h : -k = 0
    · rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
    · rw [Real.zero_rpow h, mul_zero]

Goal state after:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.sumInvPow 0 = L.G

Tactic:
by
  ext; simp [sumInvPow, G]

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

Goal state before:
pp: case hf
n x : ℕ
hx : x ∈ ↑(Finset.range n)
⊢ ∀ ⦃x₂ : ℕ⦄,
    x₂ ∈ ↑(Finset.range n) → (fun k ↦ (↑k + 1) * π / (↑n + 1)) x = (fun k ↦ (↑k + 1) * π / (↑n + 1)) x₂ → x = x₂

Tactic:
y

Goal state after:
case hf
n x : ℕ
hx : x ∈ ↑(Finset.range n)
y : ℕ
⊢ y ∈ ↑(Finset.range n) → (fun k ↦ (↑k + 1) * π / (↑n + 1)) x = (fun k ↦ (↑k + 1) * π / (↑n + 1)) y → x = y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ cos ((↑k + 1) * π / (↑(n - 1) + 1)) = cos (↑(k + 1) * π / ↑n)

Tactic:
congr

Goal state after:
case mp.e_a.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ ↑k + 1 = ↑(k + 1)

case mp.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ ↑(n - 1) + 1 = ↑n
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k

Tactic:
congr

Goal state after:
case succ.e_a
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (1 + n), a ^ k
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
grind [fib_add_two]

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 (↑π * x) * deriv (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:
Complex.logDeriv_sin,

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ (↑π * x).cot * 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.Data.Int.Fib.Basic

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
grind [fib_add_two]

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

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

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

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

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

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

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

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

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

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

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

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

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

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

Tactic:
Real.coe_fib_eq'

Goal state after:
⊢ (fun n ↦ (φ ^ n - ψ ^ n) / √5) = fun n ↦ (φ ^ n - ψ ^ n) / √5
Module: Mathlib.Analysis.SumIntegralExpDecay

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

Tactic:
y

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

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

Tactic:
y

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

Goal state before:
pp: case mk
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
carrier✝ : Set (H →L[ℂ] H)
mul_mem'✝ : ∀ {a b : H →L[ℂ] H}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : H →L[ℂ] H},
    a ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    (algebraMap ℂ (H →L[ℂ] H)) r ∈
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
          zero_mem' := zero_mem'✝ }.carrier
star_mem'✝ :
  ∀ {a : H →L[ℂ] H},
    a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier →
      star a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier
centralizer_centralizer'✝¹ :
  { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
            algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝ }.carrier.centralizer.centralizer =
    { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
        algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝ }.carrier
toStarSubalgebra✝ : StarSubalgebra ℂ (H →L[ℂ] H)
centralizer_centralizer'✝ : toStarSubalgebra✝.carrier.centralizer.centralizer = toStarSubalgebra✝.carrier
h :
  (fun S ↦ S.carrier)
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
        zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝,
        centralizer_centralizer' := centralizer_centralizer'✝¹ } =
    (fun S ↦ S.carrier) { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
      algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝,
      centralizer_centralizer' := centralizer_centralizer'✝¹ } =
    { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }

Tactic:
congr

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 ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
by
  rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
  refine ⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩
  · exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyonedaObj P)
        (forget _)
  · intro
    exact (inferInstance : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
⊢ ∑ i ∈ Finset.range M, f ↑(i + (N + 1)) = ∑ n ∈ Finset.Ico N (N + M), f ↑(n + 1)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]; grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Set.Ici ↑N)
integrable : IntegrableOn f (Set.Ioi ↑N) volume
nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t
s : Finset ℕ
t : ℕ
ht : s ⊆ Finset.range t
⊢ ∑ i ∈ Finset.range t, f ↑(i + N + 1) = ∑ i ∈ Finset.Ico N (N + t), f ↑(i + 1)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]; grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case e'_3
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∑' (i : ℕ), f ↑(i + N) = ∑' (n : ℕ), f ↑(n + (N - 1) + 1)

Tactic:
congr

Goal state after:
case e'_3.e_f
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ (fun i ↦ f ↑(i + N)) = fun n ↦ f ↑(n + (N - 1) + 1)
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
⊢ PreservesFiniteLimits (embedding F)

Tactic:
by
  rw [embedding]
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
  infer_instance

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ StructuredArrow.map₂ u₂ iR.hom =
    StructuredArrow.map₂ ((𝟙 (L'.obj i₂) ≫ (𝟭 T').map u₂) ≫ (𝟭 T' ⋙ 𝟭 T').map (𝟙 (R'.obj j₂)))
      ((G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
        whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
          ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
            (𝟭 B).whiskerLeft
                (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                  whiskerRight iR.hom (𝟭 T') ≫
                    ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫
                      (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
              ((𝟭 B).associator (𝟭 B ⋙ R) H).inv)

Tactic:
congr

Goal state after:
case e_α
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ u₂ = (𝟙 (L'.obj i₂) ≫ (𝟭 T').map u₂) ≫ (𝟭 T' ⋙ 𝟭 T').map (𝟙 (R'.obj j₂))

case e_β
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ iR.hom =
    (G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
      whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
        ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
          (𝟭 B).whiskerLeft
              (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                whiskerRight iR.hom (𝟭 T') ≫
                  ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫ (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
            ((𝟭 B).associator (𝟭 B ⋙ R) H).inv
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
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| d g ≫ Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g))

Tactic:
congr

Goal state after:
case a
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
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| d g

case a
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
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g))
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 : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
      (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι'))) ⋯ =
    (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
      (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ 𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯

Tactic:
congr

Goal state after:
case e_g
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ inv (DerivedCategory.Q.map R.ι') = inv (DerivedCategory.Q.map R.ι') ≫ 𝟙 ((DerivedCategory.singleFunctor C 0).obj Y)
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✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
        (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
        (InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))

Tactic:
rw [← (HomotopyCategory.quotient _ _).map_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝) ≫
        InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1)).Exact

Tactic:
simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofCocomplex,
    CochainComplex.mk', CochainComplex.mk, CochainComplex.of_d]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).f,
      zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) 0).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) 0).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1)).f,
      zero := ⋯ }.Exact

Tactic:
apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)

Goal state after: