mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  simp only [weakEquivalence_iff]
  rfl

Goal state after:
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:
by
  simp only [weakEquivalence_iff]
  rfl

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✝⁶ : 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:
by
  simp only [weakEquivalence_iff]
  rfl

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
f g : X ⟶ Y
inst✝ : IsFibrant Y
h : RightHomotopyRel f g
P : Cylinder X
h✝ : P.IsVeryGood
⊢ LeftHomotopyRel f g

Tactic:
exact ⟨P, ⟨h.leftHomotopy P⟩⟩

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 g : X ⟶ Y
h : homRel C f g
⊢ weakEquivalences (FibrantObject C) f ↔ weakEquivalences (FibrantObject C) g

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ L.map R.w ≫ L.map (Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = y

Tactic:
← L.map_comp_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ L.map (R.w ≫ Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = y
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✝ : W₁.ContainsIdentities
⊢ (id W₁).IsRightDerivabilityStructure

Tactic:
rw [(LocalizerMorphism.id W₁).isRightDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]
  dsimp
  exact TwoSquare.guitartExact_id W₁.Q

Goal state after:
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₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : S → CostructuredArrowDownwards e.hom g := fun s ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv ↑s ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ s, Nonempty (Z s ⟶ A)
s₀ : S
f₀ : Z s₀ ⟶ A₀
s₁ : S
f₁ : Z s₁ ⟶ A₁
P : Precylinder X₀
hP : T.map P.i₀ = T.map P.i₁
h : (P.map L).LeftHomotopy ↑s₀ ↑s₁
Z' : CostructuredArrowDownwards e.hom g := CostructuredArrowDownwards.mk e.hom g P.I (e₀.inv ≫ T.map P.i₀) h.h ⋯
⊢ (structuredArrowDownwards e.hom Y₀).map (StructuredArrow.homMk P.i₁ ⋯) ≫ CostructuredArrow.hom Z' =
    CostructuredArrow.hom (Z s₁)

Tactic:
simp [Z, Z', dsimp% h.h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α

Tactic:
by
  constructor
  · exact fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W
  · exact fun h => ⟨h⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
  rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]
  obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
  refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
  · simp [hg]
  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
⊢ (∃ β, δ (n - 1) n β = ↑(fromSingleMk f h q' hq' hf)) → ∃ g, g ≫ K.d q'' q = f

Tactic:
rintro ⟨α, hα⟩

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
α : Cochain ((singleFunctor C p).obj X) K (n - 1)
hα : δ (n - 1) n α = ↑(fromSingleMk f h q' hq' hf)
⊢ ∃ g, g ≫ K.d q'' q = f
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case mp
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''
⊢ (∃ β, δ (n - 1) n β = ↑(toSingleMk f h p' hp' hf)) → ∃ g, K.d p p'' ≫ g = f

Tactic:
rintro ⟨α, hα⟩

Goal state after:
case mp
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)
hα : δ (n - 1) n α = ↑(toSingleMk f h p' hp' hf)
⊢ ∃ g, K.d p p'' ≫ g = f
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J K : Ideal R
hJK : J.radical = K.radical
L : Ideal R
hL : J.radical ≤ L.radical
⊢ K.radical ≤ L.radical

Tactic:
exact hJK.symm.trans_le hL

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.opcyclesMap f g f' g' α n ≫ X.fromOpcycles f' g' fg' h' n = X.fromOpcycles f g fg h n ≫ (X.H n).map β

Tactic:
rw [← cancel_epi (X.pOpcycles f g n), p_fromOpcycles_assoc,
    X.p_opcyclesMap_assoc f g f' g' α (homMk₁ (α.app 0) (α.app 1)
      (naturality' α 0 1)) n rfl,
    p_fromOpcycles, ← Functor.map_comp, ← Functor.map_comp]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j 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.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') = (X.H n).map (twoδ₂Toδ₁ f g fg h ≫ β)
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₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this :
  X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ =
    X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃ (𝟙 (mk₂ f₂ f₃)) n₁
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
rw [opcyclesMap_id, comp_id] at this

Goal state after:
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₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this : X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ = X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)
Module: Mathlib.Algebra.Homology.SpectralObject.Homology

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₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁
hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
refine ⟨A₂, π₂ ≫ π₁, inferInstance, y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂, ?_⟩

Goal state after:
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₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁
hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f
⊢ (π₂ ≫ π₁) ≫ x₂ =
    (y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
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₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂ = x

Tactic:
dsimp only [descE]
  rw [← Category.assoc]
  apply (X.cokernelSequenceE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂).g_desc

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

Goal state before:
pp: case refine_2
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)
⊢ Function.Injective fun N ↦
    let __AddSubmonoid := N.toAddSubmonoid;
    { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }

Tactic:
intro N1 N2 h
    rwa [Submodule.ext_iff] at h ⊢

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

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ n₀ = data.deg pq

Tactic:
have := data.hc r pq pq' h

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
this : data.deg pq + 1 = data.deg pq'
⊢ n₀ = data.deg pq
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x✝ y✝ z : L
m n : M
x y : L
f : M →ₗ[R] N
⊢ {
      toFun := fun m ↦
        ⁅x, { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } m⁆ -
          { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅x, m⁆,
      map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅⁅x, y⁆, f m⁆ - f ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      {
        toFun := fun m ↦
          ⁅y, { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } m⁆ -
            { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅y, m⁆,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext n
    simp only [lie_lie, coe_mk, AddHom.coe_mk, map_sub, add_apply, lie_sub]
    abel

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

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Fork.ι (kf X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
      Cofork.π (cc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯) =
    X.mapFourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ≫ X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯

Tactic:
simp [← map_comp]

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.map (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
      (fourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ ≫ fourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯) n₀ n₁ n₂ ⋯ ⋯ =
    X.map (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
      (fourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ ≫ fourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' ⋯ ⋯ ⋯ ⋯) n₀ n₁ n₂ ⋯ ⋯
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsLeftRegular x ∧ IsUnit x

Tactic:
and_iff_right_of_imp (·.isRegular.1)

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsUnit x
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n * 1

Tactic:
convert! hy using 1

Goal state after:
case e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n.succ • y
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
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'
⊢ (∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆) → ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z

pp: case mpr
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'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z) → ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆

Tactic:
· intro h x y; obtain ⟨z, hz⟩ := h x (f y) y rfl; use z; exact hz.symm

Goal state after:
case mpr
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'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z) → ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆
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'
x : L
⊢ x ∈ ↑f.ker ↔ f x = 0

Tactic:
simp only [ker_toSubmodule, LinearMap.mem_ker, coe_toLinearMap]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ ↑N = ⊤ ↔ ↑N = ↑⊤

Tactic:
top_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 : LieSubmodule R L M
⊢ ↑N = ⊤ ↔ ↑N = ⊤
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ ↑{ toSubmodule := N, lie_mem := h } = ↑⊤ ↔ N = ⊤

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(sInf (range fun i ↦ p i)) = ⨅ i, ↑(p i)

Tactic:
sInf_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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ sInf {x | ∃ s ∈ range fun i ↦ p i, ↑s = x} = ⨅ i, ↑(p i)
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ ≤ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
let s := { ⁅(x : L), (n : M)⁆ | (x : I) (n : N) }
    have aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s := by
      intro y m' hm'
      refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
      · rintro m'' ⟨x, n, hm''⟩; rw [← hm'', leibniz_lie]
        refine Submodule.add_mem _ ?_ ?_ <;> apply Submodule.subset_span
        · use ⟨⁅y, ↑x⁆, I.lie_mem x.property⟩, n
        · use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩
      · simp
      · intro m₁ m₂ _ _ hm₁ hm₂; rw [lie_add]; exact Submodule.add_mem _ hm₁ hm₂
      · intro t m'' _ hm''; rw [lie_smul]; exact Submodule.smul_mem _ t hm''
    change _ ≤ ({ Submodule.span R s with lie_mem := fun hm' => aux _ _ hm' } : LieSubmodule R L M)
    rw [lieIdeal_oper_eq_span, lieSpan_le]
    exact Submodule.subset_span

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

Goal state before:
pp: A : Type v
inst✝ : Ring A
⊢ IsMulCommutative A ↔ IsLieAbelian A

Tactic:
have : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨(·.trivial), (⟨·⟩)⟩

Goal state after:
A : Type v
inst✝ : Ring A
this : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ IsMulCommutative A ↔ IsLieAbelian A