mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : (Functor.const (Under j₁)).obj X ⟶ D' :=
  { app := fun k ↦ s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj k).hom f', naturality := ⋯ }
k : Under j₁
⊢ s'.app k ≫ c'.ι.app k = p ≫ q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsArtinianObject X ↔ ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ (M.tensorBimod N).whiskerLeft f =
    (M.associatorBimod N P).hom ≫ M.whiskerLeft (N.whiskerLeft f) ≫ (M.associatorBimod N P').inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ IsArtinianObject X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isArtinianObject 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ localEpi (fun x ↦ x ∈ Set.range G.obj) f ↔ Epi (F.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsArtinianObject Y
⊢ IsArtinianObject X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ whiskerRight (f ≫ g) Q = whiskerRight f Q ≫ whiskerRight g Q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hY : isArtinianObject Y✝
⊢ isArtinianObject X✝

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
⊢ (localEpi fun x ↦ x ∈ Set.range G.obj) = (MorphismProperty.epimorphisms D).inverseImage F

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
⊢ G.essImage.localEpi = (MorphismProperty.epimorphisms D).inverseImage F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
⊢ ∃ Y, Simple (underlying.obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y : C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
⊢ Mono (simpleSubobjectArrow h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (f : ℕ → Subobject X), ¬StrictMono f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ IsNoetherianObject X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsNoetherianObject Y
⊢ IsNoetherianObject X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hY : isNoetherianObject Y✝
⊢ isNoetherianObject X✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
⊢ P.ind (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsStableUnderShift A
a : A
X Y : C
hY : P Y
i : X ⟶ Y
r : Y ⟶ X
w : i ≫ r = 𝟙 X
⊢ (shiftFunctor C a).map i ≫ (shiftFunctor C a).map r = 𝟙 ((shiftFunctor C a).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsStableUnderShift A
a : A
⊢ P.retractClosure ≤ P.retractClosure.shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ofObj X (X i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
⊢ P.limitsClosure J ≤ (P.limitsClosure J).shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
X₁ : C₁
hX₁ : Q₁ X₁
e₁ : f.left ≅ X₁
X₂ : C₂
hX₂ : Q₂ X₂
e₂ : f.right ≅ X₂
⊢ comma F₁ F₂ Q₁ Q₂ { left := X₁, right := X₂, hom := F₁.map e₁.inv ≫ f.hom ≫ F₂.map e₂.hom }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
⊢ Function.Surjective fun i ↦ ⟨X i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
⊢ ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ whiskerRight f (regular Y) = M.rightUnitorBimod.hom ≫ f ≫ N.rightUnitorBimod.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : R ∈ K.coverings X
Y : C
f : Y ⟶ X
hf : R f
hX : P X
⊢ P Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : R ∈ K.coverings X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
⊢ P X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
K L : Precoverage C
⊢ ∀ {X : C} {R : Presieve X}, R ∈ K.coverings X → ∀ {Y : C} (f : Y ⟶ X), R f → ⊤ X → ⊤ Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
K L : Precoverage C
⊢ ∀ {X : C} {R : Presieve X}, R ∈ K.coverings X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → ⊤ Y) → ⊤ X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
α β : F ⟶ G
⊢ T.map (α.f + β.f) ≫ G.a = F.a ≫ (α.f + β.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
⊢ T.map 0 ≫ G.a = F.a ≫ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
n : ℕ
α : F ⟶ G
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
α : F ⟶ G
⊢ T.map (-α.f) ≫ G.a = F.a ≫ (-α.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
α β : F ⟶ G
⊢ T.map (α.f - β.f) ≫ G.a = F.a ≫ (α.f - β.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
r : ℤ
α : F ⟶ G
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f + β.f) = (α.f + β.f) ≫ G.a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
⊢ F.a ≫ U.map 0 = 0 ≫ G.a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
n : ℕ
α : F ⟶ G
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
α : F ⟶ G
⊢ F.a ≫ U.map (-α.f) = (-α.f) ≫ G.a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f - β.f) = (α.f - β.f) ≫ G.a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
r : ℤ
α : F ⟶ G
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f + β.f) ≫ A₂.str = A₁.str ≫ (α.f + β.f)

Tactic:
simp only [Functor.map_add, add_comp, Endofunctor.Algebra.Hom.h, comp_add]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f + β.f) ≫ A₂.str = A₁.str ≫ (α.f + β.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
⊢ F.map 0 ≫ A₂.str = A₁.str ≫ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
α : A₁ ⟶ A₂
⊢ F.map (-α.f) ≫ A₂.str = A₁.str ≫ (-α.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f - β.f) ≫ A₂.str = A₁.str ≫ (α.f - β.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f + β.f) = (α.f + β.f) ≫ A₂.str

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
⊢ A₁.str ≫ F.map 0 = 0 ≫ A₂.str

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (-α.f) = (-α.f) ≫ A₂.str

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f - β.f) = (α.f - β.f) ≫ A₂.str

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : LeftHomotopy f g
⊢ Hom.left (f - g) - Hom.left 0 = u.hom ≫ h.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : LeftHomotopy (f - g) 0
⊢ Hom.left f - Hom.left g = u.hom ≫ h.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
⊢ Function.LeftInverse (fun h ↦ { hom := h.hom, comm := ⋯ }) fun h ↦ { hom := h.hom, comm := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
⊢ Function.RightInverse (fun h ↦ { hom := h.hom, comm := ⋯ }) fun h ↦ { hom := h.hom, comm := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ f g : u ⟶ v
h : LeftHomotopy f g
⊢ Hom.left g - Hom.left f = u.hom ≫ (-h.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ e f g : u ⟶ v
h : LeftHomotopy e f
k : LeftHomotopy f g
⊢ Hom.left e - Hom.left g = u.hom ≫ (h.hom + k.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g f₁ g₁ f₂ g₂ : u ⟶ v
h₁ : LeftHomotopy f₁ g₁
h₂ : LeftHomotopy f₂ g₂
⊢ Hom.left (f₁ + f₂) - Hom.left (g₁ + g₂) = u.hom ≫ (h₁.hom + h₂.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ e f : u ⟶ v
h : LeftHomotopy e f
g : v ⟶ w
⊢ Hom.left (e ≫ g) - Hom.left (f ≫ g) = u.hom ≫ h.hom ≫ Hom.left g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ : u ⟶ v
f g : v ⟶ w
h : LeftHomotopy f g
e : u ⟶ v
⊢ Hom.left (e ≫ f) - Hom.left (e ≫ g) = u.hom ≫ Hom.right e ≫ h.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : RightHomotopy f g
⊢ Hom.right (f - g) - Hom.right 0 = h.hom ≫ v.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : RightHomotopy (f - g) 0
⊢ Hom.right f - Hom.right g = h.hom ≫ v.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ f g : u ⟶ v
h : RightHomotopy f g
⊢ Hom.right g - Hom.right f = (-h.hom) ≫ v.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ e f g : u ⟶ v
h : RightHomotopy e f
k : RightHomotopy f g
⊢ Hom.right e - Hom.right g = (h.hom + k.hom) ≫ v.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g f₁ g₁ f₂ g₂ : u ⟶ v
h₁ : RightHomotopy f₁ g₁
h₂ : RightHomotopy f₂ g₂
⊢ Hom.right (f₁ + f₂) - Hom.right (g₁ + g₂) = (h₁.hom + h₂.hom) ≫ v.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ e f : u ⟶ v
h : RightHomotopy e f
g : v ⟶ w
⊢ Hom.right (e ≫ g) - Hom.right (f ≫ g) = (h.hom ≫ Hom.left g) ≫ w.hom

Tactic:
by

Goal state after: