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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ ∃ X_1 Y,
    ∃ (_ : ∃ K x, K.IsStrictlyLE 0) (_ : ∃ K x, K.IsStrictlyGE 1), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
refine ⟨Q.obj (K.truncLE 0), Q.obj (K.truncGE 1),
      ⟨_, Iso.refl _, inferInstance⟩, ⟨_, Iso.refl _, inferInstance⟩,
      Q.map (K.ιTruncLE 0) ≫ e₂.hom, e₂.inv ≫ Q.map (K.πTruncGE 1),
      inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by lia))) ≫ (triangleOfSES h).mor₃,
      isomorphic_distinguished _ (triangleOfSES_distinguished h) _ (Iso.symm ?_)⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ triangleOfSES h ≅
    Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
      (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
        (triangleOfSES h).mor₃)
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ sq.HasLift

Tactic:
have w : (s ≫ u) ≫ g' = f ≫ (t ≫ v) := by
      rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
    exact ⟨h.desc u (CommSq.mk w).lift (by rw [CommSq.fac_left]), h.inl_desc ..,
      h.hom_ext (by rw [h.inl_desc_assoc, sq.w]) (by rw [h.inr_desc_assoc, CommSq.fac_right])⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ (δ m n (n.negOnePow • f.rightUnshift m ⋯)).rightShift n 0 ⋯ = (↑z).rightShift n 0 ⋯

Tactic:
rw [← hφ, hf, δ_units_smul, Cochain.rightShift_units_smul,
    Cochain.δ_rightUnshift _ _ _ _ 0 (by simp)]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ n.negOnePow • (n.negOnePow • (δ (-1) 0 f).rightUnshift n ⋯).rightShift n 0 ⋯ = δ (-1) 0 f
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty Cᵒᵖ
inst✝ : A.IsVerdierLeftLocalizing B
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hX : B.unop X✝
hY : A.unop Y✝
⊢ ∃ Z a b, A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierLeftLocalizing.fac f.op hY hX
    exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ t.IsLE ((t.truncLT n₁).obj Y) n₀

Tactic:
subst hn

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ : ℤ
hf : IsIso ((t.truncGE (n₀ + 1)).map g)
⊢ t.IsLE ((t.truncLT (n₀ + 1)).obj Y) n₀
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ (i ≫ l.homOf).f n = t.f n

Tactic:
have h₁ : i.f n ≫ π.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hπ]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
h₁ : i.f n ≫ π.f n = 0
⊢ (i ≫ l.homOf).f n = t.f n
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ LeftHomotopyClass.mk x✝¹ = LeftHomotopyClass.mk x✝

