mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : b < a
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a

Tactic:
· simp only [uIcc_of_ge hab.le] at h ⊢
    rw [integral_symm, integral_derivWithin_Icc_of_contDiffOn_Icc h hab.le]
    abel

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

Goal state before:
pp: case zero
⊢ √2 ≤ rexp 1

Tactic:
Real.sqrt_le_left (by positivity),

Goal state after:
case zero
⊢ 2 ≤ rexp 1 ^ 2
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
q : ℚ
h₁ : IsIntegral ℤ ↑q
⊢ ∃ k, ↑q = ↑k

Tactic:
ratCast_iff

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
q : ℚ
h₁ : IsIntegral ℤ q
⊢ ∃ k, ↑q = ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) / (Complex.exp (-↑k / ↑n * ↑π * I) - 1) * ((-1) ^ (-k) - 1) =
    0

Tactic:
Complex.exp_neg,

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / (Complex.exp (-↑k / ↑n * ↑π * I) - 1) * ((-1) ^ (-k) - 1) =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / (Complex.exp (-(↑k / ↑n * ↑π * I)) - 1) * ((-1) ^ (-k) - 1) =
    0

Tactic:
Complex.exp_neg,

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / ((Complex.exp (↑k / ↑n * ↑π * I))⁻¹ - 1) * ((-1) ^ (-k) - 1) =
    0
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
⊢ P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ ↑n

Tactic:
refine ⟨fun hP => ?_, fun hP => by simp [hP]⟩

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
⊢ P = T ℝ ↑n
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.leadingCoeff = 2 ^ (n - 1)
hPdeg' : ↑n ≤ P.degree
⊢ P.coeff n = 2 ^ (n - 1)

Tactic:
replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
hPdeg' : P.degree = ↑n
⊢ P.coeff n = 2 ^ (n - 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Tactic:
have hn0 : ‖x‖ ≠ 0 := by rwa [norm_ne_zero_iff]

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hbc
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

Tactic:
rcases div_max_sq_ge_one x hx with H1 | H2
    · simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1
    · simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound2 z (x 0 / ‖x‖) H2

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
z : ℂ
⊢ (if z = l₀ then 1 else (z - l₀) ^ 2 * ℘[L] z) = (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2

Tactic:
grind [L.weierstrassPExcept_add ⟨_, hl₀⟩]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ TendstoLocallyUniformlyOn (fun n a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
    (fun {x} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s

Tactic:
obtain ⟨g, hg⟩ := h

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
g : 𝕜 → F
hg : HasSumLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) g s
⊢ TendstoLocallyUniformlyOn (fun n a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
    (fun {x} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
simp only [fib_add_two, add_sub_cancel_left]

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

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

Tactic:
fibRec.eq_iff_eqOn_range_order

Goal state after:
⊢ Set.EqOn (fun n ↦ ↑(Nat.fib n)) (fun n ↦ (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)

case hu
⊢ fibRec.IsSolution fun n ↦ ↑(Nat.fib n)

case hv
⊢ fibRec.IsSolution fun n ↦ (φ ^ n - ψ ^ n) / √5
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
⊢ z ∈ ℍₒ

Tactic:
simp [hz]

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

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

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

Tactic:
· exact (ha N (a.le_succ.trans aN)).2

Goal state after:
case hbc
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) - ↑(c (N - 1)) ≤ ε * ↑(c (N - 1))
Module: Mathlib.Analysis.SpecificLimits.FloorPow

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

Tactic:
gcongr
        have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
        simpa [B] using (ha _ aN').1

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
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < (↑n)⁻¹ * ↑n * (l - ε * (1 + l))

Tactic:
rw [inv_mul_cancel₀, one_mul]
        · linarith only [hε]
        · exact Nat.cast_ne_zero.2 (ne_of_gt npos)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
a b : ℕ
anti : AntitoneOn f (Icc ↑a ↑b)
integrable : IntegrableOn f (Ioi ↑a) volume
nonneg : ∀ t ∈ Ioi ↑a, 0 ≤ f t
hab : a ≤ b
⊢ 0 ≤ᵐ[volume.restrict (Ioi ↑a)] f

Tactic:
exact ae_restrict_of_forall_mem measurableSet_Ioi nonneg

Goal state after:
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:
embedding

Goal state after:
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 (preadditiveCoyonedaObj (generator F))
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
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
· have := essentiallySmallSelf (CostructuredArrow yoneda A)
      apply finallySmall_of_essentiallySmall

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
h : Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H)))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
by
  obtain ⟨t⟩ := h
  let t₂ := limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t
  let t₃ := (colimitLimitIso (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢).flip).inv t₂
  obtain ⟨k, y, -⟩ := Types.jointly_surjective'.{v, max u v} t₃
  refine ⟨k, ⟨?_⟩⟩
  let z := (limitObjIsoLimitCompEvaluation (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢).flip k).hom y
  let y := flipCompEvaluation (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢) k
  exact (lim.mapIso y).hom z

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.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv + g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯
          ⋯))

Tactic:
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])]

Goal state after:
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.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ +
          Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (Cocycle.toSingleMk (-(R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))

Tactic:
Cocycle.toSingleMk_neg _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
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
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        (F.rightDerivedToHomotopyCategory.map f ≫ (J.isoRightDerivedToHomotopyCategoryObj F).hom) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n

Tactic:
InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality f I J φ comm F,

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
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
          (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ P.isoModSerre f ↔ P.epiModSerre f

Tactic:
have := P.monoModSerre_of_mono f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
this : P.monoModSerre f
⊢ P.isoModSerre f ↔ P.epiModSerre f
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
M : Action V G
⊢ { hom := F.map (𝟙 M).hom, comm := ⋯ } =
    𝟙 { V := F.obj M.V, ρ := { toFun := fun g ↦ F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }

Tactic:
by ext; simp only [Action.id_hom, F.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map (inv f)ᘁ ⊗ₘ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ ≫ 𝟙 (𝟙_ D)

Tactic:
Category.comp_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map (inv f)ᘁ ⊗ₘ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }.f

Tactic:
dsimp only

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
Module: Mathlib.CategoryTheory.Bicategory.End

Goal state before:
pp: C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ ((fun {x x_1} η h ↦ η ▷ h) f₁✝ X₂✝ ≫ (fun {f x x_1} η ↦ f ◁ η) f₂✝) ≫
      (fun {x x_1} η h ↦ η ▷ h) g₁✝ Y₂✝ ≫ (fun {f x x_1} η ↦ f ◁ η) g₂✝ =
    (fun {x x_1} η h ↦ η ▷ h) (f₁✝ ≫ g₁✝) X₂✝ ≫ (fun {f x x_1} η ↦ f ◁ η) (f₂✝ ≫ g₂✝)

Tactic:
dsimp only

Goal state after:
C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ▷ X₂✝ ≫ Y₁✝ ◁ f₂✝) ≫ g₁✝ ▷ Y₂✝ ≫ Z₁✝ ◁ g₂✝ = (f₁✝ ≫ g₁✝) ▷ X₂✝ ≫ Z₁✝ ◁ (f₂✝ ≫ g₂✝)
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (ρ_ (𝟙_ V)).hom ≫
        (eHomEquiv V) f ≫
          eHomWhiskerRight V α.inv Y ≫
            eHomWhiskerLeft V X₁ β.hom ≫
              (ρ_ (X₁ ⟶[V] Y₁)).inv ≫
                (X₁ ⟶[V] Y₁) ◁ (eHomEquiv V) g ≫
                  (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫
                    (X₁ ⟶[V] Y₁) ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁

Tactic:
rw [rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc, hom_inv_id_assoc, ← whisker_exchange_assoc,
    ← whisker_exchange_assoc, ← eComp_eHomWhiskerLeft, eHom_whisker_cancel_assoc,
    ← eComp_eHomWhiskerRight_assoc, ← tensorHom_def_assoc,
    ← eHomEquiv_comp_assoc]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
by
  obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]
  infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
⊢ ∀ {b' : 𝒳} (g_1 : T ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift ((f ≫ g) ≫ g_1) φ'],
    ∃! χ, p.IsHomLift g_1 χ ∧ (φ ≫ ψ) ≫ χ = φ'

Tactic:
by
    intro c' h τ hτ
    use map p g ψ (f' := g ≫ h) rfl <| map p f φ (assoc f g h) τ
    refine ⟨⟨inferInstance, ?_⟩, ?_⟩
    · simp only [assoc, fac]
    · intro π' ⟨hπ'₁, hπ'₂⟩
      apply map_uniq
      apply map_uniq
      simp only [← hπ'₂, assoc]

Goal state after: