mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 0 ≤ 1 - ε / 4

Tactic:
by linarith

Goal state after:
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
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l‖ - ‖s‖

Tactic:
by linarith

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 ≤ ‖↑l‖ - ‖s‖

Tactic:
by linarith

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

Goal state before:

Tactic:
_ = n * n ^ b.card * n ^ (a.card - b.card - (1 : ℤ)) *
        (a.map (fun x : ℂ ↦ (x + n) / n)).prod := by
      congr 1
      rw [← pow_succ', ← zpow_natCast, ← zpow_natCast, ← zpow_add' (by left; norm_cast)]
      grind
    _ = _ := by ring

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 ≤ 2

Tactic:
by linarith

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

Goal state before:
pp: ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
line7 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| < √ε
line2 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| ≤ √ε
line6 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| ≤ √ε
line4 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'| = 0
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| +
                |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| +
              |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| +
            |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'| +
          |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| +
        |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| +
      |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤
    6 * √ε

Tactic:
by linarith

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - (1 / 2 * log (2 * ↑(n✝ + 1)) + ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)) =
    log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

pp: case succ.hx
n✝ : ℕ
⊢ 0 < 2 * ↑(n✝ + 1)

pp: case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

pp: case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

Tactic:
tsub_tsub

Goal state after:
case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - (1 / 2 * log (2 * ↑(n✝ + 1)) + ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)) =
    log ↑(n✝ + 1)! - (1 / 2 * log (2 * ↑(n✝ + 1)) + ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1))

case succ.hx
n✝ : ℕ
⊢ 0 < 2 * ↑(n✝ + 1)

case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ 2 < i + 3

Tactic:
by linarith

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

Goal state before:
pp: n m : ℤ
⊢ ∫ (x : ℝ), eval x (T ℝ (n + m)) + eval x (T ℝ (n - m)) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT

Tactic:
rw [MeasureTheory.integral_add
    (integrable_measureT (by fun_prop)) (integrable_measureT (by fun_prop))]

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

Goal state before:
pp: n m : ℕ
h : n ≠ m
⊢ ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑m) ∂measureT = 0

Tactic:
integral_eval_T_real_mul_eval_T_real_measureT,

Goal state after:
n m : ℕ
h : n ≠ m
⊢ (∫ (x : ℝ), eval x (T ℝ (↑n + ↑m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑m)) ∂measureT) / 2 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑n) ∂measureT = π / 2

Tactic:
integral_eval_T_real_mul_eval_T_real_measureT,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (∫ (x : ℝ), eval x (T ℝ (↑n + ↑n)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑n)) ∂measureT) / 2 = π / 2
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
⊢ P.coeff n ≤ 2 ^ (n - 1)

Tactic:
convert! sumNodes_le_sumNodes_T (fun i hi => le_of_lt <| negOnePow_mul_leadingCoeffC_pos hi) hPbnd
  · rw [sumNodes_eq_coeff hPdeg]
  · rw [sumNodes_T_eq]

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

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l / ↑n ! * ↑n ! = if n = 0 then ℘[L - l] l else ↑(n + 1)! * L.sumInvPow l (n + 2)

Tactic:
← eq_div_iff_mul_eq (by simp)

Goal state after:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l / ↑n ! = (if n = 0 then ℘[L - l] l else ↑(n + 1)! * L.sumInvPow l (n + 2)) / ↑n !
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ 0 ≤ ↑k

Tactic:
hk'

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ 0 ≤ ↑n * (arccos x / π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ ↑k ≤ ↑n * 1

Tactic:
hk'

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ ↑n * (arccos x / π) ≤ ↑n * 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ 1 - k < -1

Tactic:
by linarith

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

Goal state before:
pp: L : PeriodPair
⊢ AnalyticAt ℂ (L.relation * id ^ 6) 0

Tactic:
refine .congr ?_ L.relation_mul_id_pow_six_eventuallyEq.symm
  fun_prop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)

Tactic:
apply ShortComplex.isColimitOfIsColimitπ <;>
      apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2
    · exact cokernelIsCokernel _
    · exact isColimit f g
    · exact cokernelIsCokernel _

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

Goal state before:
pp: case refine_1
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
⊢ ∃ W x x, True

Tactic:
obtain ⟨Q⟩ : Nonempty (CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))) :=
        IsCofiltered.nonempty
      obtain ⟨ia, va₁, va₂, heqa⟩ := exists_eq_of_isCofiltered_costructuredArrow L
        (Q.hom ≫ R.map (IsCofiltered.minToLeft j₁.right j₂.right)) j₁.hom
      obtain ⟨ib, vb₁, vb₂, heqb⟩ := exists_eq_of_isCofiltered_costructuredArrow L
        (Q.hom ≫ R.map (IsCofiltered.minToRight j₁.right j₂.right)) j₂.hom
      obtain ⟨i₀, il₀, ir₀, heq⟩ := IsCofiltered.cospan va₁ vb₁
      exact ⟨⟨i₀, IsCofiltered.min j₁.right j₂.right, L.map (il₀ ≫ va₁) ≫ Q.hom⟩,
        ⟨il₀ ≫ va₂, IsCofiltered.minToLeft _ _, by simp [← heqa]⟩,
        ⟨ir₀ ≫ vb₂, IsCofiltered.minToRight _ _, by cat_disch⟩, trivial⟩

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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
b : B
⊢ Nonempty (Comma L R)

Tactic:
obtain ⟨X⟩ : Nonempty (CostructuredArrow L (R.obj b)) := IsCofiltered.nonempty

Goal state after:
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
b : B
X : CostructuredArrow L (R.obj b)
⊢ Nonempty (Comma L R)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_1
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
b : B
⊢ ∃ c, Nonempty ((fst L R).obj c ⟶ a)

Tactic:
obtain ⟨X⟩ : Nonempty (CostructuredArrow L (R.obj b)) := IsCofiltered.nonempty

Goal state after:
case refine_1
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
b : B
X : CostructuredArrow L (R.obj b)
⊢ ∃ c, Nonempty ((fst L R).obj c ⟶ a)
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).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
    (yoneda.obj A).map (colimit.ι F (op i)).op

Tactic:
by
  simp only [colimitHomIsoLimitYoneda', Iso.trans_hom,
    Iso.app_hom, Category.assoc]
  erw [limitObjIsoLimitCompEvaluation_hom_π]
  change ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ _).app A = _
  rw [coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, Functor.flip_map_app]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ObjectProperty.strictColimitsOfShape IsIndObject J ≤ IsIndObject

Tactic:
rintro _ ⟨F, hF⟩
    exact isIndObject_colimit _ _ hF

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
X' : C
R' : InjectiveResolution X'
f : X ⟶ X'
φ : R.Hom R' f
⊢ (R.ι' ≫ φ.hom').f 0 = ((CochainComplex.singleFunctor C 0).map f ≫ R'.ι').f 0

Tactic:
by
    simp [hom'_f _ 0 0 rfl, ι'_f_zero, CochainComplex.singleFunctor,
      CochainComplex.singleFunctors,
      HomologicalComplex.single, HomologicalComplex.singleObjXSelf,
      HomologicalComplex.singleObjXIsoOfEq]

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
⊢ ∃ a, (preadditiveCoyonedaObj G).map a = f

Tactic:
refine ⟨epiDesc _ _ h, ?_⟩

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
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
⊢ (preadditiveCoyonedaObj G).map (epiDesc (Sigma.desc fun m ↦ m) (Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) h) = f
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:
by
    rw [← (HomotopyCategory.quotient _ _).map_comp]
    apply HomotopyCategory.eq_of_homotopy
    apply InjectiveResolution.descCompHomotopy

Goal state after:
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
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
W : C
s : Y ⟶ W
hs : P.monoModSerre s
eq : (z ≫ f) ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), z ≫ s = 0

Tactic:
exact ⟨W, f ≫ s, MorphismProperty.comp_mem _ _ _ hf hs, by simpa using! eq⟩

Goal state after:
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
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ z = 0

Tactic:
rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]

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
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ L.map φ.f = 0
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Tactic:
rw [← comp_hom, Iso.hom_inv_id, id_hom]

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
⊢ PreservesFiniteColimits
    ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
have : PreservesFiniteColimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
this : PreservesFiniteColimits ((evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesFiniteColimits
    ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
      fiber :=
        (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
          (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber } =
    { base := f.base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map f.fiber ≫
            (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
      { base := g.base,
        fiber :=
          (α.app { as := op b.base }).toFunctor.map g.fiber ≫
            (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }

Tactic:
ext
    · dsimp
    · simp only [categoryStruct_comp_base, op_comp, Quiver.Hom.comp_toLoc,
        categoryStruct_comp_fiber, Cat.Hom.comp_toFunctor, map_comp, naturality_comp_hom_app, assoc,
        eqToHom_refl, comp_id]
      slice_lhs 2 4 => simp [← Cat.Hom.toNatIso_inv, Cat.Hom.comp_toFunctor,
        ← Cat.Hom.toNatIso_hom, ← map_comp, Iso.inv_hom_id_app, comp_obj, map_id, comp_id]
      simp only [assoc, ← reassoc_of% Cat.Hom.comp_map,
        Cat.Hom.comp_toFunctor, Functor.comp_obj, NatTrans.naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }

Tactic:
rcases List.exists_isChain_cons_of_relationReflTransGen h₁₂ with ⟨l, hl₁, hl₂⟩

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y : RelCat
r : X ⟶ Y
⊢ IsIso r ↔ ∃ f, graphFunctor.map f.hom = r

Tactic:
constructor
  · intro h
    have h1 := congr_fun₂ congr((· ~[($h.hom_inv_id).rel] ·))
    have h2 := congr_fun₂ congr((· ~[($h.inv_hom_id).rel] ·))
    simp only [RelCat.Hom.rel_comp_apply₂, RelCat.Hom.rel_id_apply₂, eq_iff_iff] at h1 h2
    obtain ⟨f, hf⟩ := Classical.axiomOfChoice (fun a => (h1 a a).mpr rfl)
    obtain ⟨g, hg⟩ := Classical.axiomOfChoice (fun a => (h2 a a).mpr rfl)
    suffices hif : IsIso (C := Type u) (↾f) by
      use asIso (↾f)
      ext ⟨x, y⟩
      exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩
    use ↾g
    constructor
    · ext x
      apply (h1 _ _).mp
      use f x, (hg _).2, (hf _).2
    · ext y
      apply (h2 _ _).mp
      use g y, (hf (g y)).2, (hg y).2
  · rintro ⟨f, rfl⟩
    apply graphFunctor.map_isIso

Goal state after:
Module: Mathlib.CategoryTheory.Widesubcategory

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty D
inst✝ : P.IsMultiplicative
X Y : InducedWideCategory D F P
f g : X ⟶ Y
eq : (wideInducedFunctor F P).map f = (wideInducedFunctor F P).map g
⊢ f = g

Tactic:
by
    cases f
    cases g
    aesop

Goal state after:
Module: Mathlib.CategoryTheory.DinatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f =
    (F.obj (op Y✝)).map f ≫ δ.app Y✝ ≫ (α.app (op Y✝)).app Y✝ ≫ (H.map f.op).app Y✝

Tactic:
← NatTrans.naturality_app,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f =
    (F.obj (op Y✝)).map f ≫ δ.app Y✝ ≫ (G.map f.op).app Y✝ ≫ (α.app (op X✝)).app Y✝
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = (g' ≫ g) ≫ f

Tactic:
rwa [assoc, ← H]

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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : IsIso f
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ; clear a b R S
  -- Let `φ'` be the morphism induced by applying universal property to `𝟙 a` lying over `f ≫ f⁻¹`.
  let φ' := map p (p.map φ) φ (IsIso.hom_inv_id (p.map φ)).symm (𝟙 a)
  use φ'
  -- `φ ≫ φ' = 𝟙 a` follows immediately from the universal property.
  have inv_hom : φ ≫ φ' = 𝟙 a := fac p (p.map φ) φ _ (𝟙 a)
  refine ⟨inv_hom, ?_⟩
  -- We will now show that `φ' ≫ φ = 𝟙 b` by showing that `φ ≫ (φ' ≫ φ) = φ ≫ 𝟙 b`.
  have h₁ : IsHomLift p (𝟙 (p.obj b)) (φ' ≫ φ) := by
    rw [← IsIso.inv_hom_id (p.map φ)]
    apply IsHomLift.comp
  apply IsStronglyCocartesian.ext p (p.map φ) φ (𝟙 (p.obj b))
  simp only [← assoc, inv_hom, comp_id, id_comp]

Goal state after: