mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f s b ∈ Pretriangulated.distinguishedTriangles
⊢ B.trW s

Tactic:
rw [trW_iff']

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f s b ∈ Pretriangulated.distinguishedTriangles
⊢ ∃ X f h, ∃ (_ : Triangle.mk f s h ∈ Pretriangulated.distinguishedTriangles), B X
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✝ : IsTriangulated C
⊢ ∀ (X : C), t.plus X → ∀ (n : ℤ), t.plus ((t.truncLE n).obj X) ∧ t.plus ((t.truncGE n).obj X)

Tactic:
rintro X ⟨a, _⟩ n; exact ⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩

Goal state after:
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✝ : IsTriangulated C
⊢ ∀ (X : C), t.minus X → ∀ (n : ℤ), t.minus ((t.truncLE n).obj X) ∧ t.minus ((t.truncGE n).obj X)

Tactic:
rintro X ⟨a, _⟩ n; exact ⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ n✝ ⋯ = 𝟙 (X n✝)
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f (n✝ + 1) (n✝ + 1) ⋯ = 𝟙 (X (n✝ + 1))

Tactic:
| succ _ hi =>

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ (n✝ + 1) ⋯ = f n✝
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f (n✝ + 1) (n✝ + 1 + 1) ⋯ = f (n✝ + 1)

Tactic:
| succ _ hi =>

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ Triangle.mk ((t.truncLTι n₁).app Y) (g ≫ (t.truncGEπ n₁).app Z)
      (inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y) ≅
    (t.triangleLTGE n₁).obj Y

Tactic:
exact Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
      (asIso ((t.truncGE n₁).map g)) (by simp) (by simp) (by simp))

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
l : Q.X n ⟶ X.X m
hl : π.f n ≫ l = (↑(cocycle₁' sq hsq)).v n m hnm
⊢ l ≫ (HomologicalComplex.eval C (ComplexShape.up ℤ) m).map p = 0

Tactic:
by
      simp [← cancel_epi (π.f n), reassoc_of% hl]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : HasInitial C
inst✝² : CategoryWithWeakEquivalences C
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
f : X ⟶ Y
⊢ WeakEquivalence (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : HasInitial C
inst✝² : CategoryWithWeakEquivalences C
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
f : X ⟶ Y
⊢ weakEquivalences (CofibrantObject C) (homMk f) ↔ weakEquivalences C f
Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithFibrations C
inst✝³ : HasTerminal C
inst✝² : CategoryWithWeakEquivalences C
X Y : C
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ WeakEquivalence (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithFibrations C
inst✝³ : HasTerminal C
inst✝² : CategoryWithWeakEquivalences C
X Y : C
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ weakEquivalences (FibrantObject C) (homMk f) ↔ weakEquivalences C f
Module: Mathlib.AlgebraicTopology.ModelCategory.Bifibrant

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
inst✝⁸ : CategoryWithCofibrations C
inst✝⁷ : HasInitial C
inst✝⁶ : CategoryWithFibrations C
inst✝⁵ : HasTerminal C
inst✝⁴ : CategoryWithWeakEquivalences C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsFibrant X
inst✝¹ : IsCofibrant Y
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ WeakEquivalence (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
inst✝⁸ : CategoryWithCofibrations C
inst✝⁷ : HasInitial C
inst✝⁶ : CategoryWithFibrations C
inst✝⁵ : HasTerminal C
inst✝⁴ : CategoryWithWeakEquivalences C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsFibrant X
inst✝¹ : IsCofibrant Y
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ weakEquivalences (BifibrantObject C) (homMk f) ↔ weakEquivalences C f
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
⊢ ∀ {X Y : Plus C} (f : X ⟶ Y), Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) f)

Tactic:
intro ⟨K, n, hn⟩ ⟨L, m, hm⟩ ⟨f⟩
    obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩
    obtain ⟨K', _, i, p, _, _, hp, fac⟩ := cm5a f d
    exact ⟨{
      Z := ⟨K', d, inferInstance⟩
      i := ObjectProperty.homMk i
      p := ObjectProperty.homMk p
      hi :=
        ⟨by rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff],
          by assumption⟩
      hp := hp }⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f : X ⟶ Y
⊢ WeakEquivalence (toHoCat.map f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f : X ⟶ Y
⊢ weakEquivalences (HoCat C) (toHoCat.map f) ↔ weakEquivalences (FibrantObject C) f
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
dsimp
  rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.IsLeftDerivabilityStructure
⊢ Φ.op.IsRightDerivabilityStructure

Tactic:
← isLeftDerivabilityStructure_iff_op

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.IsLeftDerivabilityStructure
⊢ Φ.IsLeftDerivabilityStructure
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseRightDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ L.HasPointwiseLeftKanExtensionAt F (L.obj (L.objPreimage Y))

Tactic:
← F.hasPointwiseRightDerivedFunctorAt_iff L W

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseRightDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ F.HasPointwiseRightDerivedFunctorAt W (L.objPreimage Y)
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝ : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F : C₂ ⥤ D
⊢ IsIso
      (((L.lanAdjunction D).homEquiv (((whiskeringLeft C₁ C₂ D).obj T).obj F)
            ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F)).symm
        (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))) ↔
    (StructuredArrow.right ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))

Tactic:
isIso_lanAdjunction_homEquiv_symm_iff

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝ : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F : C₂ ⥤ D
⊢ ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)) ↔
    (StructuredArrow.right ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} C₁
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
⊢ IsIso (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)

Tactic:
have : F.HasPointwiseRightDerivedFunctor W₂ := by
    rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]
    infer_instance
  dsimp only [rightDerivedFunctorComparison]
  rw [← isRightDerivedFunctor_iff_isIso_rightDerivedDesc,
    isRightDerivedFunctor_iff_isLeftKanExtension]
  exact ((F₂.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor α₂ W₂).compTwoSquare
    ((Φ.catCommSq L₁ L₂).iso).hom).isLeftKanExtension

Goal state after:
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✝¹ : T.IsLeftDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
Y₂ : D₂
X₂ : C₂
e₂ : R.functor.obj X₂ ≅ Y₂
ρ : T.LeftResolution X₂
⊢ Nonempty (B.LeftResolution Y₂)

Tactic:
exact ⟨{
      X₁ := L.functor.obj ρ.X₁
      w := iso.inv.app _ ≫ R.functor.map ρ.w ≫ e₂.hom
      hw := (W₂'.arrow_mk_iso_iff (Arrow.isoMk (iso.app _) e₂)).1 (R.map _ ρ.hw) }⟩

Goal state after:
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 ℤ
hK : (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
n : ℤ
⊢ (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K))

Tactic:
exact ObjectProperty.prop_of_iso _
    (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app K)
    ((HomotopyCategory.subcategoryAcyclic C).leftOrthogonal.le_shift n _ hK)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

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✝¹³ : 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
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
ι : Type u_4
inst✝ : Category.{v_4, u_4} ι
X✝ Y✝ : Triangulated.SpectralObject C ι
α : X✝ ⟶ Y✝
i✝ j✝ k✝ : ι
f : i✝ ⟶ j✝
g : j✝ ⟶ k✝
hf :
  F.map ((shiftFunctor C 1).map (α.hom.app (mk₁ f))) ≫ (commShiftIso F 1).hom.app (Y✝.ω₁.obj (mk₁ f)) =
    (commShiftIso F 1).hom.app (X✝.ω₁.obj (mk₁ f)) ≫ (shiftFunctor D 1).map (F.map (α.hom.app (mk₁ f)))
⊢ F.map (X✝.δ f g ≫ (shiftFunctor C 1).map (α.hom.app (mk₁ f))) ≫ (commShiftIso F 1).hom.app (Y✝.ω₁.obj (mk₁ f)) =
    F.map (α.hom.app (mk₁ g)) ≫ F.map (Y✝.δ f g) ≫ (commShiftIso F 1).hom.app (Y✝.ω₁.obj (mk₁ f))

Tactic:
α.comm,

Goal state after:
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
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
ι : Type u_4
inst✝ : Category.{v_4, u_4} ι
X✝ Y✝ : Triangulated.SpectralObject C ι
α : X✝ ⟶ Y✝
i✝ j✝ k✝ : ι
f : i✝ ⟶ j✝
g : j✝ ⟶ k✝
hf :
  F.map ((shiftFunctor C 1).map (α.hom.app (mk₁ f))) ≫ (commShiftIso F 1).hom.app (Y✝.ω₁.obj (mk₁ f)) =
    (commShiftIso F 1).hom.app (X✝.ω₁.obj (mk₁ f)) ≫ (shiftFunctor D 1).map (F.map (α.hom.app (mk₁ f)))
⊢ F.map (α.hom.app (mk₁ g) ≫ Y✝.δ f g) ≫ (commShiftIso F 1).hom.app (Y✝.ω₁.obj (mk₁ f)) =
    F.map (α.hom.app (mk₁ g)) ≫ F.map (Y✝.δ f g) ≫ (commShiftIso F 1).hom.app (Y✝.ω₁.obj (mk₁ f))
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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ homMk₁ (α'.app 0) (α'.app 1) ⋯) ≫ X.pOpcycles f'' g'' n =
    X.pOpcycles f g n ≫ X.opcyclesMap f g f'' g'' (α ≫ α') n

Tactic:
exact (X.p_opcyclesMap _ _ _ _ _ _ _ (by cat_disch)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : Square C
φ : X✝ ⟶ Y✝
⊢ (X✝.map F).f₁₃ ≫ F.map φ.τ₃ = F.map φ.τ₁ ≫ (Y✝.map F).f₁₃

Tactic:
by simpa only [Functor.map_comp] using! F.congr_map φ.comm₁₃

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

Goal state before:
pp: 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 := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          a ≤
        {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          b ↔
      a ≤ b

Tactic:
intro N1 N2

Goal state after:
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)
N1 N2 : Submodule S M
⊢ {
          toFun := fun N ↦
            let __AddSubmonoid := N.toAddSubmonoid;
            { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
          inj' := ⋯ }
        N1 ≤
      {
          toFun := fun N ↦
            let __AddSubmonoid := N.toAddSubmonoid;
            { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
          inj' := ⋯ }
        N2 ↔
    N1 ≤ N2
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_1
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
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅y, m''⁆ ∈ Submodule.span R s

Tactic:
← hm'',

Goal state after:
case refine_1
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
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅y, ⁅↑x, ↑n⁆⁆ ∈ 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 : Function.Surjective ⇑f
x : L'
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
⊢ ⁅x, f z₂⁆ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier

Tactic:
obtain ⟨z₁, rfl⟩ := h x

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
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
z₁ : L
⊢ ⁅f z₁, f z₂⁆ ∈ (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
h₁ : f.ker = ⊥
h₂ : map f I = ⊥
⊢ I = ⊥

Tactic:
LieHom.ker

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₁ : comap f ⊥ = ⊥
h₂ : map f I = ⊥
⊢ I = ⊥
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
⊢ ⁅⊥, N⁆ = ⊥

Tactic:
suffices ⁅(⊥ : LieIdeal R L), N⁆ ≤ ⊥ by exact le_bot_iff.mp this
  rw [lieIdeal_oper_eq_span, lieSpan_le]; rintro m ⟨⟨x, hx⟩, n, hn⟩; rw [← hn]
  change x ∈ (⊥ : LieIdeal R L) at hx; rw [mem_bot] at hx; simp [hx]

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
ι : Type u_1
N : ι → LieSubmodule R L M
⊢ (iSupIndep fun i ↦ ↑(N i)) ↔ iSupIndep N

Tactic:
by
  simp [iSupIndep_def, ← disjoint_toSubmodule]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ (Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0

Tactic:
aeval_map_algebraMap,

Goal state after:
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ (Polynomial.aeval x) (minpoly A x) = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
g : F[X]
hg : map (algebraMap F E) g = minpoly E a
hgdeg : g.natDegree = (minpoly E a).natDegree
hgmon : g.Monic
⊢ (Polynomial.aeval a) (map (algebraMap E A) (minpoly E a)) = 0

Tactic:
aeval_map_algebraMap,

Goal state after:
F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
g : F[X]
hg : map (algebraMap F E) g = minpoly E a
hgdeg : g.natDegree = (minpoly E a).natDegree
hgmon : g.Monic
⊢ (Polynomial.aeval a) (minpoly E a) = 0