mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ F.mapDerivedCategoryFactors.hom =
    whiskerRight (DerivedCategory.quotientCompQhIso C₁).inv F.mapDerivedCategory ≫
      ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).associator DerivedCategory.Qh F.mapDerivedCategory).hom ≫
        (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).whiskerLeft F.mapDerivedCategoryFactorsh.hom ≫
          ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).associator (F.mapHomotopyCategory (ComplexShape.up ℤ))
                DerivedCategory.Qh).inv ≫
            whiskerRight (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom DerivedCategory.Qh ≫
              ((F.mapHomologicalComplex (ComplexShape.up ℤ)).associator
                    (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh).hom ≫
                (F.mapHomologicalComplex (ComplexShape.up ℤ)).whiskerLeft (DerivedCategory.quotientCompQhIso C₂).hom

Tactic:
by
      ext K
      dsimp
      simp only [id_comp, mapDerivedCategoryFactorsh_hom_app, assoc, comp_id,
        ← Functor.map_comp_assoc, Iso.inv_hom_id_app, map_id, comp_obj]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_3
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ quasiIso C ≤ (CochainComplex.Plus.quasiIso C).map (quotient C)

Tactic:
rintro K L f hf

Goal state after:
case refine_3
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
K L : Plus C
f : K ⟶ L
hf : quasiIso C f
⊢ (CochainComplex.Plus.quasiIso C).map (quotient C) f
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero ((double f hi₀₁).X k)

Tactic:
dsimp [double]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
i : ι
⊢ (i ∈ Function.support fun x ↦ ↑(Module.finrank R ↑(X x))) ↔ i ∈ Function.support fun i ↦ Module.finrank R ↑(X i)

Tactic:
simp [Function.mem_support]

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
⊢ (double f hi₀₁).X i₁ = X₁

Tactic:
dsimp [double]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
⊢ (if i₁ = i₀ then X₀ else if i₁ = i₁ then X₁ else 0) = X₁
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
⊢ shiftFunctor C (m + n) ≅ shiftFunctor C m ⋙ shiftFunctor C n

Tactic:
refine NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) ?_) (fun f => ?_)
  · dsimp
    rw [← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)]
    simp only [Category.assoc, Iso.inv_hom_id_app_assoc]
    rw [← NatTrans.naturality_assoc]
    dsimp
    simp only [Functor.map_comp, Category.assoc,
      shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 1 m n X.obj,
      Iso.inv_hom_id_app_assoc]
  · ext; dsimp; exact NatTrans.naturality _ _

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = ↑n
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ opcyclesMap (h.map h' fK fL f_comm) m =
    (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯).inv ≫
      opcyclesMap h.restrictionGEIso.hom n ≫
        opcyclesMap fL n ≫
          opcyclesMap h'.restrictionGEIso.inv n ≫
            (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯).hom

Tactic:
← cancel_epi (HomologicalComplex.pOpcycles ..)

Goal state after:
case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = ↑n
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ pOpcycles h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    pOpcycles h.cochainComplex m ≫
      (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯).inv ≫
        opcyclesMap h.restrictionGEIso.hom n ≫
          opcyclesMap fL n ≫
            opcyclesMap h'.restrictionGEIso.inv n ≫
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯).hom
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = -↑(n + 1)
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology K n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology K' n
⊢ opcyclesMap (h.map h' fK fL f_comm) m =
    (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯).inv ≫
      opcyclesMap h.restrictionLEIso.hom n ≫
        opcyclesMap fK n ≫
          opcyclesMap h'.restrictionLEIso.inv n ≫
            (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯).hom

Tactic:
← cancel_epi (HomologicalComplex.pOpcycles ..)

Goal state after:
case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = -↑(n + 1)
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology K n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology K' n
⊢ pOpcycles h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    pOpcycles h.cochainComplex m ≫
      (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯).inv ≫
        opcyclesMap h.restrictionLEIso.hom n ≫
          opcyclesMap fK n ≫
            opcyclesMap h'.restrictionLEIso.inv n ≫
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯).hom
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ (π Λ).app ((toKaroubi A).obj X) = (π' Λ).app X

Tactic:
simp [π, whiskeringLeftObjToKaroubiFullyFaithful]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Single

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X : C
i : J
h : i ≠ j
⊢ IsInitial ((single j).obj X i)

Tactic:
dsimp [single]

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X : C
i : J
h : i ≠ j
⊢ IsInitial (if i = j then X else ⊥_ C)
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α

Tactic:
convert! h

Goal state after:
case e'_2.e'_6.e'_8
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
    ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
e_3✝ : (X.H n₀).obj (mk₁ g) = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯))
e_4✝ : (X.H n₀).obj (mk₁ g') = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯))
e_6✝ : mk₁ g = mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)
e_7✝ : mk₁ g' = mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯)
⊢ β = homMk₁ (α.app 1) (β.app 1) ⋯

