mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ (kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0 = 𝟙 (kernel t) ≫ equalizer.ι t 0

Tactic:
;

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ (kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0 = 𝟙 (kernel t) ≫ equalizer.ι t 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    coequalizer.π b 0 ≫ 𝟙 (cokernel b)

Tactic:
;

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    coequalizer.π b 0 ≫ 𝟙 (cokernel b)
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
ha : a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
ha : a ∈ (ModuleCat.Hom.hom y.hom).range
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
⊢ P (Abelian.image f)

Tactic:
rw [← exists_epiModSerre_comp_eq_zero_iff P]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
⊢ ∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ f = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
inst✝⁴ : L.IsLocalization P.isoModSerre
inst✝³ : Preadditive D
inst✝² : L.Additive
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ L.map f ≫ L.map g = 0 ↔ P Z

Tactic:
← L.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
inst✝⁴ : L.IsLocalization P.isoModSerre
inst✝³ : Preadditive D
inst✝² : L.Additive
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ L.map (f ≫ g) = 0 ↔ P Z
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Mono (L.map f)
⊢ L.map (kernel.ι f) ≫ L.map f = 0

Tactic:
← L.map_comp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Mono (L.map f)
⊢ L.map (kernel.ι f ≫ f) = 0
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯)).pt

Tactic:
· exact P.prop_cokernel f.hom X.property Y.property

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map f ≫ L.map (cokernel.π f) = 0

Tactic:
← L.map_comp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map (f ≫ cokernel.π f) = 0
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
x✝¹ : SingleObj M
x✝ : X
⊢ (ConcreteCategory.hom (↾fun x ↦ 𝟙 x✝¹ • x)).toFun x✝ = (ConcreteCategory.hom (𝟙 X)).toFun x✝

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
x✝¹ : SingleObj M
x✝ : X
⊢ (ConcreteCategory.hom (↾fun x ↦ 𝟙 x✝¹ • x)).toFun x✝ = (ConcreteCategory.hom (𝟙 X)).toFun x✝
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
X✝ Y✝ Z✝ : SingleObj M
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : X
⊢ (ConcreteCategory.hom (↾fun x ↦ f ≫ g • x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x)).toFun x

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
X✝ Y✝ Z✝ : SingleObj M
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : X
⊢ (ConcreteCategory.hom (↾fun x ↦ f ≫ g • x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x)).toFun x
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: case mk
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
fst✝ : SingleObj M
snd✝ : (actionAsFunctor M X).obj fst✝
⊢ ⟨(), ActionCategory.back ⟨fst✝, snd✝⟩⟩ = ⟨fst✝, snd✝⟩

Tactic:
;

Goal state after:
case mk
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
fst✝ : SingleObj M
snd✝ : (actionAsFunctor M X).obj fst✝
⊢ ⟨(), ActionCategory.back ⟨fst✝, snd✝⟩⟩ = ⟨fst✝, snd✝⟩
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
x✝ : Function.End X
⊢ (fun f ↦ ⇑(ConcreteCategory.hom f)) ((fun f ↦ ↾f) x✝) = x✝

Tactic:
;

Goal state after:
X : Type u
x✝ : Function.End X
⊢ (fun f ↦ ⇑(ConcreteCategory.hom f)) ((fun f ↦ ↾f) x✝) = x✝
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
x✝ : End X
⊢ (fun f ↦ ↾f) ((fun f ↦ ⇑(ConcreteCategory.hom f)) x✝) = x✝

Tactic:
;

Goal state after:
X : Type u
x✝ : End X
⊢ (fun f ↦ ↾f) ((fun f ↦ ⇑(ConcreteCategory.hom f)) x✝) = x✝
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s

