mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
⊢ Function.Bijective ((fun f ↦ f.postcomp h.r) ∘ fun f ↦ f.postcomp h.i)

Tactic:
convert! Function.bijective_id

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
⊢ ((fun f ↦ f.postcomp h.r) ∘ fun f ↦ f.postcomp h.i) = id
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
⊢ Function.Bijective ((fun g ↦ g.precomp h.s) ∘ fun g ↦ g.precomp h.p)

Tactic:
convert! Function.bijective_id

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
⊢ ((fun g ↦ g.precomp h.s) ∘ fun g ↦ g.precomp h.p) = id
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₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
x✝ : x₁ ≫ K.d n₁ (n₁ + 1) = 0
y₀ : A ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ (ι f n₁).f n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁_1, π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁

Tactic:
obtain ⟨y₀, rfl⟩ : ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ (σ K L n₁).f n₀ = y₀ := by
    refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩
    have : (biprod.inl : _ ⟶ mid K L n₁).f n₀ = 0 :=
      (isZero_single_obj_X (.up ℤ) _ _ _ (by lia)).eq_of_src _ _
    simp [this, ← biprod_total_f]

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₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
x✝ : x₁ ≫ K.d n₁ (n₁ + 1) = 0
y₀ : A ⟶ L.X n₀
hy₀ : x₁ ≫ (ι f n₁).f n₁ = (y₀ ≫ (σ K L n₁).f n₀) ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁_1, π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
⊢ QuasiIsoAt (ι f n) n

Tactic:
have := mono_homologyMap_π f n n (by lia)
    have : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n) := by
      dsimp; infer_instance
    have h₁ := (exact_homologyShortComplex f n).fIsKernel
    have h₂ := (CochainComplex.homologyMap_exact₂_of_distTriang _
      (DerivedCategory.mappingCocone_triangle_distinguished (α f n)) n).fIsKernel
    have : homologyMap (ι f n) n = (IsLimit.conePointUniqueUpToIso h₁ h₂).hom := by
      simp [← cancel_mono (homologyMap (π f n) n),
        dsimp% IsLimit.conePointUniqueUpToIso_hom_comp h₁ h₂ .zero,
        ← homologyMap_comp, mappingCocone.lift_fst]
    rw [quasiIsoAt_iff_isIso_homologyMap, this]
    infer_instance

Goal state after:
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 Y

