mathlib-initiative/mathlib-tactics huggingface dataset:
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 (Q.map ((F.mapCochainComplexSingleFunctor 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:
dsimp% triangleOfSESδ_naturality h1 h2
      (S.mapNatTrans (F.mapCochainComplexSingleFunctor 0).hom),

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₃) ≫
      Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app S.X₃) ≫ triangleOfSESδ h2 =
    𝟙 (((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.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✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 ⋯
      (((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
        (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.map
            ((CochainComplex.singleFunctor C 0).map f) ≫
          ((F.mapCochainComplexSingleFunctor 0).app Y).hom) =
    SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 mk₀._proof_1
      ((CochainComplex.singleFunctor D 0).map (F.map f))

Tactic:
congr

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✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
      (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.map
          ((CochainComplex.singleFunctor C 0).map f) ≫
        ((F.mapCochainComplexSingleFunctor 0).app Y).hom =
    (CochainComplex.singleFunctor D 0).map (F.map f)
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Tactic:
congr

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: case e_a.e_a
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app { X := P.X, p := 𝟙 P.X, idem := ⋯ } =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app ((toKaroubi C).obj P.X)

Tactic:
congr

Goal state after:
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✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift (f ≫ g) (projectiveResolution X✝) (projectiveResolution Z✝)) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
        (ProjectiveResolution.lift f (projectiveResolution X✝) (projectiveResolution Y✝)) ≫
      (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
        (ProjectiveResolution.lift g (projectiveResolution Y✝) (projectiveResolution Z✝))

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

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift (f ≫ g) (projectiveResolution X✝) (projectiveResolution Z✝)) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift f (projectiveResolution X✝) (projectiveResolution Y✝) ≫
        ProjectiveResolution.lift g (projectiveResolution Y✝) (projectiveResolution Z✝))
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom) =
    X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯)

Tactic:
congr

Goal state after:
case e'_2
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom =
    homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: 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₃
⊢ (associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom = tensorHom (rightUnitor X₁).hom (𝟙 X₃)

Tactic:
by
  convert!
    mapBifunctor_triangle (curriedAssociatorNatIso C) (𝟙_ C) (rightUnitorNatIso C)
      (leftUnitorNatIso C) (triangleIndexData I) X₁ X₃ (by simp)
  all_goals assumption

Goal state after:
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₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
⊢ π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = z₂ ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)

Tactic:
← reassoc_of% dsimp% hz₂,

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₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
⊢ π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = π₂ ≫ z₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
f : α → β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (∃ i, p i ∧ (f '' s i).Subsingleton) ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y

Tactic:
by simp only [Set.Subsingleton, forall_mem_image]

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₀ 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₂
⊢ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫
      X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ =
    0

Tactic:
rw [← cancel_epi (X.pOpcycles ..), comp_zero,
    p_opcyclesMap_assoc _ _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)]
  simp

Goal state after:
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
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ Submodule S M ↪o Submodule R M

Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ Submodule S M → Submodule R M

case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ Function.Injective ?refine_1

case refine_3
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ ∀ {a b : Submodule S M},
    { toFun := ?refine_1, inj' := ?refine_2 } a ≤ { toFun := ?refine_1, inj' := ?refine_2 } b ↔ a ≤ b
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L : Type u_1
inst✝ : LieRing L
toModule✝¹ : Module ℚ L
h₁ : ∀ (t : ℚ) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆
toModule✝ : Module ℚ L
h₂ : ∀ (t : ℚ) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆
heq : { toModule := toModule✝¹, lie_smul := h₁ }.toModule = { toModule := toModule✝, lie_smul := h₂ }.toModule
⊢ { toModule := toModule✝¹, lie_smul := h₁ } = { toModule := toModule✝, lie_smul := h₂ }

Tactic:
congr

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
t : R
x m : L
⊢ -(t • ⁅m, x⁆) = t • -⁅m, x⁆

Tactic:
smul_neg

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
t : R
x m : L
⊢ -(t • ⁅m, x⁆) = -(t • ⁅m, x⁆)
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
x✝² : L₁ →ₗ⁅R⁆ L₂
x✝¹ : R
x✝ : L₁
⊢ ↑x✝² (x✝¹ • x✝) = (RingHom.id R) x✝¹ • ↑x✝² x✝

Tactic:
map_smulₛₗ

Goal state after:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
x✝² : L₁ →ₗ⁅R⁆ L₂
x✝¹ : R
x✝ : L₁
⊢ (RingHom.id R) x✝¹ • ↑x✝² x✝ = (RingHom.id R) x✝¹ • ↑x✝² x✝
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L₁ → L₂
map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : L₁),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x y : L₁},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun x,
        { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun y⁆
g : L₁ → L₂
map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : L₁),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x y : L₁},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun x,
        { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun y⁆
h :
  ⇑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    ⇑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L₂
⊢ ∀ {y : L₂}, ((↑f).inverse g h₁ h₂).toFun ⁅x, y⁆ = ⁅((↑f).inverse g h₁ h₂).toFun x, ((↑f).inverse g h₁ h₂).toFun y⁆

Tactic:
y

Goal state after:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : L₂
⊢ ((↑f).inverse g h₁ h₂).toFun ⁅x, y⁆ = ⁅((↑f).inverse g h₁ h₂).toFun x, ((↑f).inverse g h₁ h₂).toFun y⁆
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h : Bijective ⇑f
x : L₁
⊢ ∀ {y : L₁}, f ⁅x, y⁆ = ⁅f x, f y⁆

Tactic:
y

Goal state after:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h : Bijective ⇑f
x y : L₁
⊢ f ⁅x, y⁆ = ⁅f x, f y⁆
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M →ₗ⁅R,L⁆ N
x✝¹ : R
x✝ : M
⊢ ↑x✝² (x✝¹ • x✝) = (RingHom.id R) x✝¹ • ↑x✝² x✝

Tactic:
map_smulₛₗ

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M →ₗ⁅R,L⁆ N
x✝¹ : R
x✝ : M
⊢ (RingHom.id R) x✝¹ • ↑x✝² x✝ = (RingHom.id R) x✝¹ • ↑x✝² x✝
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✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M → N
map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : M),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x : L} {m : M},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆
g : M → N
map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : M),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x : L} {m : M},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆
h :
  ⇑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    ⇑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }

Tactic:
congr

Goal state after:
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₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
            n₀ n₁ n₂ hn₁' ⋯ ⋯).right.homologyIso.hom =
    (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
            n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso.hom

Tactic:
simp [ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ IsNilpotent (Ring.jacobson R)

Tactic:
have hn : Jac * Jac ^ n = Jac ^ n := by
      rw [← Ideal.IsTwoSided.pow_succ]; exact (hn _ n.le_succ).symm

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
⊢ IsNilpotent (Ring.jacobson R)