mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ : ι
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ 0 =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
double_d_eq_zero₀ _ _ _ _ h.symm,

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

Goal state before:
pp: case h₁
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₁
X : C
K : HomologicalComplex C c
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ ((fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯) ((fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀) g)).f i₁ =
    g.f i₁

Tactic:
· simp [double_d _ _ h]

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
⊢ { f := fun i ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ } =
    { f := fun i ↦ (C.X i).map h₁, comm' := ⋯ } ≫ { f := fun i ↦ (C.X i).map h₂, comm' := ⋯ }

Tactic:
by
    ext i
    dsimp
    rw [Functor.map_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
emb : (K ⟶ L) → (i : Shrink.{w, t} ι) → Shrink.{w, v} (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i)) :=
  fun f i ↦ (equivShrink (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i))) (f.f ((equivShrink ι).symm i))
f g : K ⟶ L
h : emb f = emb g
⊢ f = g

Tactic:
by
      ext i
      obtain ⟨i, rfl⟩ := (equivShrink.{w} _).symm.surjective i
      simpa [emb] using congr_fun h i

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f

Tactic:
have h'' := F.congr_map (p_comp f)

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
h'' : F.map (x✝¹.p ≫ f.f) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ } ⟶
  { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ } :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.X₂,
    τ₃ := 𝟙 { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.Exact

Tactic:
ShortComplex.exact_iff_of_epi_of_isIso_of_mono α

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ } ⟶
  { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ } :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.X₂,
    τ₃ := 𝟙 { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }.Exact
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 : GradedObject J D
inst✝ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j ⋯ ≫ (mapBifunctorRightUnitor F Y e p hp X).hom j =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)

Tactic:
by
  dsimp [mapBifunctorRightUnitor]
  erw [CofanMapObjFun.ιMapObj_iso_inv]
  rw [mapBifunctorRightUnitorCofan_inj]

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
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex C c
⊢ (α_ K₁ K₂ K₃).hom.f = 𝟙 ((K₁ ⊗ K₂).X ⊗ K₃.X) ≫ 𝟙 (K₁.X ⊗ K₂.X) ▷ K₃.X ≫ (α_ K₁.X K₂.X K₃.X).hom

Tactic:
id_whiskerRight

Goal state after:
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
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex C c
⊢ (α_ K₁ K₂ K₃).hom.f = 𝟙 ((K₁ ⊗ K₂).X ⊗ K₃.X) ≫ 𝟙 ((K₁ ⊗ K₂).X ⊗ K₃.X) ≫ (α_ K₁.X K₂.X K₃.X).hom
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
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + (i₂ + i₃ + i₄) = j

Tactic:
rw [← h, ← add_assoc, ← add_assoc]

Goal state after:
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
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
⊢ tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫
      (associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom =
    (associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom

Tactic:
← cancel_epi (associator (tensorObj X₁ X₂) X₃ X₄).inv,

Goal state after:
I : Type u
inst✝²⁵ : AddMonoid I
C : Type u_1
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
⊢ (associator (tensorObj X₁ X₂) X₃ X₄).inv ≫
      tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫
        (associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom =
    (associator (tensorObj X₁ X₂) X₃ X₄).inv ≫
      (associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁

Tactic:
rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]

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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)) (asIso f) ⋯
h : (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) = 0
⊢ IsZero ((X.H n).obj (mk₁ (𝟙 i)))

Tactic:
rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← 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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)) (asIso f) ⋯
h : (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) = 0
⊢ (X.H n).map (𝟙 (mk₁ (𝟙 i))) = (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)
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.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = X.iCycles f₁ f₂ n₁ ≫ X.pOpcycles f₂ f₃ n₁

Tactic:
simp [πE, ιE]

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq' : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
⊢ i₁ ≤ i₂

Tactic:
by
  simpa only [hi₁, hi₂] using data.le₁₂ pq'

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
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
by
  rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A x₂ hx₂
  dsimp at x₂ hx₂
  obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    (X.kernelSequenceOpcyclesE_exact f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).exact_up_to_refinements
      (X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ (by simpa using hx₂ =≫ biprod.fst)) (by
        dsimp
        rw [← X.fromOpcyles_δ f₁ f₂ f₃ f₂₃ h₂₃ n₁ n₂,
          X.liftOpcycles_fromOpcycles_assoc]
        simpa using hx₂ =≫ biprod.snd)
  dsimp at x₁ hx₁
  refine ⟨A₁, π₁, inferInstance, x₁, ?_⟩
  dsimp
  rw [← reassoc_of% hx₁, liftOpcycles_fromOpcycles]