Tactic:
LeftHomotopyClass.mk_eq_mk_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ LeftHomotopyRel x✝¹ x✝
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n : ℤ
this✝¹ : IsIso ((S f n).homologyπ n)
this✝ : Mono (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
this : IsIso (homologyπ ((cokernel f).truncGE n) n)
⊢ Mono (homologyMap (p f n) n)

Tactic:
rw [← IsIso.inv_hom_id_assoc ((truncGE (cokernel f) n).homologyπ n) (homologyMap (p f n) n)]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n : ℤ
this✝¹ : IsIso ((S f n).homologyπ n)
this✝ : Mono (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
this : IsIso (homologyπ ((cokernel f).truncGE n) n)
⊢ Mono (inv (homologyπ ((cokernel f).truncGE n) n) ≫ homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ 𝟙 T.X₂ ≫ homologyMap (α f n) n = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n

Tactic:
Category.id_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ homologyMap (α f n) n = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ ∀ (X₂ : D₁), ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C₃
inst✝⁵ : Category.{v_4, u_4} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
inst✝³ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst✝² : R₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ᵥ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C₃
inst✝⁵ : Category.{v_4, u_4} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
inst✝³ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst✝² : R₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ᵥ w').GuitartExact
⊢ ∀ (X₂ : D₂), (w'.structuredArrowDownwards X₂).Initial
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝² : L.IsEquivalence
inst✝¹ : R.IsEquivalence
inst✝ : IsIso w.natTrans
⊢ w.GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝² : L.IsEquivalence
inst✝¹ : R.IsEquivalence
inst✝ : IsIso w.natTrans
⊢ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
pf✝⁷ : HasZeroObject C
pf✝⁶ : IsRightCancelAdd ℤ
pf✝⁵ : IsRightCancelAdd ℤ
pf✝⁴ : F.PreservesZeroMorphisms
pf✝³ : (HomologicalComplex.single C (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
pf✝² : (F.mapHomologicalComplex (ComplexShape.up ℤ)).PreservesZeroMorphisms
h1 :
  ((S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)).map
      (F.mapHomologicalComplex (ComplexShape.up ℤ))).ShortExact
pf✝¹ : HasZeroObject D
pf✝ : (HomologicalComplex.single D (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
h2 : ((S.map F).map (HomologicalComplex.single D (ComplexShape.up ℤ) 0)).ShortExact
⊢ Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app S.X₃) ≫
      triangleOfSESδ h1 ≫
        (shiftFunctor (DerivedCategory D) 1).map
            (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)) ≫
          𝟙 ((shiftFunctor (DerivedCategory D) 1).obj (F.mapDerivedCategory.obj ((singleFunctor C 0).obj S.X₁))) ≫
            (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    𝟙 (((singleFunctors D).functor 0).obj (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫ (shiftFunctor (DerivedCategory D) 1).map (𝟙 ((singleFunctor D 0).obj (F.obj S.X₁)))

Tactic:
Category.id_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
pf✝⁷ : HasZeroObject C
pf✝⁶ : IsRightCancelAdd ℤ
pf✝⁵ : IsRightCancelAdd ℤ
pf✝⁴ : F.PreservesZeroMorphisms
pf✝³ : (HomologicalComplex.single C (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
pf✝² : (F.mapHomologicalComplex (ComplexShape.up ℤ)).PreservesZeroMorphisms
h1 :
  ((S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)).map
      (F.mapHomologicalComplex (ComplexShape.up ℤ))).ShortExact
pf✝¹ : HasZeroObject D
pf✝ : (HomologicalComplex.single D (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
h2 : ((S.map F).map (HomologicalComplex.single D (ComplexShape.up ℤ) 0)).ShortExact
⊢ Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app S.X₃) ≫
      triangleOfSESδ h1 ≫
        (shiftFunctor (DerivedCategory D) 1).map
            (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)) ≫
          (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    𝟙 (((singleFunctors D).functor 0).obj (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫ (shiftFunctor (DerivedCategory D) 1).map (𝟙 ((singleFunctor D 0).obj (F.obj S.X₁)))
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
inst✝ : Projective Z
n✝ : ℕ
⊢ Projective (((single₀ C).obj Z).X (n✝ + 1))

Tactic:
apply IsZero.projective

Goal state after:
case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
inst✝ : Projective Z
n✝ : ℕ
⊢ IsZero (((single₀ C).obj Z).X (n✝ + 1))
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

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✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (F.leftDerived n).map f ≫ (Q.isoLeftDerivedObj F n).hom =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        φ

Tactic:
dsimp [isoLeftDerivedObj, Functor.leftDerived]
  rw [assoc, ← Functor.map_comp_assoc,
    ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality f P Q φ comm F,
    Functor.map_comp, assoc]
  erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.naturality]
  rfl

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 ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
⊢ 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ

Tactic:
Category.id_comp,

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 ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
⊢ (X.H n).map φ = 0 ≫ (X.H n).map φ
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ ((Injective fun x_1 ↦ x_1 * x) ∧ Surjective fun x_1 ↦ x_1 * x) ↔ Injective fun x_1 ↦ x_1 * x

Tactic:
and_iff_left_of_imp

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ (Injective fun x_1 ↦ x_1 * x) ↔ Injective fun x_1 ↦ x_1 * x

R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ (Injective fun x_1 ↦ x_1 * x) → Surjective fun x_1 ↦ x_1 * x
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
S : Set (LieSubmodule R L M)
⊢ sInf (toSubmodule '' S) = ⨅ N ∈ S, ↑N

Tactic:
sInf_image

Goal state after:
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 (LieSubmodule R L M)
⊢ ⨅ a ∈ S, ↑a = ⨅ N ∈ S, ↑N
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_1.refine_2
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := ⋯
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅↑x, ⁅y, ↑n⁆⁆ ∈ s

Tactic:
· use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩

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

Goal state before:
pp: case a
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ↑(lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x})

Tactic:
apply submodule_span_le_lieSpan

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
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ map f ⊤

Tactic:
exact LieSubmodule.map_mono le_top

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' ≤ map N.incl ⊤

Tactic:
exact LieSubmodule.map_mono le_top

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

Goal state before:
pp: A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ minpoly K x ∣ map (algebraMap A K) (minpoly A x)

Tactic:
refine minpoly.dvd K x ?_
  rw [aeval_map_algebraMap, minpoly.aeval]

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

Goal state before:
pp: case inr
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) g = 0
⊢ False

Tactic:
· refine aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, ?_⟩ heval
    rw [mul_comm, he]

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
⊢ b ^ m ≠ a

Tactic:
have hn : n ≠ 0 := fun e ↦ not_irreducible_C
    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)
  obtain ⟨k, rfl⟩ := hm
  rintro rfl
  obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
  rw [mul_comm, pow_mul, map_pow, hq] at H
  have : degree q = 0 := by
    simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 rfl
  apply_fun degree at hq
  simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
    Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
    Nat.cast_injective.eq_iff] at hq
  exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases eq_or_ne r 0 with (rfl | hr)
    · exact .inl (by simpa using h)
    · exact .inr ((squarefree_iff_no_irreducibles hr).mpr h)
  · rintro (⟨rfl, h⟩ | h)
    · simpa using h
    intro x hx t
    exact hx.not_isUnit (h x t)

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
x : R
⊢ f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)

Tactic:
apply_fun (frobeniusEquiv S p)

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
x : R
⊢ (frobeniusEquiv S p) (f ((frobeniusEquiv R p).symm x)) = (frobeniusEquiv S p) ((frobeniusEquiv S p).symm (f x))
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →+* S
x : R
⊢ f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)

Tactic:
apply_fun (frobeniusEquiv S p)

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →+* S
x : R
⊢ (frobeniusEquiv S p) (f ((frobeniusEquiv R p).symm x)) = (frobeniusEquiv S p) ((frobeniusEquiv S p).symm (f x))
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree * 1 < N.succ

Tactic:
← hg1

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree * 1 < g.natDegree * p
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
by
  have H := roots_expand_pow (p := p) (n := n) (f := X - C y)
  rwa [roots_X_sub_C, Multiset.map_singleton, map_sub, expand_X, expand_C] at H

Goal state after: