mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

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
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
hf : W f
⊢ IsIso ((Quotient.functor L.homRel).map f)

Tactic:
have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
hf : W f
this : IsIso (F.map ((Quotient.functor L.homRel).map f))
⊢ IsIso ((Quotient.functor L.homRel).map f)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ P T.obj₁ ∧ P T.obj₃

Tactic:
obtain ⟨e, _⟩ := t.triangle_iso_exists hT
    (P.ι.map_distinguished _ ((P.tStructure t).triangleLEGE_distinguished n₀ n₁ h ⟨_, h₂⟩))
    (Iso.refl _) n₀ n₁ inferInstance inferInstance
      (by dsimp; rw [← P.tStructure_isLE_iff]; infer_instance)
      (by dsimp; rw [← P.tStructure_isGE_iff]; infer_instance)

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
e : T ≅ P.ι.mapTriangle.obj (((P.tStructure t).triangleLEGE n₀ n₁ h).obj { obj := T.obj₂, property := h₂ })
h✝ : e.hom.hom₂ = (Iso.refl T.obj₂).hom
⊢ P T.obj₁ ∧ P T.obj₃
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
P✝ : ObjectProperty C
t✝ : TStructure C
inst✝⁶ : P✝.IsTriangulated
h : P✝.HasInducedTStructure t✝
P P' : ObjectProperty C
inst✝⁵ : P.IsTriangulated
inst✝⁴ : P'.IsTriangulated
t : TStructure C
inst✝³ : P.HasInducedTStructure t
inst✝² : P'.HasInducedTStructure t
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ (P ⊓ P') ((t.truncLE n).obj X) ∧ (P ⊓ P') ((t.truncGE n).obj X)

Tactic:
exact
      ⟨⟨(P.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished n _ rfl X) n _ rfl
          (by dsimp; infer_instance) hX (by dsimp; infer_instance)).1,
        (P'.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished n _ rfl X) n _ rfl
          (by dsimp; infer_instance) hX' (by dsimp; infer_instance)).1⟩,
          ⟨(P.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished (n - 1) n (by lia) X)
          (n - 1) n (by lia) (by dsimp; infer_instance) hX (by dsimp; infer_instance)).2,
        (P'.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished (n - 1) n (by lia) X)
          (n - 1) n (by lia) (by dsimp; infer_instance) hX' (by dsimp; infer_instance)).2⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g

Tactic:
by
      have := coprod.inr ≫= sq.fac_left
      rw [Q.inr_i_assoc, coprod.inr_desc] at this
      simp [reassoc_of% this, P]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ModelCategory C
X Y : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ ∃ g, RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
by
  obtain ⟨g, hg⟩ := (precomp_bijective_of_weakEquivalence X f).2 (.mk (𝟙 X))
  obtain ⟨g, rfl⟩ := g.mk_surjective
  dsimp at hg
  refine ⟨g, by rwa [← mk_eq_mk_iff], ?_⟩
  rw [← mk_eq_mk_iff]
  apply (precomp_bijective_of_weakEquivalence Y f).1
  simp only [precomp_mk, Category.comp_id]
  rw [mk_eq_mk_iff, ← leftHomotopyRel_iff_rightHomotopyRel] at hg ⊢
  simpa using hg.postcomp f

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n i : ℤ
hi : (ComplexShape.up ℤ).Rel i n
⊢ ((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n) = 0

Tactic:
simp only [ComplexShape.up_Rel] at hi

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n i : ℤ
hi : i + 1 = n
⊢ ((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n) = 0
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
⊢ GuitartExact e.hom

Tactic:
rw [guitartExact_iff_isConnected_downwards]
  intro Y₀ X g
  let X₀ := T.objPreimage Y₀
  let e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
  let S := { f : L.obj X₀ ⟶ X // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
  let Z (s : S) : CostructuredArrowDownwards e.hom g :=
    CostructuredArrowDownwards.mk _ _ X₀ e₀.inv s.val (by simp [s.property])
  have : Nonempty (CostructuredArrowDownwards e.hom g) := by
    obtain ⟨f, hf⟩ := B.map_surjective (e.inv.app _ ≫ R.map e₀.hom ≫ g)
    exact ⟨Z ⟨f, hf⟩⟩
  refine zigzag_isConnected (fun A₀ A₁ ↦ ?_)
  have H (A : CostructuredArrowDownwards e.hom g) : ∃ s, Nonempty (Z s ⟶ A) := by
    obtain ⟨a, ha⟩ := T.map_surjective (e₀.hom ≫ A.left.hom)
    refine ⟨⟨L.map a ≫ A.hom.right, ?_⟩,
      ⟨CostructuredArrow.homMk (StructuredArrow.homMk a ?_)⟩⟩
    · simp [← dsimp% NatIso.naturality_1 e a, ha, dsimp% A.hom.w]
    · cat_disch
  obtain ⟨s₀, ⟨f₀⟩⟩ := H A₀
  obtain ⟨s₁, ⟨f₁⟩⟩ := H A₁
  obtain ⟨P, hP, ⟨h⟩⟩ := he s₀.val s₁.val (by simp [s₀.property, s₁.property])
  let Z' : CostructuredArrowDownwards e.hom g :=
    CostructuredArrowDownwards.mk _ _ P.I (e₀.inv ≫ T.map P.i₀) h.h (by
      simp [R.map_comp, ← B.map_comp, dsimp% h.h₀, s₀.property,
        dsimp% e.hom.naturality_assoc P.i₀])
  calc
    Zigzag A₀ (Z s₀) := .of_inv f₀
    Zigzag (Z s₀) Z' := .of_hom <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₀) (by simp [Z, Z', dsimp% h.h₀])
    Zigzag Z' (Z s₁) := .of_inv <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₁) (by simp [Z, Z', dsimp% h.h₁])
    Zigzag (Z s₁) A₁ := .of_hom f₁

Goal state after:
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: case hP₁
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ : C
⊢ ∀ ⦃Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ W.Q.map f))

Tactic:
Y₂

Goal state after:
case hP₁
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
⊢ ∀ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁), P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ W.Q.map f))
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: case hP₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ : C
⊢ ∀ ⦃Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))

Tactic:
Y₂

Goal state after:
case hP₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
⊢ ∀ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ⟨ConcreteCategory.hom { f := ConcreteCategory.ofHom ↑x✝, comm := ⋯ }.f, ⋯⟩ = x✝

Tactic:
dsimp; ext; simp [ConcreteCategory.hom_ofHom]

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
X' : C
g : X ⟶ X'
⊢ toSingleMk (f ≫ g) h = (toSingleMk f h).comp (ofHom ((singleFunctor C q).map g)) ⋯

Tactic:
by
  apply (toSingleEquiv h).injective
  simp [toSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]

Goal state after:
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
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 P =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p

Tactic:
rw [natTrans_eq]
  congr 2
  rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).map_preimage τ) P.X]
  dsimp
  congr

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 : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ F.map ((toKaroubi C).obj X).decompId_i ≫ τ.app X ≫ G.map ((toKaroubi C).obj X).decompId_p = τ.app X

Tactic:
rw [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi,
      Functor.map_id, Category.id_comp]

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 : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ τ.app X ≫ G.map (𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }) = τ.app X
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 : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
      { app := fun P ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ } =
    τ

Tactic:
ext X
    dsimp
    rw [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi,
      Functor.map_id, Category.id_comp]
    change _ ≫ G.map (𝟙 _) = _
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.complex.d 1 0) ≫ F.map (P.π.f 0) = 0

Tactic:
rw [← F.map_comp, complex_d_comp_π_f_zero, F.map_zero]

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
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
X X' : GradedObject I C
φ : X ⟶ X'
⊢ tensorHom φ (𝟙 tensorUnit) ≫ (rightUnitor X').hom = (rightUnitor X).hom ≫ φ

Tactic:
by
  apply mapBifunctorRightUnitor_naturality

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₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.pOpcycles f (𝟙 i₁) n₁ ≫
      (X.opcyclesIso (𝟙 i₀) f (𝟙 i₁) n₀ n₁ (n₁ + 1) hn₁ ⋯).inv ≫
        (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯).right.opcyclesIso.hom =
    (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)

Tactic:
simp only [p_opcyclesIso_inv_assoc, homologyDataIdId_right_p, ← Functor.map_id,
    ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom]

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₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)
Module: Mathlib.Algebra.Lie.Basic

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

Tactic:
apply lie_self

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✝⁴ : 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⁆

Tactic:
intro x y; exact f.map_lie x y

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
⊢ IsUnit.submonoid R = R⁰

Tactic:
ext; simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors_of_mulOpposite]

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

Goal state before:
pp: A : Type v
inst✝² : Ring A
R : Type u
inst✝¹ : CommRing R
inst✝ : Algebra R A
t : R
x y : A
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]

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' : LieSubalgebra R L
x✝ : ↥L'
⊢ ↑⟨⁅↑x✝, ↑x✝⁆, ⋯⟩ = ↑0

Tactic:
apply lie_self

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' : LieSubalgebra R L
M : Type w
inst✝⁶ : AddCommGroup M
inst✝⁵ : LieRingModule L M
N : Type w₁
inst✝⁴ : AddCommGroup N
inst✝³ : LieRingModule L N
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]

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
K K' : LieSubalgebra R L
x : L
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'

Tactic:
← mem_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
x : L
⊢ x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ 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
K K' : LieSubalgebra R L
x : L
⊢ x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'

Tactic:
← mem_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
x : L
⊢ x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ 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
K K' : LieSubalgebra R L
x : L
⊢ x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'

Tactic:
← mem_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
x : L
⊢ x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
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
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
lieSpan,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ↑(sInf {N | s ⊆ ↑N}) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
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 : Function.Surjective ⇑f
x y : L'
hy : y ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier

Tactic:
have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]

Goal state after:
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 : Function.Surjective ⇑f
x y : L'
hy : y ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
hy' : ∃ x ∈ I, f x = y
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
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
⊢ ↑(Submodule.map (↑f) (toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule) ⊆
    ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
rintro x ⟨y, hy₁, hy₂⟩

Goal state after:
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
x : L'
y : L
hy₁ : y ∈ ↑(toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule
hy₂ : ↑f y = x
⊢ x ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)
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
x : M
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'

Tactic:
← mem_toSubmodule,

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
x : M
⊢ x ∈ ↑(N ⊓ N') ↔ x ∈ N ∧ x ∈ 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
x : M
⊢ x ∈ ↑(N ⊓ N') ↔ x ∈ N ∧ x ∈ N'

Tactic:
← mem_toSubmodule,

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
x : M
⊢ x ∈ ↑(N ⊓ N') ↔ x ∈ ↑N ∧ x ∈ 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
x : M
⊢ x ∈ ↑(N ⊓ N') ↔ x ∈ ↑N ∧ x ∈ N'

Tactic:
← mem_toSubmodule,

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
x : M
⊢ x ∈ ↑(N ⊓ N') ↔ x ∈ ↑N ∧ x ∈ ↑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
x : M
⊢ x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Tactic:
← mem_toSubmodule,

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
x : M
⊢ x ∈ ↑(N ⊔ N') ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x