Goal state after:
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
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L N
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
x : L
m : M
n : N
⊢ ⁅x, (f m) n⁆ = (f ⁅x, m⁆) n + (f m) ⁅x, n⁆

Tactic:
by simp only [sub_add_cancel, map_lie, LieHom.lie_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
⊢ iInf PrimeSpectrum.asIdeal ^ n = ∏ i, i.asIdeal ^ n

Tactic:
Finset.prod_pow,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
⊢ iInf PrimeSpectrum.asIdeal ^ n = (∏ x, x.asIdeal) ^ n
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a

Tactic:
rw [← mul_assoc, ← mul_assoc]

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₂
x y : L
⊢ ⁅↑f x, ↑f y⁆ ∈ (↑f).range.carrier

Tactic:
exact ⟨⁅x, y⁆, f.map_lie x y⟩

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 = ⊥ ↔ N = ⊥

Tactic:
← toSubmodule_inj,

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 : LieSubmodule R L M
⊢ ↑N = ⊥ ↔ ↑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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥

Tactic:
← toSubmodule_inj,

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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ ↑{ toSubmodule := N, lie_mem := h } = ↑⊥ ↔ 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
⊢ ↑N = ⊤ ↔ N = ⊤

Tactic:
← toSubmodule_inj,

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 : LieSubmodule R L M
⊢ ↑N = ⊤ ↔ ↑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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤

Tactic:
← toSubmodule_inj,

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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ ↑{ toSubmodule := N, lie_mem := h } = ↑⊤ ↔ N = ⊤
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_3
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 := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m₁ : M
⊢ ∀ (y_1 : M),
    m₁ ∈ Submodule.span R s →
      y_1 ∈ Submodule.span R s →
        ⁅y, m₁⁆ ∈ Submodule.span R s → ⁅y, y_1⁆ ∈ Submodule.span R s → ⁅y, m₁ + y_1⁆ ∈ Submodule.span R s

Tactic:
m₂

Goal state after:
case refine_3
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 := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m₁ m₂ : M
⊢ m₁ ∈ Submodule.span R s →
    m₂ ∈ Submodule.span R s →
      ⁅y, m₁⁆ ∈ Submodule.span R s → ⁅y, m₂⁆ ∈ Submodule.span R s → ⁅y, m₁ + m₂⁆ ∈ Submodule.span R s
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I ≤ ⊥

Tactic:
exact h₂

Goal state after:
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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
lieIdeal_oper_eq_linear_span

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 : 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} = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = 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
N N' : LieSubmodule R L M
⊢ ↑N ⊓ ↑N' = ⊥ ↔ N ⊓ N' = ⊥

Tactic:
← toSubmodule_inj,

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
⊢ ↑N ⊓ ↑N' = ⊥ ↔ ↑(N ⊓ 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 N' : LieSubmodule R L M
⊢ ↑N ⊔ ↑N' = ⊤ ↔ N ⊔ N' = ⊤

Tactic:
← toSubmodule_inj,

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
⊢ ↑N ⊔ ↑N' = ⊤ ↔ ↑(N ⊔ N') = ↑⊤
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case left
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 : LieIdeal R L
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
apply mono_lie_right

Goal state after:
case left
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 : LieIdeal R L
⊢ N ≤ N ⊔ N'
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case right
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 : LieIdeal R L
⊢ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
apply mono_lie_right

Goal state after:
case right
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 : LieIdeal R L
⊢ N' ≤ N ⊔ 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
⊢ ⊥ = ⊤ ↔ ⊥ = ⊤

Tactic:
← toSubmodule_inj,

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
⊢ ↑⊥ = ↑⊤ ↔ ⊥ = ⊤
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : 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
I : LieIdeal R L
⊢ ⁅I, maxTrivSubmodule R L M⁆ = ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span,
    LieSubmodule.bot_toSubmodule, Submodule.span_eq_bot]
  rintro m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩
  exact hm x

Goal state after: