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

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 C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasRightResolutions
X₂ : C₂
⊢ Nonempty (T.RightResolution X₂)

Tactic:
let ρ : B.RightResolution (R.functor.obj X₂) := Classical.arbitrary _

Goal state after:
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 C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasRightResolutions
X₂ : C₂
ρ : B.RightResolution (R.functor.obj X₂) := Classical.arbitrary (B.RightResolution (R.functor.obj X₂))
⊢ Nonempty (T.RightResolution X₂)
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

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 : B.op.obj X₃ ⟶ R.op.obj X₂
f f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ StructuredArrow.hom
        (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
          (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op ⋯) ≫
      (w.op.costructuredArrowRightwards X₂).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left).op ⋯) =
    StructuredArrow.hom
      (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
        (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)

Tactic:
ext
            exact Quiver.Hom.unop_inj
              ((StructuredArrow.proj _ _).congr_map (CostructuredArrow.w φ))

Goal state after:
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✝¹ : w.GuitartExact
inst✝ : B.EssSurj
F : C₂ ⥤ D
h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)
X₄ : C₄
⊢ R.HasPointwiseLeftKanExtensionAt F (B.obj (B.objPreimage X₄))

Tactic:
apply h

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
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✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
X✝ : C₁ᵒᵖ
⊢ (w ≫ₕ w'.hom).op.natTrans.app X✝ = (w.op ≫ᵥ w''.hom).natTrans.app X✝

Tactic:
simp [w'']

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

Goal state before:
pp: case refine_1
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₀ =
    (L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₁

Tactic:
ext : 1

Goal state after:
case refine_1
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ ((L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₀).hom =
    ((L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₁).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Abelian C
inst✝⁴ : Category.{v_2, u_2} H
inst✝³ : EnoughInjectives C
F : Plus C ⥤ H
inst✝² : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝¹ : F'.IsRightDerivedFunctor α (quasiIso C)
K : Plus C
inst✝ : ∀ (n : ℤ), Injective (K.obj.as.X n)
⊢ IsIso (α.app K)

Tactic:
by
  have (Y : HomotopyCategory.Plus (InjectiveObject C)) :
      IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y)) :=
    (localizerMorphism_derives F).isIso_of_isRightDerivedFunctor _ _
  obtain ⟨Y, ⟨e⟩⟩ : (InjectiveObject.ι C).mapHomotopyCategoryPlus.essImage K := by
    obtain ⟨X, hX⟩ := K
    obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective X
    refine ⟨(quotient _).obj
      ((CochainComplex.Plus.fibrantObjectEquivalence C).inverse.obj
      ⟨⟨K, by simpa using hX⟩, ?_⟩), ⟨Iso.refl _⟩⟩
    dsimp [fibrantObjects]
    rwa [CochainComplex.Plus.modelCategoryQuillen.isFibrant_iff]
  rw [← NatTrans.isIso_app_iff_of_iso α e]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc 0 + 1 = m
⊢ h.d (Int.negSucc 0) m ≫ h.d m p = 0

Tactic:
obtain rfl : m = 0 := by lia
    obtain rfl : p = 1 := by lia
    simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.negSucc.succ.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = m
⊢ h.d (Int.negSucc (n + 1 + 1)) m ≫ h.d m p = 0

Tactic:
· obtain rfl : m = .negSucc (n + 1) := by lia
    obtain rfl : p = .negSucc n := by lia
    simp

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 0) ∧ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
constructor <;> dsimp <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 0) ∧ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
constructor <;> dsimp <;> infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ fromSingleMk (g ≫ f) h q' hq' ⋯ = (fromSingleMk f h q' hq' hf).precomp ((singleFunctor C p).map g)

Tactic:
ext : 1

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

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

Tactic:
ext : 1

Goal state after:
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
L : CochainComplex C ℤ
g : K ⟶ L
⊢ ↑(fromSingleMk (f ≫ g.f q) h q' hq' ⋯) = ↑((fromSingleMk f h q' hq' hf).postcomp g)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ fromSingleMk f h q' hq' ⋯ = α

Tactic:
ext : 1

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
X' : C
g : X ⟶ X'
⊢ toSingleMk (f ≫ g) h p' hp' ⋯ = (toSingleMk f h p' hp' hf).postcomp ((singleFunctor C q).map g)

Tactic:
ext : 1

Goal state after:
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
X' : C
g : X ⟶ X'
⊢ ↑(toSingleMk (f ≫ g) h p' hp' ⋯) = ↑((toSingleMk f h p' hp' hf).postcomp ((singleFunctor C q).map g))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
X' : C
g : X ⟶ X'
⊢ toSingleMk (f ≫ g) h p' hp' ⋯ = (toSingleMk f h p' hp' hf).postcomp ((singleFunctor C q).map g)

Tactic:
by
  ext : 1
  exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_postcomp])

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
L : CochainComplex C ℤ
g : L ⟶ K
⊢ toSingleMk (g.f p ≫ f) h p' hp' ⋯ = (toSingleMk f h p' hp' hf).precomp g

Tactic:
ext : 1

Goal state after:
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
L : CochainComplex C ℤ
g : L ⟶ K
⊢ ↑(toSingleMk (g.f p ≫ f) h p' hp' ⋯) = ↑((toSingleMk f h p' hp' hf).precomp g)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ toSingleMk f h p' hp' ⋯ = α

Tactic:
ext : 1

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ↑(toSingleMk f h p' hp' ⋯) = ↑α
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
⊢ 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)

Tactic:
rw [mapBifunctorLeftUnitorCofan_inj]

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
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData

Tactic:
exact {
    K := X.cycles f₁ f₂ n₁
    H := cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁)
    i := X.iCycles f₁ f₂ n₁
    π := cokernel.π _
    wi := by simp
    hi := hi
    wπ := by rw [this]; simp
    hπ := by
      refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (cokernelIsCokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁))
      · exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
      · exact Cofork.ext (Iso.refl _) }

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ x, M✝ (e x))

Tactic:
apply h

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L
n : N
⊢ g ⁅x, n⁆ = g ⁅x, f (g n)⁆

Tactic:
by rw [h₂]

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₁' L₂' : LieSubalgebra R L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'

Tactic:
exact h

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₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L₂
hx : x ∈ (Submodule.map (↑f) K.toSubmodule).carrier
hy : y ∈ (Submodule.map (↑f) K.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f) K.toSubmodule).carrier

Tactic:
simp only [AddSubsemigroup.mem_carrier] at hx hy
      rcases hx with ⟨x', hx', rfl⟩
      rcases hy with ⟨y', hy', rfl⟩
      simpa using ⟨⁅x', y'⁆, K.lie_mem hx' hy', f.map_lie x' y'⟩

Goal state after:
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
z : M
n : ℕ
⊢ (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_antidiagonal_choose_succ_nsmul
      (fun i j ↦ ⁅((ad R L x) ^ i) y, ((φ x) ^ j) z⁆) n]
    simp only [pow_succ', Module.End.mul_apply, ih, map_sum, map_nsmul,
      toEnd_lie, nsmul_add, sum_add_distrib]
    rw [add_comm, add_left_cancel_iff, sum_congr rfl]
    rintro ⟨i, j⟩ hij
    rw [mem_antidiagonal] at hij
    rw [Nat.choose_symm_of_eq_add hij.symm]

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₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥ ↔ ⟨x, hx⟩ ∈ ⊤

Tactic:
change x ∈ ⊥ at hx

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥ ↔ ⟨x, hx⟩ ∈ ⊤
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case a
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₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule

Tactic:
exact h

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:
exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h

Goal state after:
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'
I : LieIdeal R L
x : L
h : f x = 0
hx : x ∈ I
⊢ f x = 0

Tactic:
exact h

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 N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
refine ⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N') → {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N'
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✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ m ∈ N

Tactic:
apply h

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
Module: Mathlib.Algebra.Lie.Abelian

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
⊢ IsFaithful R L M ↔ LieModule.ker R L M = ⊥

Tactic:
by
  rw [isFaithful_iff', LieSubmodule.ext_iff]
  aesop

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

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
c : R
x : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
y : L
⊢ ⁅y, c • x⁆ = 0

Tactic:
rw [lie_smul, hx, smul_zero]

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
⊢ Submodule.comap (↑N).subtype ↑N = ⊤

Tactic:
rw [Submodule.comap_subtype_self]

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
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ (algebraMap A B).range

Tactic:
rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add,
    aeval_C, aeval_X, ← eq_neg_iff_add_eq_zero, ← map_neg] at key

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : x = (algebraMap A B) (-(minpoly A x).coeff 0)
⊢ x ∈ (algebraMap A B).range
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
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) f = 0 ∨ (Polynomial.aeval x) g = 0
⊢ False

Tactic:
rcases heval with heval | heval

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
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) f = 0
⊢ False

case inr
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) g = 0
⊢ False
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: A : Type u_3
inst✝ : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : x₁ ≡ y₁ [SMOD I]
hxy₂ : x₂ ≡ y₂ [SMOD I]
⊢ x₁ * x₂ ≡ y₁ * y₂ [SMOD I]

Tactic:
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
  rw [hxy₁, hxy₂]

Goal state after: