mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Injective J

Tactic:
rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']
  have := Functor.preservesHomologyOfExact (preadditiveYonedaObj J)
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) → IsZero (Ψ.r.obj (Φ.quotient.obj X))

pp: case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsZero (Ψ.r.obj (Φ.quotient.obj X)) → IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)

Tactic:
<;>

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) → IsZero (Ψ.r.obj (Φ.quotient.obj X))

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsZero (Ψ.r.obj (Φ.quotient.obj X)) → IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ desc (𝟙 X) I I = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι

pp: case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ 𝟙 I.cocomplex = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι

Tactic:
<;>

Goal state after:
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ desc (𝟙 X) I I = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι

case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ 𝟙 I.cocomplex = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
apply descHomotopy (𝟙 X) <;> simp

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

Goal state before:
pp: case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc (f ≫ g) K I = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι

pp: case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc f J I ≫ desc g K J = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι

Tactic:
<;>

Goal state after:
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc (f ≫ g) K I = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι

case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc f J I ≫ desc g K J = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X 0)

pp: case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X (0 + 1))

pp: case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X (0 + 1 + 1))

pp: case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X (n + 1 + 1 + 1))

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X 0)

case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X (0 + 1))

case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X (0 + 1 + 1))

case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X (n + 1 + 1 + 1))
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f) =
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f)

Tactic:
rw [← Category.assoc, pullback.condition]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Abelian D
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
⊢ P ≤ F.kernel

Tactic:
intro X hX

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Abelian D
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
hX : P X
⊢ F.kernel X
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
⊢ G.kernel.isoModSerre = (isomorphisms C).inverseImage G

Tactic:
by
  ext X Y f
  refine ⟨(G.kernel.isoModSerre_isInvertedBy_iff G).2 (by rfl) _, fun hf ↦ ?_⟩
  simp only [inverseImage_iff, isomorphisms.iff] at hf
  constructor
  · exact KernelFork.IsLimit.isZero_of_mono
      (KernelFork.mapIsLimit _ (kernelIsKernel f) G)
  · exact CokernelCofork.IsColimit.isZero_of_epi
      (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
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⟩.left = (⟨x✝, 1⟩ * ⟨y✝, 1⟩).left

pp: case right
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⟩.right = (⟨x✝, 1⟩ * ⟨y✝, 1⟩).right

Tactic:
<;>

Goal state after:
case left
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⟩.left = (⟨x✝, 1⟩ * ⟨y✝, 1⟩).left

case right
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⟩.right = (⟨x✝, 1⟩ * ⟨y✝, 1⟩).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
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✝⟩.left = (⟨1, x✝⟩ * ⟨1, y✝⟩).left

pp: case right
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✝⟩.right = (⟨1, x✝⟩ * ⟨1, y✝⟩).right

Tactic:
<;>

Goal state after:
case left
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✝⟩.left = (⟨1, x✝⟩ * ⟨1, y✝⟩).left

case right
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✝⟩.right = (⟨1, x✝⟩ * ⟨1, y✝⟩).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ (inl ((φ g) n)).left = (inr g * inl n * inr g⁻¹).left

pp: case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ (inl ((φ g) n)).right = (inr g * inl n * inr g⁻¹).right

Tactic:
<;>

Goal state after:
case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ (inl ((φ g) n)).left = (inr g * inl n * inr g⁻¹).left

case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ (inl ((φ g) n)).right = (inr g * inl n * inr g⁻¹).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ ⟨n, g⟩.left = (inl n * inr g).left

pp: case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ ⟨n, g⟩.right = (inl n * inr g).right

Tactic:
<;>

Goal state after:
case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ ⟨n, g⟩.left = (inl n * inr g).left

case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ ⟨n, g⟩.right = (inl n * inr g).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (inl x.left * inr x.right).left = x.left

pp: case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (inl x.left * inr x.right).right = x.right

Tactic:
<;>

Goal state after:
case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (inl x.left * inr x.right).left = x.left

case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (inl x.left * inr x.right).right = x.right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ rightHom.ker
⊢ (inl x.left).left = x.left

pp: case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ rightHom.ker
⊢ (inl x.left).right = x.right

Tactic:
<;>

Goal state after:
case left
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ rightHom.ker
⊢ (inl x.left).left = x.left

case right
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ rightHom.ker
⊢ (inl x.left).right = x.right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
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₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.left = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).left

pp: case right
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₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.right = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).right

Tactic:
<;>

Goal state after:
case left
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₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.left = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).left

case right
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₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.right = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : N₁
⊢ (((map fn fg h).comp inl) x✝).left = ((inl.comp fn) x✝).left

pp: case right
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : N₁
⊢ (((map fn fg h).comp inl) x✝).right = ((inl.comp fn) x✝).right

Tactic:
<;>

Goal state after:
case left
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : N₁
⊢ (((map fn fg h).comp inl) x✝).left = ((inl.comp fn) x✝).left

case right
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : N₁
⊢ (((map fn fg h).comp inl) x✝).right = ((inl.comp fn) x✝).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : G₁
⊢ (((map fn fg h).comp inr) x✝).left = ((inr.comp fg) x✝).left

pp: case right
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : G₁
⊢ (((map fn fg h).comp inr) x✝).right = ((inr.comp fg) x✝).right

Tactic:
<;>

Goal state after:
case left
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : G₁
⊢ (((map fn fg h).comp inr) x✝).left = ((inr.comp fg) x✝).left

case right
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₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x✝ : G₁
⊢ (((map fn fg h).comp inr) x✝).right = ((inr.comp fg) x✝).right
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
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₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.left = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).left

pp: case right
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₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.right = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).right

Tactic:
<;>

Goal state after:
case left
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₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.left = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).left

case right
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₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.right = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).right
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 0 =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 0

pp: case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
i✝ : Fin n
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 i✝.succ =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 i✝.succ

Tactic:
<;>

Goal state after:
case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 0 =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 0

case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
i✝ : Fin n
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 i✝.succ =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 i✝.succ
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ X Y').symm (L.map g ≫ h) =
    g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ Y Y').symm h

Tactic:
rw [constructRightAdjointEquiv_symm_apply, constructRightAdjointEquiv_symm_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ ↑⟨(adj₂.homEquiv X (F.obj Y'))
          ((adj₁.homEquiv (L.obj X) (F.obj Y')).symm
            ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h))),
        ⋯⟩ =
    ↑((Fork.IsLimit.homIso
          (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) X)
        (g ≫
          (Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                ((adj₁.homEquiv (L.obj Y) (F.obj Y')).symm
                  ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h)),
              ⋯⟩))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
⊢ L.IsLeftAdjoint

Tactic:
let L' : _ ⥤ _ := L ⋙ Comonad.comparison (comonadicAdjunction F)

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ L.IsLeftAdjoint