mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

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₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
have : (w ≫ₕ w'.hom).op = (w.op ≫ᵥ w''.hom) := by ext; simp [w'']

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₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

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
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X Y : C
n : ℕ
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y n)

Tactic:
induction n generalizing Y with
  | zero => simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩
  | succ n hn =>
    let I : InjectivePresentation Y := Classical.arbitrary _
    let S := ShortComplex.mk _ _ (cokernel.condition I.f)
    have : Injective (S.map F).X₂ := Functor.PreservesInjectiveObjects.injective_obj I.injective
    have hS : S.ShortExact := { exact := ShortComplex.exact_cokernel I.f }
    exact AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact _ _ _ _
      (F.mapExtAddHom X S.X₂ n) (F.mapExtAddHom X S.X₃ n) (F.mapExtAddHom X S.X₁ (n + 1))
      (by cat_disch) (by cat_disch)
      ((ShortComplex.ab_exact_iff_function_exact _).mp
        (Ext.covariant_sequence_exact₃' X hS n (n + 1) rfl))
      ((ShortComplex.ab_exact_iff_function_exact _).mp
        (Ext.covariant_sequence_exact₃' (F.obj X) (hS.map F) n (n + 1) rfl))
      (hn _).surjective (hn _)
      (fun x₁ ↦ Ext.covariant_sequence_exact₁ _ hS x₁ (by subsingleton) rfl)
      (fun y₁ ↦ Ext.covariant_sequence_exact₁ _ (hS.map F) y₁ (by subsingleton) rfl)

Goal state after:
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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map
          ((CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
            (CochainComplex.mappingCone.triangle ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map S.f)).mor₃) ≫
        (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
rw [← CochainComplex.mappingCone.map_δ, Functor.map_comp_assoc,
    ← F.mapDerivedCategoryFactors_hom_naturality_assoc, Functor.map_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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      F.mapDerivedCategory.map ((Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      F.mapDerivedCategoryFactors.hom.app
          ((shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle S.f).obj₁) ≫
        Q.map ((Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
          (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (F.map X✝.d ≫ η.app X✝.obj) ≫ (shiftFunctor D 1).map (F.map f.f) = F.map f.f ≫ F.map Y✝.d ≫ η.app Y✝.obj

Tactic:
slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ F.map X✝.d ≫ (shiftFunctor C 1 ⋙ F).map f.f ≫ η.app Y✝.obj = F.map f.f ≫ F.map Y✝.d ≫ η.app Y✝.obj
Module: Mathlib.Algebra.Homology.Double

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

Tactic:
simp only [not_or] at h
    apply (isZero_double_X f hi₀₁ k h.1 h.2).eq_of_src

Goal state after:
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
n : S
X : DifferentialObject S C
⊢ { f := (CategoryTheory.shiftFunctor C n).map (𝟙 X).f, comm := ⋯ } =
    𝟙
      { obj := (CategoryTheory.shiftFunctor C n).obj X.obj,
        d := (CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom, d_squared := ⋯ }

Tactic:
ext1; dsimp; rw [Functor.map_id]

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

Goal state before:
pp: case pos
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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : k₀ = i₁
⊢ (if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
subst h₁
        dsimp
        rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]

Goal state after:
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₁ m₂ m₃ : S
X : DifferentialObject S C
⊢ (shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X ≫ (shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X) =
    eqToHom ⋯ ≫
      (shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)

Tactic:
ext1
        convert! shiftFunctorAdd_assoc_hom_app m₁ m₂ m₃ X.obj
        dsimp [shiftFunctorAdd']
        simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
this : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
have : Epi (hS.cokerToKer' k hk cc kf hcc hkf) :=
    hS.epi_cokerToKer' k hk cc kf hcc hkf (hS.exact (k + 1))

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
this✝ : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
this : Epi (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X)) =
    𝟙 ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution X).complex)

Tactic:
rw [← (HomotopyCategory.quotient _ _).map_id]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X)) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (𝟙 (projectiveResolution X).complex)
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 : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0

Tactic:
by_cases h₁ : c.Rel i₁ (c.next i₁)

Goal state after:
case pos
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 : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0

case neg
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 : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : ¬c.Rel i₁ (c.next i₁)
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    e.inv.app (X j) ≫
      (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫
        (F.map (φ j)).app ((single₀ I).obj Y 0) ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯

Tactic:
NatTrans.naturality_assoc

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    e.inv.app (X j) ≫
      (F.map (φ j)).app Y ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

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
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0

Tactic:
← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀),

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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ =
    X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

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
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A✝ : C
z₀ :
  A✝ ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A✝
w✝ : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
H : X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = X.pOpcycles f₁ f₂₃ n₁
⊢ z₁ ≫ X.pOpcycles f₁ f₂₃ n₁ = 0

Tactic:
← 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 ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A✝ : C
z₀ :
  A✝ ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A✝
w✝ : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
H : X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = X.pOpcycles f₁ f₂₃ n₁
⊢ z₁ ≫ X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
by
  rw [eventuallyConst_atTop]
  refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩
  · exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm
  · induction m, hm using Nat.le_induction with
    | base => rfl
    | succ m hm ihm => exact (h m hm).trans ihm

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

Goal state before:
pp: L : Type v
inst✝ : LieRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

Tactic:
rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]

Goal state after:
L : Type v
inst✝ : LieRing L
x y z : L
⊢ -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ ∃ b, x * b = 1

Tactic:
obtain ⟨n, y, hy⟩ := IsArtinian.exists_pow_succ_smul_dvd x (1 : R)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ ∃ b, x * b = 1
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
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
by
  constructor
  · rintro ⟨K, rfl⟩ _ _
    exact K.lie_mem'
  · intro h
    use { p with lie_mem' := h _ _ }

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

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K

Tactic:
· intro h' x y hx hy; exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy

Goal state after:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
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
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
⊢ ∀ {x y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s

Tactic:
intro x y hx hy

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : x ∈ span R s
hy : y ∈ span R s
⊢ ⁅x, y⁆ ∈ span R s
Module: Mathlib.Algebra.Lie.IdealOperations

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✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N

Tactic:
rintro m' ⟨⟨x, hx⟩, ⟨n, hn⟩, hm⟩

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
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ m' ∈ ↑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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
have := Submodule.coe_iSup_of_directed _ hdir.directed_val

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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ x, ↑↑x) = ⋃ i, ↑↑↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N
Module: Mathlib.Algebra.Lie.Abelian

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
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ ⁅x, ↑f⁆ m = 0

Tactic:
f.property x,

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
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ 0 m = 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = minpoly A x

Tactic:
rw [hr]

Goal state after:
case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = p * r
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [comap_bracket_incl]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