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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) * ‖z - x‖ ^ (p.1 + 1) =
    ‖↑p.1 + 2‖ * ((‖↑p.2 - x‖ / ‖z - x‖) ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)

Tactic:
simp [hpx, zpow_sub₀, div_pow]; field

Goal state after:
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 ((-1).1 + (-↑n).1) ((↑n).1 + 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)

Tactic:
fst_neg,

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.1 + -(↑n).1) ((↑n).1 + 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.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
⊢ x ∈ box 0 ↔ max x.1.natAbs x.2.natAbs = 0

Tactic:
simp [Prod.ext_iff]

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n))

Tactic:
convert! one_lt_eval_T_real hn (lt_neg_of_lt_neg hx)

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)

Goal state after:
case refine_1
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

case refine_2
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 ≤ ∏ a ∈ i_1, (x - node n a)

case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : ↑n * eval x (U ℝ (↑n - 1)) = 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

Tactic:
mul_eq_zero_iff_left (by aesop)

Goal state after:
case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : eval x (U ℝ (↑n - 1)) = 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x + ↑l) = L.relation x

Tactic:
simp only [relation, derivWeierstrassP_add_coe, weierstrassP_add_coe]
  congr 1
  simpa using (L.lattice.toAddSubgroup.add_mem_cancel_right (y := x) l.2)

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

Goal state before:
pp: ⊢ MeromorphicNFOn tan Set.univ

Tactic:
intro x _
  refine MeromorphicNFOn.div analyticAt_sin analyticAt_cos.meromorphicNFAt ?_
  grind [sin_sq_add_cos_sq]

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

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
rw [← hfderiv, Polynomial.eval_finsetSum]

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = ∑ i ∈ f.support, eval y (f i • i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
| Summable fun i ↦ ‖(↑i + 1) ^ (-1 - ↑k)‖

Tactic:
conv =>

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ↑(n + 1)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: β : Type u_2
inst✝ : CommRing β
⊢ { order := 2, coeffs := ![1, 1] }.charPoly = X ^ 2 - (X + 1)

Tactic:
LinearRecurrence.charPoly

Goal state after:
β : Type u_2
inst✝ : CommRing β
⊢ (monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      ∑ i, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) =
    X ^ 2 - (X + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + ∑' (n : ℕ), iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z =
    (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
conv =>

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑n + 1)) ^ (-1 - ↑k) + (z - (↑n + 1)) ^ (-1 - ↑k))) z
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
ε : ℝ
ε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 : ℕ := (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
h : N < a + 1
cNM : c N ≤ M
⊢ False

Tactic:
exact lt_irrefl _ ((cNM.trans hn).trans_lt ncN)

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
⊢ (f ≫ biprod.inl) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = biprod.inl ≫ 0

Tactic:
assoc,

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
⊢ f ≫ biprod.inl ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = biprod.inl ≫ 0
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : ObjectProperty C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (G : C), P G → ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

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

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.π₂)

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.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
h : N < a + 1
cNM : c N ≤ M
⊢ False

Tactic:
exact lt_irrefl _ ((cNM.trans hn).trans_lt ncN)

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

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
⊢ (iso A K).hom = limit.post K A

Tactic:
dsimp [iso, -Iso.app_hom]

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
⊢ (((((((((((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
                              (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))).app
                          (limit K)).hom ≫
                      (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (limit K)).hom) ≫
                    (HasColimit.isoOfNatIso
                        ((CostructuredArrow.proj yoneda A).associator yoneda
                          ((evaluation Cᵒᵖ (Type u)).obj (limit K)))).hom) ≫
                  (HasColimit.isoOfNatIso (isoAux A K)).hom) ≫
                (HasColimit.isoOfNatIso
                    (preservesLimitIso
                      (coyoneda ⋙
                        (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                      K)).hom) ≫
              (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom) ≫
            (colimitLimitIso (functorToInterchange A K)).hom) ≫
          (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))).hom) ≫
        (HasLimit.isoOfNatIso
            (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K)).hom) ≫
      (HasLimit.isoOfNatIso
          (K.isoWhiskerLeft
            ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
              (Presheaf.isColimitTautologicalCocone A)))).hom =
    limit.post K A
Module: Mathlib.CategoryTheory.Limits.Indization.Equalizers

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
inst✝ : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
P : IndParallelPairPresentation (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)
⊢ IsIndObject (limit F)

Tactic:
exact IsIndObject.map
      (HasLimit.isoOfNatIso (P.parallelPairIsoParallelPairCompYoneda.symm ≪≫
        (diagramIsoParallelPair _).symm)).hom
      (isIndObject_limit_comp_yoneda_comp_colim (parallelPair P.φ P.ψ)
        (fun i => isIndObject_limit_comp_yoneda _))

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
⊢ IsIndObject = leftExactFunctor Cᵒᵖ (Type u)

Tactic:
by ext; apply isIndObject_iff_preservesFiniteLimits

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
hpush :
  IsPushout (limMap c.π) (limMap ((Functor.const J).map f)) (limMap (pushout.inl c.π ((Functor.const J).map f)))
    (limMap (pushout.inr c.π ((Functor.const J).map f)))
this : IsIso (limMap c.π)
⊢ IsIso (limMap (pushout.inr c.π ((Functor.const J).map f)))

Tactic:
apply hpush.isIso_inr_of_isIso

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

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

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

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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (g ≫ f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
Cocycle.fromSingleMk_precomp g _ (zero_add _) _ (by lia) (by
      simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]),

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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              ((Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯).precomp
                ((singleFunctor C 0).map g)))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
        (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ)) ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
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) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (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:
assoc,

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 (F.rightDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (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
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 : ℕ
⊢ ((I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f) ≫ (J.isoRightDerivedObj F n).hom =
    ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
        (J.isoRightDerivedObj F n).inv) ≫
      (J.isoRightDerivedObj F n).hom

Tactic:
assoc,

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 : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
    ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
        (J.isoRightDerivedObj F n).inv) ≫
      (J.isoRightDerivedObj F n).hom
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 : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
    ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
        (J.isoRightDerivedObj F n).inv) ≫
      (J.isoRightDerivedObj F n).hom

Tactic:
assoc,

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 : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv ≫ (J.isoRightDerivedObj F n).hom