Tactic:
rw [← hasPointwiseLeftKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y),
    ← 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.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₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ (Φ.localizedFunctor L₁ L₂ ⋙ F₂).IsLeftKanExtension
    (Φ.functor.whiskerLeft α₂ ≫
      (Φ.functor.associator L₂ F₂).inv ≫
        whiskerRight (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂ ≫
          (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom)

Tactic:
exact ((F₂.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor α₂ W₂).compTwoSquare
    ((Φ.catCommSq L₁ L₂).iso).hom).isLeftKanExtension

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 : K.IsKProjective
n : ℤ
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).IsKProjective

Tactic:
rw [isKProjective_iff_leftOrthogonal] at hK ⊢
  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.Algebra.Homology.HomotopyCategory.KProjective

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

Tactic:
exact (K.isZero_of_isStrictlyLE d _ (by dsimp; lia)).op

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
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| φ.app P

Tactic:
rw [← id_comp (φ.app P), ← F.map_id]

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
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| F.map (𝟙 P) ≫ φ.app P
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
by
  ext
  simp [lift, liftFZero, liftFOne]

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

Tactic:
exact (natTrans_eq _ _).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ QuasiIsoAt (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩) n

Tactic:
cases n
    · rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros']
      · dsimp
        refine (ShortComplex.exact_and_epi_g_iff_of_iso ?_).2
          ⟨exact_d_f (Projective.π Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
          (by simp [ofComplex]) (by simp)
      all_goals rfl
    · rw [quasiIsoAt_iff_exactAt']
      · apply ofComplex_exactAt_succ
      · apply ChainComplex.exactAt_succ_single_obj

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case e_a.e_a.e_a
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst✝¹⁵ : Category.{v_1, u_1} C₁
inst✝¹⁴ : Category.{v_2, u_2} C₂
inst✝¹³ : Category.{v_3, u_3} C₃
inst✝¹² : Category.{v_4, u_4} D
inst✝¹¹ : Zero I₂
inst✝¹⁰ : DecidableEq I₂
inst✝⁹ : HasInitial C₂
F₁ : C₁ ⥤ C₂ ⥤ C₁
F₂ : C₂ ⥤ C₃ ⥤ C₃
G : C₁ ⥤ C₃ ⥤ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst✝⁸ : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst✝⁷ : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂
inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π
inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃
inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π
inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃
inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃
inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ (G.map ((F₁.obj (X₁ i₁)).map (singleObjApplyIso 0 X₂).hom)).app (X₃ i₃) ≫
      ((associator.hom.app (X₁ i₁)).app X₂).app (X₃ i₃) =
    ((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫
      (G.obj (X₁ i₁)).map ((F₂.map (singleObjApplyIso 0 X₂).hom).app (X₃ i₃))

Tactic:
apply NatTrans.naturality_app (associator.hom.app (X₁ i₁))

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0

Tactic:
by
  rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_comp]

Goal state after:
Module: Mathlib.Order.WithBotTop

Goal state before:
pp: ι : Type u_1
inst✝ : LT ι
a b : ι
⊢ coe a < coe b ↔ a < b

Tactic:
rw [← WithTop.coe_lt_coe (α := ι)]
  exact WithBot.coe_lt_coe

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
γ : mk₂ f₂ f₃ ⟶ mk₂ f₂' f₃'
hγ : γ = homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) ≫
      (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁

Tactic:
by
  subst hγ
  simp [← cancel_epi (ShortComplex.pOpcycles _), p_opcyclesMap]

Goal state after:
Module: Mathlib.Order.Filter.Subsingleton

Goal state before:
pp: α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l.IsCountablyGenerated

Tactic:
rcases subsingleton_iff_bot_or_pure.1 hl with rfl | ⟨x, rfl⟩
  · exact isCountablyGenerated_bot
  · exact isCountablyGenerated_pure x

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁
⊢ x = 0

Tactic:
rw [zero_comp, Category.assoc,
    X.opcyclesMap_fromOpcycles f₁ f₂₃ f₁₂ f₃ (f₁₂ ≫ f₃) (by cat_disch) _ rfl _ (𝟙 _) n₁
      (by simp) (by cat_disch), Functor.map_id, Category.comp_id] at hx

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₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ x = 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case neg
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'' : κ
hpq' : (c r).next pq' = pq''
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' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq' pq''
⊢ (kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).Exact

Tactic:
rw [ShortComplex.exact_iff_epi _ ((page X data r hr).shape _ _ h)]

Goal state after:
case neg
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'' : κ
hpq' : (c r).next pq' = pq''
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' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq' pq''
⊢ Epi (kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).f
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Tactic:
convert congr($h1.symm - $h2)

Goal state after:
case e'_2
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

case e'_3
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)
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
t : R
x m : L
⊢ -⁅m, t • x⁆ = t • -⁅m, x⁆

Tactic:
LieAlgebra.lie_smul,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x m : L
⊢ -(t • ⁅m, x⁆) = t • -⁅m, x⁆
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ (Subalgebra.toSubmodule A').carrier
hy : y ∈ (Subalgebra.toSubmodule A').carrier
⊢ ⁅x, y⁆ ∈ (Subalgebra.toSubmodule A').carrier

Tactic:
change ⁅x, y⁆ ∈ A'

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ (Subalgebra.toSubmodule A').carrier
hy : y ∈ (Subalgebra.toSubmodule A').carrier
⊢ ⁅x, y⁆ ∈ A'
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ -⁅y, x⁆ ∈ I

Tactic:
← neg_lie

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅-y, x⁆ ∈ I
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 (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ =
    ⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ +
          ⁅L a, 2 • L (b * c)⁆ +
        (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ +
          ⁅L b, 2 • L (b * c)⁆) +
      (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ +
        ⁅L c, 2 • L (b * c)⁆)

Tactic:
rw [add_lie, add_lie]

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ +
        ⁅L b, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ +
      ⁅L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ =
    ⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ +
          ⁅L a, 2 • L (b * c)⁆ +
        (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ +
          ⁅L b, 2 • L (b * c)⁆) +
      (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ +
        ⁅L 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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨆ i, p i) = ⨆ i, ↑(p i)

Tactic:
rw [iSup, sSup_toSubmodule]; ext; simp [Submodule.mem_sSup, Submodule.mem_iSup]

Goal state after:
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
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]; rintro m ⟨x, n, hn⟩; rw [← hn]
  exact N.lie_mem n.property

Goal state after:
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
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
⊢ minpoly A x ∣ p

Tactic:
by
  by_cases hp0 : p = 0
  · simp only [hp0, dvd_zero]
  have hx : IsIntegral A x := IsAlgebraic.isIntegral ⟨p, hp0, hp⟩
  rw [← modByMonic_eq_zero_iff_dvd (monic hx)]
  by_contra hnz
  apply degree_le_of_ne_zero A x hnz
    ((aeval_modByMonic_eq_self_of_root (aeval _ _)).trans hp) |>.not_gt
  exact degree_modByMonic_lt _ (monic hx)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
⊢ q.coeff i = coeff 0 i

Tactic:
obtain lt | le := lt_or_ge i n

Goal state after:
case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt✝ : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
lt : i < n
⊢ q.coeff i = coeff 0 i

case inr
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
le : n ≤ i
⊢ q.coeff i = coeff 0 i