mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-(↑n + 1)).1 (↑n + 1).1) * #(Icc (-(↑n + 1)).2 (↑n + 1).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-(↑n + 1)) (↑n + 1)) * #(Icc (-(↑n + 1)) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
neg_add_rev,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -↑n).1 (↑n + 1).1) * #(Icc (-1 + -↑n).2 (↑n + 1).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hasSum
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ {y : ℂ}, y ∈ Metric.eball 0 ↑r → HasSum (fun n ↦ (L.weierstrassPExceptSeries l₀ x n) fun x ↦ y) (℘[L - l₀] (x + y))

Tactic:
intro z

Goal state after:
case hasSum
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
⊢ z ∈ Metric.eball 0 ↑r → HasSum (fun n ↦ (L.weierstrassPExceptSeries l₀ x n) fun x ↦ z) (℘[L - l₀] (x + z))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
simp [div_eq_iff, Nat.factorial_ne_zero, Nat.factorial_succ] at this ⊢

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

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ Multiset.count (cos ((2 * ↑k + 1) * π / (2 * ↑n)))
      (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val =
    1

Tactic:
Multiset.count_eq_one_of_mem (by simp)

Goal state after:
n k : ℕ
hk : k < n
⊢ 1 = 1

n k : ℕ
hk : k < n
⊢ cos ((2 * ↑k + 1) * π / (2 * ↑n)) ∈ (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : z = 0
⊢ (L.relation * id ^ 6) z =
    (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6

Tactic:
simp [hz0, relation]

Goal state after:
case pos
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : z = 0
⊢ 0 = 2 ^ 2 - 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ Multiset.count (cos ((↑k + 1) * π / (↑n + 1)))
      (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val =
    1

Tactic:
Multiset.count_eq_one_of_mem (by simp)

Goal state after:
n k : ℕ
hk : k < n
⊢ 1 = 1

n k : ℕ
hk : k < n
⊢ cos ((↑k + 1) * π / (↑n + 1)) ∈ (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn✝ : ¬n = 0
hn : 2 * k + 1 = n
hroot : x ∈ Finset.image (fun k ↦ cos (↑(2 * k + 1) * π / ↑(2 * n))) (Finset.range n)
hk₂ : cos (↑(2 * k + 1) * π / ↑(2 * n)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ cos (↑n * π / ↑(2 * n)) = 0

Tactic:
convert! cos_pi_div_two using 2

Goal state after:
n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn✝ : ¬n = 0
hn : 2 * k + 1 = n
hroot : x ∈ Finset.image (fun k ↦ cos (↑(2 * k + 1) * π / ↑(2 * n))) (Finset.range n)
hk₂ : cos (↑(2 * k + 1) * π / ↑(2 * n)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ ↑n * π / ↑(2 * n) = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
⊢ EqOn (iteratedDeriv k fun z ↦ cotTerm z d)
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) ℂ_ℤ

Tactic:
intro z

Goal state after:
k d : ℕ
z : ℂ
⊢ z ∈ ℂ_ℤ →
    iteratedDeriv k (fun z ↦ cotTerm z d) z =
      (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
⊢ EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℂ_ℤ)
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) ℂ_ℤ

Tactic:
apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen Complex.isOpen_compl_range_intCast)

Goal state after:
k d : ℕ
⊢ EqOn (iteratedDeriv k fun z ↦ cotTerm z d)
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) (range Int.cast)ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
⊢ EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) (range Int.cast)ᶜ)
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) ℍₒ

Tactic:
intro z

Goal state after:
k d : ℕ
z : ℂ
⊢ z ∈ ℍₒ →
    iteratedDerivWithin k (fun z ↦ cotTerm z d) (range Int.cast)ᶜ z =
      (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.CategoryTheory.Abelian.Projective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
⊢ Projective P

Tactic:
rw [projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))

Tactic:
by
  rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
  exact hf.neg.sum_le_integral

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
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₁)

pp: case h₂
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₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

pp: case h₃
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₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
· exact cokernelIsCokernel _

Goal state after:
case h₂
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₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

case h₃
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₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)
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
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
· exact cokernelIsCokernel _

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case pos
f : ℝ → ℝ
a b : ℕ
anti : AntitoneOn f (Icc ↑a ↑b)
integrable : IntegrableOn f (Ioi ↑a) volume
nonneg : ∀ t ∈ Ioi ↑a, 0 ≤ f t
hab : b < a
⊢ ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi ↑a, f x

Tactic:
simpa [Finset.Ico_eq_empty_of_le hab.le] using setIntegral_nonneg measurableSet_Ioi nonneg

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
hM : 0 < M
x : ℝ
⊢ x ∈ uIoo (↑N) (↑M + ↑N) → ‖f x‖ = f x

Tactic:
grind [Real.norm_of_nonneg, uIoo_of_le]

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

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log ((c⁻¹ ^ 2) ^ (Real.log j / Real.log c)) = Real.log (1 / j ^ 2)

Tactic:
Real.log_rpow A

Goal state after:
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log j / Real.log c * Real.log (c⁻¹ ^ 2) = Real.log (1 / j ^ 2)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y Z : StructuredArrow X (Comma.map α β)
f : Y ⟶ Z
⊢ (map₂ (𝟙 (L'.obj X.left)) α).map (homMk (Hom.right f).left ⋯) ≫
      { left := mk Z.hom.left, right := mk Z.hom.right, hom := homMk Z.right.hom ⋯ }.hom =
    { left := mk Y.hom.left, right := mk Y.hom.right, hom := homMk Y.right.hom ⋯ }.hom ≫
      (map₂ X.hom (inv β)).map (homMk (Hom.right f).right ⋯)

Tactic:
simp only [map₂_obj_right, mk_right, hom_eq_iff, comp_right,
      map₂_map_right, homMk_right, CommaMorphism.w]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Indization

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Ind C
f g : X ⟶ Y
h : ∀ (G : Ind C), ObjectProperty.ofObj Ind.yoneda.obj G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
i : X.presentation.I
⊢ colimit.ι (X.presentation.F ⋙ Ind.yoneda) i ≫ X.colimitPresentationCompYoneda.hom ≫ f =
    colimit.ι (X.presentation.F ⋙ Ind.yoneda) i ≫ X.colimitPresentationCompYoneda.hom ≫ g

Tactic:
simp [← Category.assoc, h]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ (J : ι → Type w) [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [inst_2 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)
⊢ IsIPCOfShape.{w, u_2, v_1, u_1} ι C

Tactic:
by
  refine .of_forall_exists fun J _ _ F _ ↦ ?_
  refine ⟨fun i ↦ colimit.cocone _, fun i ↦ colimit.isColimit _, ?_⟩
  obtain ⟨_, h⟩ := H J F
  rwa [IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
⊢ (finiteSubproductsCone f).π.app S = ∑ a ∈ (Opposite.unop S).attach, Pi.π f (↑a).as ≫ Pi.ι (fun a ↦ f (↑a).as) a

Tactic:
dsimp only [finiteSubproductsCone_pt, Functor.const_obj_obj, liftToFinsetObj_obj,
    Discrete.functor_obj_eq_as, finiteSubproductsCone_π_app]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
⊢ (Pi.lift fun s ↦ Pi.π f (↑s).as) = ∑ a ∈ (Opposite.unop S).attach, Pi.π f (↑a).as ≫ Pi.ι (fun a ↦ f (↑a).as) a
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ QuasiIso R.π'

Tactic:
dsimp [π']; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: 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))
⊢ (Φ.colonπ Ψ).app X ≫ Ψ.ι.app (Φ.quotient.obj X) = 0

Tactic:
h.eq_zero_of_tgt ((colonπ Φ Ψ).app X),

Goal state after:
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))
⊢ 0 ≫ Ψ.ι.app (Φ.quotient.obj X) = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f =
    0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
have : S.g (kernel.ι S.g) = 0 := apply_eq_zero_of_comp_eq_zero _ _ (kernel.condition _)
      -- By pseudo-exactness, we get a preimage.
      obtain ⟨a', ha⟩ := hS _ this
      obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
      rw [← ha'] at ha
      obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
      -- Consider the pullback of `kernel.ι (cokernel.π f)` and `kernel.ι g`.
      -- The commutative diagram given by the pseudo-equality `f a = b` induces
      -- a cone over this pullback, so we get a factorization `z`.
      obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g) _ (r ≫ a.hom ≫ Abelian.factorThruImage S.f) q (by
          simp only [Category.assoc, Abelian.image.fac]
          exact comm)
      -- Let's give a name to the second pullback morphism.
      let j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd _ _
      -- Since `q` is an epimorphism, in particular this means that `j` is an epimorphism.
      have pe : Epi j := epi_of_epi_fac hz₂
      -- But it is also a monomorphism, because `kernel.ι (cokernel.π f)` is: A kernel is
      -- always a monomorphism and the pullback of a monomorphism is a monomorphism.
      -- But mono + epi = iso, so `j` is an isomorphism.
      have : IsIso j := isIso_of_mono_of_epi _
      -- But then `kernel.ι g` can be expressed using all of the maps of the pullback square, and we
      -- are done.
      rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
      simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]

Goal state after:
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
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
⊢ (Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ = R'.extMk (φ.hom.f n ≫ f) m hm ⋯

Tactic:
by
  have := HasDerivedCategory.standard C
  ext
  have : (R'.cochainComplexXIso (-n) n (by lia)).hom ≫ φ.hom.f n =
      φ.hom'.f (-n) ≫ (R.cochainComplexXIso (-n) n (by lia)).hom := by
    simp [φ.hom'_f _ _ rfl]
  simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, reassoc_of% this]
  rw [Cocycle.toSingleMk_precomp _ _ _ (by lia)
    (by simpa [R.cochainComplex_d _ _ _ _ rfl rfl]),
    Cocycle.equivHomShift_symm_precomp,
    ← ShiftedHom.mk₀_comp 0 rfl, ShiftedHom.map_comp,
    ← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) _ (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) _ (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),
    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]
  congr 3
  simp [← Functor.map_comp_assoc, ← Functor.map_comp]

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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
this : StrongEpi f
⊢ P (Abelian.image (f ≫ g)) ↔ P Z

Tactic:
exact P.prop_iff_of_iso (Abelian.imageIsoImage _ ≪≫ (image.isoStrongEpiMono f g rfl).symm)

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
⊢ (MorphismProperty.monomorphisms D).inverseImage L = P.monoModSerre

Tactic:
ext
  simp [mono_map_iff L P]

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : G
⊢ (leftRegular G ⊗ X).ρ x✝ ≫
      { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom =
    { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom ≫
      (leftRegular G ⊗ trivial G X.V).ρ x✝

Tactic:
ext _
      simp only [tensorObj_V, tensor_ρ]
      simp [types_tensorObj_def]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
⊢ (Sigma.desc fun h ↦ (Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) = f.app x

Tactic:
ext g

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
g : c ⟶ x
⊢ (Sigma.ι (fun x ↦ d) g ≫ Sigma.desc fun h ↦ (Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    Sigma.ι (fun x ↦ d) g ≫ f.app x
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
⊢ (Pi.lift fun g ↦ F.map g ≫ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) = f.app x

Tactic:
ext g

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
g : x ⟶ c
⊢ (Pi.lift fun g ↦ F.map g ≫ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) ≫ Pi.π (fun x ↦ d) g = f.app x ≫ Pi.π (fun x ↦ d) g
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
← (adj₁.homEquiv _ _).injective.eq_iff,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ (adj₁.homEquiv ((𝟭 B).obj (L.obj Y)) (F.obj (U.obj (F.obj X)))) (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      (adj₁.homEquiv ((𝟭 B).obj (L.obj Y)) (F.obj (U.obj (F.obj X)))) (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))