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₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ (w ≫ₕ w').GuitartExact

Tactic:
← guitartExact_op_iff

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₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ (w ≫ₕ w').op.GuitartExact
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this✝ : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
  (T.functor.associator R.functor W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor.associator B.functor W₂'.Q ≪≫ L.functor.isoWhiskerLeft e' ≪≫ (L.functor.associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
this : TwoSquare.hComp iso.inv e'.inv = e.inv
⊢ TwoSquare.GuitartExact e.inv

Tactic:
← this

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this✝ : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
  (T.functor.associator R.functor W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor.associator B.functor W₂'.Q ≪≫ L.functor.isoWhiskerLeft e' ≪≫ (L.functor.associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
this : TwoSquare.hComp iso.inv e'.inv = e.inv
⊢ (TwoSquare.hComp iso.inv e'.inv).GuitartExact
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
⊢ ∀ (i : ℤ), autoParam (i < -d) isStrictlyGE_iff._auto_1 → IsZero (L.X i)

Tactic:
intro i hi

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ IsZero (L.X i)
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (match Int.negSucc 0 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n) ≫
      h'.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1) =
    h.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1) ≫
      match Int.negSucc 0 + 1 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n

Tactic:
simpa

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

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

Tactic:
ext : 1
  exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_precomp])

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ IsColimit P.cokernelCofork

Tactic:
refine IsColimit.ofIsoColimit (P.complex.opcyclesIsCokernel 1 0 (by simp)) ?_
  refine Cofork.ext (P.complex.isoHomologyι₀.symm ≪≫ isoOfQuasiIsoAt P.π 0 ≪≫
    singleObjHomologySelfIso _ _ _) ?_
  rw [← cancel_mono (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _).inv,
    ← cancel_mono (isoHomologyι₀ _).hom]
  dsimp
  simp only [isoHomologyι₀_inv_naturality_assoc, p_opcyclesMap_assoc, single₀_obj_zero, assoc,
    Iso.hom_inv_id, comp_id, isoHomologyι_inv_hom_id, singleObjHomologySelfIso_inv_homologyι,
    singleObjOpcyclesSelfIso_hom, single₀ObjXSelf, Iso.refl_inv, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

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

Tactic:
simpa

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

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

Tactic:
simpa

Goal state after:
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'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m = e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩

Tactic:
rw [← hm ⟨⟨j, 0⟩, hp j⟩, mapBifunctorRightUnitorCofan_inj, assoc, ← Functor.map_comp_assoc,
        Iso.inv_hom_id, Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]

Goal state after:
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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ X.toCycles f g fg h n ≫ X.cyclesMap f g f' g' α n = (X.H n).map β ≫ X.toCycles f' g' fg' h' n

Tactic:
by
  rw [← cancel_mono (X.iCycles f' g' n), Category.assoc, Category.assoc, toCycles_i,
    X.cyclesMap_i f g f' g' α (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n rfl,
    toCycles_i_assoc, ← Functor.map_comp, ← Functor.map_comp]
  congr 1
  ext
  · dsimp
    rw [hβ₀]
    exact naturality' α 0 1
  · dsimp
    rw [hβ₁, Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
by
  apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
  · dsimp
    convert! (inferInstance : Epi ((X.H n₀).map (𝟙 _)))
    cat_disch
  · dsimp
    convert! (inferInstance : IsIso ((X.H n₁).map (𝟙 _)))
    cat_disch
  · exact (X.exact₂ f₂ f₃ f₂₃ h₂₃ n₂).mono_g h

Goal state after:
Module: Mathlib.Order.Fin.Clamp

Goal state before:
pp: n m : ℕ
hmn : m ≤ n
⊢ ↑(clamp n m) = ↑(last m)

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.WithBotTop

Goal state before:
pp: ι : Type u_1
inst✝ : Preorder ι
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
⊢ coe x✝² ≤ coe x✝¹

Tactic:
simpa

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₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ (parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).map
        WalkingParallelPairHom.left ≫
      (Iso.refl
          ((parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.one)).hom =
    (Iso.refl
          ((parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.zero)).hom ≫
      (parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) 0).map WalkingParallelPairHom.left

Tactic:
simpa

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₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ (parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).map
        WalkingParallelPairHom.left ≫
      (Iso.refl
          ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
            WalkingParallelPair.one)).hom =
    (Iso.refl
          ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
            WalkingParallelPair.zero)).hom ≫
      (parallelPair (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) 0).map WalkingParallelPairHom.left

Tactic:
simpa

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₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
⊢ i₃ ≤ i₃'

Tactic:
by
  simpa only [hi₃, hi₃'] using data.monotone_i₃ r r' 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
hβ : β = homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv ≫
      ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) =
    X.cyclesMap f₁ f₂ f₁' f₂' β n₁ ≫ (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv

Tactic:
subst hβ
  simp [← cancel_mono (ShortComplex.iCycles _), cyclesMap_i]

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

Tactic:
simpa [← cancel_epi (X.pOpcycles f₁₂ f₃ n₁)] using (X.p_opcyclesMap ..).symm

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

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
⊢ coreE₂HomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe (coreE₂HomologicalNat.deg (p, q) + 1)

Tactic:
simp only [coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_deg, WithBotTop.coe_le_coe]

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
⊢ -↑q - r + 2 ≤ -↑p - ↑q + 1
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
rw [← cancel_epi (X.cyclesIsoH f n₁ n₂ hn₂).inv,
    cyclesIsoH_inv .., cyclesIsoH_inv_hom_id_assoc ..]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
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.pOpcycles f₁ f₂₃ n₁ ≫ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯).f =
    (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).f ≫
      𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂

Tactic:
dsimp
        rw [Category.comp_id, X.p_opcyclesMap _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂)]

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

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
inst✝ : IsFaithful R L M
L' : LieSubalgebra R L
⊢ Injective (⇑(toEnd R L M) ∘ Subtype.val)

Tactic:
exact IsFaithful.injective_toEnd.comp Subtype.val_injective

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
s✝ s : Set L
x : L
hx : x ∈ lieSpan R L (-s)
⊢ x ∈ lieSpan R L s

Tactic:
induction hx using lieSpan_induction with

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
s : Set L
x u : L
hu : u ∈ s
⊢ ⟨u, ⋯⟩ ∈ Subtype.val ⁻¹' s

Tactic:
simpa

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
s : Set L
x : L
hx : x ∈ lieSpan R L s
⊢ ⟨x, hx⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
induction hx using lieSpan_induction with

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

Goal state before:
pp: case h
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'
h : f.range = ⊤
⊢ ↑⊤ = ⊤

Tactic:
exact LieSubmodule.top_toSubmodule

Goal state after:
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
⊢ ∀ (x y_1 : M),
    x ∈ Submodule.span R s →
      y_1 ∈ Submodule.span R s →
        ⁅y, x⁆ ∈ Submodule.span R s → ⁅y, y_1⁆ ∈ Submodule.span R s → ⁅y, x + y_1⁆ ∈ Submodule.span R s

pp: case refine_4
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
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
⊢ ∀ (a : R), ∀ x ∈ Submodule.span R s, ⁅y, x⁆ ∈ Submodule.span R s → ⁅y, a • x⁆ ∈ Submodule.span R s

Tactic:
· intro m₁ m₂ _ _ hm₁ hm₂; rw [lie_add]; exact Submodule.add_mem _ hm₁ hm₂

Goal state after:
case refine_4
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
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
⊢ ∀ (a : R), ∀ x ∈ Submodule.span R s, ⁅y, x⁆ ∈ Submodule.span R s → ⁅y, a • x⁆ ∈ Submodule.span R s
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x : L
hx : x ∈ lieSpan R L s
y : L
hy : y ∈ lieSpan R L s
⊢ ⁅⟨x, hx⟩, ⟨y, hy⟩⁆ = 0

Tactic:
induction hx using lieSpan_induction with

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

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x : L
hx : x ∈ lieSpan R L s
y : L
hy : y ∈ lieSpan R L s
⊢ ⁅⟨x, hx⟩, ⟨y, hy⟩⁆ = 0

Tactic:
· induction hx using lieSpan_induction with
    | mem w hw =>
      induction hy using lieSpan_induction with
      | mem u hu => simpa [Subtype.ext_iff] using h w hw u hu
      | zero => simp [Subtype.ext_iff]
      | add u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢
        simp [hu, hv]
      | smul t u _ hu =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
        simp [Subtype.ext_iff, hu]
      | lie u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
        rw [leibniz_lie]
        simp [hu, hv]
    | zero => simp [Subtype.ext_iff]
    | add u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] at hu hv ⊢
      simp [hu, hv]
    | smul t u _ hu =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
      simp [Subtype.ext_iff, hu]
    | lie u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
      simp [hu, hv]

Goal state after:
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
⊢ 0 m = 0

Tactic:
LinearMap.zero_apply

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ 0 = 0