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

Goal state before:
pp: 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
inst✝³ : EnoughInjectives C
F : Plus C ⥤ H
inst✝² : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝¹ : F'.IsRightDerivedFunctor α (quasiIso C)
K : CochainComplex.Plus C
n : ℤ
inst✝ : Injective (K.obj.X n)
⊢ Injective (((quotient C).obj K).obj.as.X n)

Tactic:
assumption

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

Goal state before:
pp: case pos.inl
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₁ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

Tactic:
assumption

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

Goal state before:
pp: case pos.inr
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₀ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
assumption

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

Goal state before:
pp: case pos.inl
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₁ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

Tactic:
assumption

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

Goal state before:
pp: case pos.inr
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₀ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
assumption

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d i j =
        (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d i j ≫
          (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
rintro _ n rfl

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d (n + 1) n =
    (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d (n + 1) n ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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
⊢ homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m =
    (((restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n (n + 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯).inv ≫
          homologyMap h.restrictionGEIso.hom n) ≫
        homologyMap fL n ≫
          homologyMap h'.restrictionGEIso.inv n ≫
            (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n (n + 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯).hom) ≫
      homologyι h'.cochainComplex m

Tactic:
simp only [homologyι_naturality, Category.assoc, restrictionHomologyIso_hom_homologyι,
    homologyι_naturality_assoc, restrictionHomologyIso_inv_homologyι_assoc]

Goal state after:
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
⊢ homologyι h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    homologyι 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: 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
⊢ homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m =
    (((restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              ⋯).inv ≫
          homologyMap h.restrictionLEIso.hom n) ≫
        homologyMap fK n ≫
          homologyMap h'.restrictionLEIso.inv n ≫
            (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯).hom) ≫
      homologyι h'.cochainComplex m

Tactic:
simp only [homologyι_naturality, Category.assoc, restrictionHomologyIso_hom_homologyι,
    homologyι_naturality_assoc, restrictionHomologyIso_inv_homologyι_assoc]

Goal state after:
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
⊢ homologyι h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    homologyι 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.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ ↑(fromSingleMk f h q' hq' ⋯) = ↑α

Tactic:
assumption

Goal state after:
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
⊢ Epi ((karoubi.π Λ).app ((toKaroubi A).obj X))

Tactic:
rw [karoubi.π_app_toKaroubi_obj]

Goal state after:
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
⊢ Epi ((karoubi.π' Λ).app X)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ↑(toSingleMk f h p' hp' ⋯) = ↑α

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Abelian C
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0 ≫ P.fromLeftDerivedZero' F =
    F.map (P.π.f 0)

Tactic:
by
  simp [fromLeftDerivedZero']

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : (curriedTensor C).Additive
inst✝³ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝² : AddMonoid I
c : ComplexShape I
inst✝¹ : c.TensorSigns
K₁ K₂ : HomologicalComplex C c
inst✝ : GradedObject.HasTensor K₁.X K₂.X
⊢ K₁.HasTensor K₂

Tactic:
assumption

Goal state after:
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 l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0

Tactic:
have eq := X.δ_naturality f g f (g ≫ h) (𝟙 _) (twoδ₂Toδ₁ g h _ rfl) n₁ n₂

Goal state after:
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 l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯ ≫ (X.H n₂).map (𝟙 (mk₁ f))
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: case convert_3
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₁₂Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₁₂ X₁ ((single₀ I).obj (𝟙_ C)) X₃

Tactic:
assumption

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

Goal state before:
pp: case convert_4
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₂₃Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₂₃ X₁ ((single₀ I).obj (𝟙_ C)) X₃

Tactic:
assumption

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

Goal state before:
pp: case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₁

Tactic:
assumption

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

Goal state before:
pp: case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₂

Tactic:
assumption

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

Goal state before:
pp: case inst
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯).τ₃

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f' = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁

Tactic:
by
  let hi := (X.kernelSequenceCycles_exact f₁ f₂ _ _ hn₂).fIsKernel
  exact Fork.IsLimit.hom_ext hi (by simpa using! hi.fac _ .zero)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₂₄
⊢ MorphismProperty.monomorphisms C sq.f₂₄

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₃
⊢ MorphismProperty.epimorphisms C sq.f₁₃

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ h.i = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)

Tactic:
dsimp [h]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ h.right.p = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)

Tactic:
dsimp [h]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ∀ (P : C) (g : P ⟶ X.opcycles f₁ f₂₃ n₁),
    g ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ = 0 → g = 0

Tactic:
intro A x hx

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx : x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ = 0
⊢ x = 0
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 : L
f g : M →ₗ[R] N
n : M
⊢ { toFun := fun m ↦ ⁅x, (f + g) m⁆ - (f + g) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ ⁅x, g m⁆ - g ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      n

Tactic:
simp only [coe_mk, AddHom.coe_mk, lie_add, add_apply]

Goal state after:
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 : L
f g : M →ₗ[R] N
n : M
⊢ ⁅x, f n⁆ + ⁅x, g n⁆ - (f ⁅x, n⁆ + g ⁅x, n⁆) = ⁅x, f n⁆ - f ⁅x, n⁆ + (⁅x, g n⁆ - g ⁅x, n⁆)
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ x ∈ I

Tactic:
assumption

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₂
s : Set L
⊢ map f (lieSpan R L s) = lieSpan R L₂ (⇑f '' s)

Tactic:
refine le_antisymm ?_ (lieSpan_le.mpr <| Set.image_mono subset_lieSpan)

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₂
s : Set L
⊢ map f (lieSpan R L s) ≤ lieSpan R L₂ (⇑f '' s)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p

Tactic:
· intro h; use { p with lie_mem := @h }

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

Goal state before:
pp: case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ ↑N

pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N

Tactic:
· exact Subset.trans subset_lieSpan

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ comap N.incl N = ⊤

Tactic:
simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, top_toSubmodule]
  rw [Submodule.comap_subtype_self]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' < N ↔ N' < ⊤

Tactic:
convert! (LieSubmodule.mapOrderEmbedding (f := N.incl) Subtype.coe_injective).lt_iff_lt

Goal state after:
case e'_1.e'_4
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ N = (mapOrderEmbedding ⋯) ⊤
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (minpoly A x).degree ≤ p.degree

Tactic:
by
  delta minpoly; split_ifs with hx
  · refine le_of_not_gt <| degree_lt_wf.not_lt_min _ ?_
    exact ⟨pmonic, hp⟩
  · simp only [degree_zero, bot_le]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
g : F[X]
hg : map (algebraMap F E) g = minpoly E a
hgdeg : g.natDegree = (minpoly E a).natDegree
hgmon : g.Monic
⊢ (Polynomial.aeval a) (((mapRingHom (algebraMap E A)).comp (mapRingHom (algebraMap F E))) g) = 0

Tactic:
RingHom.comp_apply,

Goal state after:
F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
g : F[X]
hg : map (algebraMap F E) g = minpoly E a
hgdeg : g.natDegree = (minpoly E a).natDegree
hgmon : g.Monic
⊢ (Polynomial.aeval a) ((mapRingHom (algebraMap E A)) ((mapRingHom (algebraMap F E)) g)) = 0