case e'_3.e'_7
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
    ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
⊢ α = homMk₁ (α.app 0) (α.app 1) ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero ((X.H n₀).obj (mk₁ f))
h₂ : IsZero ((X.H n₁).obj (mk₁ f))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
have := X.mono_H_map_twoδ₁Toδ₀ n₀ f g fg hfg h₁
  have := X.epi_H_map_twoδ₁Toδ₀ n₀ n₁ hn₁ f g fg hfg h₂
  apply isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
rw [hi₂, data.hi₂₃]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_3
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
rw [hi₂, data.hi₂₃]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_3
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
rw [hi₂, data.hi₂₃]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ data.i₁ pq = data.i₂ pq'

Tactic:
← data.hc₀₂ r₀ pq pq' hpq,

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ data.i₁ pq = data.i₀ r₀ pq ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₀ n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₁ : n₀ + 1 = data.deg pq
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
⊢ pageD X data r pq pq' ⋯ =
    (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ (data.deg pq) n₂ ⋯
          hn₁ hn₂).hom ≫
      X.d f₁ f₂ f₃ f₄ f₅ n₀ (data.deg pq) n₂ n₃ hn₁ hn₂ hn₃ ≫
        (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq) n₂
            n₃ ⋯ hn₂ hn₃).inv

Tactic:
obtain rfl : n₀ = data.deg pq - 1 := by lia

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
⊢ pageD X data r pq pq' ⋯ =
    (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
          (data.deg pq) n₂ ⋯ hn₁ hn₂).hom ≫
      X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) n₂ n₃ hn₁ hn₂ hn₃ ≫
        (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq) n₂
            n₃ ⋯ hn₂ hn₃).inv
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
WellFounded.wellFounded_iff_has_min

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔
    ∀ (s : Set (Submodule R M)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j

Tactic:
exact monotone_stabilizes f

Goal state after:
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y z : L
m✝ n✝ : M
x m : L
n : M →ₗ[R] R
⊢ { toFun := fun m_1 ↦ -{ toFun := fun m_2 ↦ -n ⁅m, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅x, m_1⁆, map_add' := ⋯,
      map_smul' := ⋯ } =
    { toFun := fun m_1 ↦ -n ⁅⁅x, m⁆, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m_1 ↦ -{ toFun := fun m ↦ -n ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅m, m_1⁆, map_add' := ⋯,
        map_smul' := ⋯ }

Tactic:
by ext p; simp

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥ ↔ ⟨x, hx⟩ ∈ ⊤

Tactic:
rw [LieSubalgebra.mem_bot] at hx

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx✝ : x ∈ ⊥
hx : x = 0
⊢ ⟨x, hx✝⟩ ∈ ⊥ ↔ ⟨x, hx✝⟩ ∈ ⊤
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk x₁ + Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₁ + Submodule.Quotient.mk y₂

Tactic:
hxy₁,

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk y₁ + Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₁ + Submodule.Quotient.mk y₂
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: A : Type u_3
inst✝ : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : (Ideal.Quotient.mk I) x₁ = (Ideal.Quotient.mk I) y₁
hxy₂ : (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₂
⊢ (Ideal.Quotient.mk I) x₁ * (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₁ * (Ideal.Quotient.mk I) y₂

Tactic:
hxy₁,

Goal state after:
A : Type u_3
inst✝ : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : (Ideal.Quotient.mk I) x₁ = (Ideal.Quotient.mk I) y₁
hxy₂ : (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₂
⊢ (Ideal.Quotient.mk I) y₁ * (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₁ * (Ideal.Quotient.mk I) y₂
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk x₁ - Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₁ - Submodule.Quotient.mk y₂

Tactic:
hxy₁,

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk y₁ - Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₁ - Submodule.Quotient.mk y₂
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x : M
⊢ x - 0 ∈ U ↔ x ∈ U

Tactic:
sub_zero

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x : M
⊢ x ∈ U ↔ x ∈ U
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p %ₘ q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0

Tactic:
by
  rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (C.comp (Quotient.mk I)) (a.coeff n) * X ^ n = 0

Tactic:
refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ ((C.comp (Quotient.mk I)) (a.coeff n)).coeff m = coeff 0 m
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inl
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Subsingleton A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f

pp: case inr
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f

Tactic:
· rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]

Goal state after:
case inr
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ ((Quotient.mk I).comp C) (f.coeff n) = 0

Tactic:
rw [RingHom.mem_ker, coe_mapRingHom] at hf

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : Polynomial.map i f = 0
n : ℕ
⊢ ((Quotient.mk I).comp C) (f.coeff n) = 0