Tactic:
simp [reassoc_of% hφ]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ ⟨x✝ * y✝, 1⟩ = ⟨x✝, 1⟩ * ⟨y✝, 1⟩

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ ⟨x✝ * y✝, 1⟩ = ⟨x✝, 1⟩ * ⟨y✝, 1⟩
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ ⟨1, x✝ * y✝⟩ = ⟨1, x✝⟩ * ⟨1, y✝⟩

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ ⟨1, x✝ * y✝⟩ = ⟨1, x✝⟩ * ⟨1, y✝⟩
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : N
⊢ (rightHom.comp inl) x✝ = 1 x✝

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : N
⊢ (rightHom.comp inl) x✝ = 1 x✝
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : G
⊢ (rightHom.comp inr) x✝ = (MonoidHom.id G) x✝

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : G
⊢ (rightHom.comp inr) x✝ = (MonoidHom.id G) x✝
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : N
⊢ ((lift fn fg h).comp inl) x✝ = fn x✝

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : N
⊢ ((lift fn fg h).comp inl) x✝ = fn x✝
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : G
⊢ ((lift fn fg h).comp inr) x✝ = fg x✝

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : G
⊢ ((lift fn fg h).comp inr) x✝ = fg x✝
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ((F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝¹))) x✝ =
    ((MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝¹))).comp (F.comp inl)) x✝

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ((F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝¹))) x✝ =
    ((MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝¹))).comp (F.comp inl)) x✝
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))
x✝¹ : G₁
x✝ : N₁
⊢ (MulEquiv.trans (φ₁ x✝¹) fn) x✝ = (fn.trans (((↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)) (fg x✝¹))) x✝

Tactic:
;

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))
x✝¹ : G₁
x✝ : N₁
⊢ (MulEquiv.trans (φ₁ x✝¹) fn) x✝ = (fn.trans (((↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)) (fg x✝¹))) x✝
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (x : F ⟶ G), 0 • x = 0

Tactic:
by
        intros
        ext
        apply zero_smul

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Tactic:
by
  rw [← comp_hom, Iso.inv_hom_id, id_hom]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
w : (M.ρ g ≫ f.hom) ≫ f.inv = (f.hom ≫ N.ρ g) ≫ f.inv
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
w : (M.ρ g ≫ f.hom) ≫ f.inv = (f.hom ≫ N.ρ g) ≫ f.inv
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
w : M.ρ g = f.hom ≫ N.ρ g ≫ f.inv
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
w : M.ρ g = f.hom ≫ N.ρ g ≫ f.inv
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = x✝
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ↑⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = ↑x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ↑⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = ↑x✝
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ ConcreteCategory.hom { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ }.hom =
    ConcreteCategory.hom x✝.hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ ConcreteCategory.hom { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ }.hom =
    ConcreteCategory.hom x✝.hom
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ ((forget V G).mapIso f).hom ≫ N.ρ g = M.ρ g ≫ ((forget V G).mapIso f).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ ((forget V G).mapIso f).hom ≫ N.ρ g = M.ρ g ≫ ((forget V G).mapIso f).hom
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
l : L.obj (cokernel f) ⟶ L.obj φ.Y'
hl : L.map (cokernel.π f) ≫ l = L.map φ.f
⊢ L.map (cokernel.π f) ≫ l ≫ inv (L.map φ.s) ≫ (L.objObjPreimageIso W).hom = w

Tactic:
by simp [reassoc_of% hl, ← hφ]

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).hom = (f✝ ≫ g✝ + f'✝ ≫ g✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).hom = (f✝ ≫ g✝ + f'✝ ≫ g✝).hom
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
x✝ : H
⊢ (MonoidHom.id H) x✝ = ((↑f).comp ↑f.symm) x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
x✝ : H
⊢ (MonoidHom.id H) x✝ = ((↑f).comp ↑f.symm) x✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
x✝ : G
⊢ ((↑f.symm).comp ↑f) x✝ = (MonoidHom.id G) x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
x✝ : G
⊢ ((↑f.symm).comp ↑f) x✝ = (MonoidHom.id G) x✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).hom = (f✝ ≫ g✝ + f✝ ≫ g'✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).hom = (f✝ ≫ g✝ + f✝ ≫ g'✝).hom
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : (f ≫ z) ≫ t = 0
⊢ ∃ l, L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯

Tactic:
rw [Category.assoc] at fac

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
⊢ ∃ l, L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ ((x✝ * y✝) • b✝).hom = (x✝ • y✝ • b✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ ((x✝ * y✝) • b✝).hom = (x✝ • y✝ • b✝).hom