mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
⊢ QuasiIso i ∨ QuasiIso p

Tactic:
simpa only [weakEquivalence_iff] using! hip

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Quotient

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : (Quotient.functor homRel).homRel f f'
⊢ W f

Tactic:
Quotient.functor_homRel_eq_compClosure_eqvGen,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : Relation.EqvGen (HomRel.CompClosure homRel) f f'
⊢ W 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 Y : FibrantObject C
inst✝ : IsCofibrant X.obj
f g : X ⟶ Y
⊢ (Quotient.functor (homRel C)).homRel f g ↔ homRel C f g

Tactic:
Quotient.functor_homRel_eq_compClosure_eqvGen,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : FibrantObject C
inst✝ : IsCofibrant X.obj
f g : X ⟶ Y
⊢ Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
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 : C
f : X ⟶ Y
⊢ ∃ g, iResolutionObj X ≫ g = f ≫ iResolutionObj Y

Tactic:
have sq : CommSq (f ≫ iResolutionObj Y) (iResolutionObj X)
    (terminal.from _) (terminal.from _) := ⟨by simp⟩
  exact ⟨sq.lift, sq.fac_left⟩

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
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro X
  apply Localization.inverts L (weakEquivalences _)
  rw [← weakEquivalence_iff]
  infer_instance

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
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
⊢ IsIso (HoCat.resolutionCompToLocalizationNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro X
  apply Localization.inverts L (weakEquivalences _)
  rw [← weakEquivalence_iff]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.CostructuredArrowDownwards g
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Tactic:
obtain ⟨g, φ, rfl⟩ := CostructuredArrow.mk_surjective f

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g✝ : R.obj X₂ ⟶ B.obj X₃
g : StructuredArrow X₂ T
φ : (w.structuredArrowDownwards X₂).obj g ⟶ StructuredArrow.mk g✝
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝), CostructuredArrow.mk φ = mk w g✝ X₁ a b comm
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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q₁ : ℕ
hi : i ≤ n₀ + ↑q₁
hq : q₁ ≤ q₁ + 1
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
dsimp [functor]

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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q₁ : ℕ
hi : i ≤ n₀ + ↑q₁
hq : q₁ ≤ q₁ + 1
⊢ IsIso
    (((Functor.ofSequence fun q ↦ (CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q).op).map
                (homOfLE hq)).unop.hom.h.f
      i)
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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i + 1 ≤ n₀ + ↑q
this : QuasiIsoAt (midπ f n₀ q) i
⊢ QuasiIsoAt (ι f n₀ ≫ midπ f n₀ q) i

Tactic:
ι_midπ

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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i + 1 ≤ n₀ + ↑q
this : QuasiIsoAt (midπ f n₀ q) i
⊢ QuasiIsoAt ((functor f n₀).obj (op q)).obj.ι i
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: case h₁
A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ (Arrow.Hom.left
        (Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((π' Λ).app X)).right) ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((toKaroubi A).map (Λ.π.app X))).right)
            ⋯)).f =
    (Arrow.Hom.left (𝟙 (Arrow.mk ((π' Λ).app X)))).f

pp: case h₂
A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ (Arrow.Hom.right
        (Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((π' Λ).app X)).right) ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((toKaroubi A).map (Λ.π.app X))).right)
            ⋯)).f =
    (Arrow.Hom.right (𝟙 (Arrow.mk ((π' Λ).app X)))).f

Tactic:
· simp [← Functor.map_comp]

Goal state after:
case h₂
A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ (Arrow.Hom.right
        (Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((π' Λ).app X)).right) ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((toKaroubi A).map (Λ.π.app X))).right)
            ⋯)).f =
    (Arrow.Hom.right (𝟙 (Arrow.mk ((π' Λ).app X)))).f
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case succ.hL
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj Z) (n✝ + 1)

Tactic:
· apply ChainComplex.exactAt_succ_single_obj

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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝¹ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
j : J
⊢ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j ⋯ ≫
      (CofanMapObjFun.iso (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y j)).inv =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)

Tactic:
erw [CofanMapObjFun.ιMapObj_iso_inv]

Goal state after:
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝¹ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
j : J
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)
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 ⋯ ≫
      (CofanMapObjFun.iso (mapBifunctorRightUnitorCofanIsColimit F Y e p hp X j)).inv =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)

Tactic:
erw [CofanMapObjFun.ιMapObj_iso_inv]

Goal state after:
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
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)
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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
⊢ φ ≫ (mapBifunctorRightUnitor F Y e p hp X').inv =
    (mapBifunctorRightUnitor F Y e p hp X).inv ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y))

Tactic:
by
  ext j
  dsimp
  rw [mapBifunctorRightUnitor_inv_apply, mapBifunctorRightUnitor_inv_apply, assoc, assoc,
    ι_mapBifunctorMapMap]
  dsimp
  rw [Functor.map_id, id_comp, NatTrans.naturality_assoc]
  erw [← NatTrans.naturality_assoc e.inv]
  rfl

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₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A Z : C
f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : (i₁, i₂, i₃) ∈ r₁₂₃ ⁻¹' {j}
⊢ (((curriedTensor C).obj Z).mapCocone
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
        { as := ⟨(i₁, i₂, i₃), hi⟩ } ≫
      f =
    (((curriedTensor C).obj Z).mapCocone
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
        { as := ⟨(i₁, i₂, i₃), hi⟩ } ≫
      g

Tactic:
exact h _ _ _ hi

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
n : ℕ
⊢ Finite ↑{i | i.1 + i.2.1 + i.2.2 = n}

Tactic:
by
  refine Finite.of_injective (fun ⟨⟨i₁, i₂, i₃⟩, (hi : i₁ + i₂ + i₃ = n)⟩ =>
    (⟨⟨i₁, by lia⟩, ⟨i₂, by lia⟩, ⟨i₃, by lia⟩⟩ :
      Fin (n + 1) × Fin (n + 1) × Fin (n + 1))) ?_
  intro _ _ h
  exact Subtype.ext (congrArg (fun x => (x.1.1, x.2.1.1, x.2.2.1)) h)

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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

Tactic:
by
  ext
  all_goals dsimp; convert! (X.H _).map_id _; cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom =
    (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).hom

Tactic:
obtain rfl := hn₂

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom =
    (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯).hom ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ (n₁ + 1) hn₁ ⋯).hom
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv =
    (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv ≫
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯).inv

Tactic:
obtain rfl := hn₂

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv =
    (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ (n₁ + 1) hn₁ ⋯).inv ≫
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯).inv
Module: Mathlib.Algebra.Lie.Basic

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

Tactic:
← neg_neg ⁅x, y⁆,

Goal state after:
L : Type v
inst✝ : LieRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, - -⁅x, y⁆⁆ = 0
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
x y : L
⊢ { toFun := fun m ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    ⁅{ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ },
      { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }⁆

Tactic:
by ext m; apply lie_lie

Goal state after:
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:
by 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' : LieSubalgebra R L
t✝ : R
x✝ y✝ : ↥L'
⊢ ↑⁅x✝, t✝ • y✝⁆ = ↑(t✝ • ⁅x✝, y✝⁆)

Tactic:
apply lie_smul

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

Goal state before:
pp: case mem
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s✝ s : Set L
x y : L
h : y ∈ -s
⊢ y ∈ lieSpan R L s

Tactic:
| mem y h =>

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (a * b) + L (b * b) + L (b * c)) + (L (a * c) + L (c * b) + L (c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (a * c) + 2 • L (b * c)⁆

Tactic:
mul_comm c b

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (a * b) + L (b * b) + L (b * c)) + (L (a * c) + L (b * c) + L (c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (a * c) + 2 • L (b * c)⁆
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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
t : R
x : L
y : ↥N
⊢ ↑⁅x, t • y⁆ = ↑(t • ⁅x, y⁆)

Tactic:
apply lie_smul

Goal state after:
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
y : L'
h₁ : Function.Surjective ⇑f
h₂ : y ∈ ↑(map f I)
⊢ ∃ x, f ↑x = y

Tactic:
coe_map_of_surjective h₁,

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
y : L'
h₁ : Function.Surjective ⇑f
h₂ : y ∈ Submodule.map ↑f ↑I
⊢ ∃ x, f ↑x = y
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : LieModule.IsTrivial L ↥I
x y : ↥I
⊢ ⁅x, y⁆ = 0

Tactic:
by apply h.trivial

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsLieAbelian ↥I
z : L
x : ↥I
y : ↥I
hz : ⁅↑x, ↑y⁆ = z
⊢ ⁅x, y⁆ = 0

Tactic:
by apply h.trivial

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

Goal state before:
pp: A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
x : B
⊢ (Polynomial.aeval (f x)) (minpoly A x) = 0

Tactic:
Polynomial.aeval_algHom,

Goal state after:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
x : B
⊢ (f.comp (Polynomial.aeval x)) (minpoly A x) = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 0 = X

Tactic:
by
  simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, map_zero] using eq_X_sub_C B (0 : A)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.map (↑(quotientSpanXSubCAlgEquiv y))
      (Ideal.map (Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (Ideal.span {C x})) =
    Ideal.span {x}

Tactic:
simp only [Ideal.map_span, Set.image_singleton]; congr 2; exact eval_C

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) X ^ pb.dim - ∑ x, (algebraMap A S) ((pb.basis.repr (pb.gen ^ pb.dim)) x) * (aeval pb.gen) X ^ ↑x = 0

Tactic:
← Algebra.smul_def,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) X ^ pb.dim - ∑ x, (pb.basis.repr (pb.gen ^ pb.dim)) x • (aeval pb.gen) X ^ ↑x = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R[X]
⊢ (span {X - C 0}).IsMaximal

Tactic:
exact PrincipalIdealRing.isMaximal_of_irreducible (irreducible_X_sub_C 0)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x : R
inst✝ : DecompositionMonoid R
⊢ x = 0 → IsRadical x

Tactic:
rintro rfl
      rw [zero_isRadical_iff]
      infer_instance

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬Separable 0

Tactic:
rintro ⟨x, y, h⟩
  simp only [derivative_zero, mul_zero, add_zero, zero_ne_one] at h

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hp : p.Separable
hq : q * q ∣ p
⊢ IsUnit q

Tactic:
by
  obtain ⟨p, rfl⟩ := hq
  apply isCoprime_self.mp
  have : IsCoprime (q * (q * p))
      (q * (derivative q * p + derivative q * p + q * derivative p)) := by
    simp only [← mul_assoc, mul_add]
    dsimp only [Separable] at hp
    convert! hp using 1
    rw [derivative_mul, derivative_mul]
    ring
  exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ LinearMap.det x✝ = (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) x✝

Tactic:
LinearMap.det_def

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) x✝ =
    (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) x✝