mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : 0 ≫ g' = 0
⊢ Mono (𝟙 S.X₃)

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : 0 ≫ g' = 0
⊢ Mono (𝟙 S.X₃)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁

Tactic:
s.f_r_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j) =
    h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)

Tactic:
;

Goal state after:
case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j) =
    h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Mono S₁.g.op

Tactic:
;

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Mono S₁.g.op
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono S₂.g.op

Tactic:
;

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono S₂.g.op
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono φ.τ₃.op

Tactic:
;

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono φ.τ₃.op
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ (g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom =
    (h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom

Tactic:
;

Goal state after:
case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ (g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom =
    (h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono φ.τ₁.op

Tactic:
;

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono φ.τ₁.op
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ Over.Hom.left
      ((fun k ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) ⋯)
        ((fun k ↦ homMk (image.lift { I := g.obj.left, m := g.arrow, m_mono := ⋯, e := Over.Hom.left k, fac := ⋯ }) ⋯)
          k)) =
    Over.Hom.left k

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ Over.Hom.left
      ((fun k ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) ⋯)
        ((fun k ↦ homMk (image.lift { I := g.obj.left, m := g.arrow, m_mono := ⋯, e := Over.Hom.left k, fac := ⋯ }) ⋯)
          k)) =
    Over.Hom.left k
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0

Tactic:
simp [imageToKernel']

Goal state after:
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageToKernel' f g w ≫ (kernelSubobjectIso g).inv) ≫ (kernelSubobject g).arrow =
    ((imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow

Tactic:
simp [imageToKernel']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ ((kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ ((kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
x✝¹ : Cᵒᵖ
x✝ : Subobject (Opposite.unop x✝¹)
⊢ (ConcreteCategory.hom (↾(pullback (𝟙 x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (𝟙 (Subobject (Opposite.unop x✝¹)))).toFun x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
x✝¹ : Cᵒᵖ
x✝ : Subobject (Opposite.unop x✝¹)
⊢ (ConcreteCategory.hom (↾(pullback (𝟙 x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (𝟙 (Subobject (Opposite.unop x✝¹)))).toFun x✝
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Subobject (Opposite.unop X✝)
⊢ (ConcreteCategory.hom (↾(pullback (x✝² ≫ x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (↾(pullback x✝².unop).obj ≫ ↾(pullback x✝¹.unop).obj)).toFun x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Subobject (Opposite.unop X✝)
⊢ (ConcreteCategory.hom (↾(pullback (x✝² ≫ x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (↾(pullback x✝².unop).obj ≫ ↾(pullback x✝¹.unop).obj)).toFun x✝
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map S.g = L.map (cokernel.π (kernel.ι S.g)) ≫ L.map (Abelian.factorThruCoimage S.g)

Tactic:
← L.map_comp,

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map S.g = L.map (cokernel.π (kernel.ι S.g) ≫ Abelian.factorThruCoimage S.g)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f) ≫ L.map (kernel.ι (cokernel.π S.f)) = L.map S.f

Tactic:
← L.map_comp,

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f)) = L.map S.f
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶
  { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }.map L := ⋯
⊢ ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }.map L).Exact

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶
  { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }.map L := ⋯
⊢ IsLimit
    (KernelFork.ofι
      ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }.map L).f ⋯)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (∐ fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f

Tactic:
refine Sigma.desc ?_

Goal state after:
case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (b : ↑(⇑(equivShrink (Subobject A)) '' s)) → underlying.obj ((equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (Sigma.map fun x ↦ x✝.app ↑x) ≫ (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
      colimMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (Sigma.map fun x ↦ x✝.app ↑x) ≫ (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
      colimMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
b✝ : ↥I
⊢ Sigma.ι (fun x ↦ X✝.obj ↑x) b✝ ≫
      (Sigma.map fun x ↦ x✝.app ↑x) ≫ (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    Sigma.ι (fun x ↦ X✝.obj ↑x) b✝ ≫
      (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
        colimMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
b✝ : ↥I
⊢ Sigma.ι (fun x ↦ X✝.obj ↑x) b✝ ≫
      (Sigma.map fun x ↦ x✝.app ↑x) ≫ (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    Sigma.ι (fun x ↦ X✝.obj ↑x) b✝ ≫
      (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
        colimMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteProducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (Pi.map fun x ↦ x✝.app ↑x) ≫ (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
      limMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteProducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (Pi.map fun x ↦ x✝.app ↑x) ≫ (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
      limMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteProducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
j✝ : Discrete ↥I
⊢ ((Pi.map fun x ↦ x✝.app ↑x) ≫ (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom) ≫
      limit.π ((Discrete.functor fun x ↦ ↑x) ⋙ Y✝) j✝ =
    ((HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
        limMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)) ≫
      limit.π ((Discrete.functor fun x ↦ ↑x) ⋙ Y✝) j✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteProducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
j✝ : Discrete ↥I
⊢ ((Pi.map fun x ↦ x✝.app ↑x) ≫ (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom) ≫
      limit.π ((Discrete.functor fun x ↦ ↑x) ⋙ Y✝) j✝ =
    ((HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
        limMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)) ≫
      limit.π ((Discrete.functor fun x ↦ ↑x) ⋙ Y✝) j✝
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
x✝ : C
⊢ ((𝟭 (C ⥤ H)).map φ ≫ L.leftKanExtensionUnit F₂).app x✝ =
    (L.leftKanExtensionUnit F₁ ≫ (L.lan ⋙ (whiskeringLeft C D H).obj L).map φ).app x✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
x✝ : C
⊢ ((𝟭 (C ⥤ H)).map φ ≫ L.leftKanExtensionUnit F₂).app x✝ =
    (L.leftKanExtensionUnit F₁ ≫ (L.lan ⋙ (whiskeringLeft C D H).obj L).map φ).app x✝
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
x✝ : C
⊢ ((L.ran ⋙ (whiskeringLeft C D H).obj L).map φ ≫ L.rightKanExtensionCounit F₂).app x✝ =
    (L.rightKanExtensionCounit F₁ ≫ (𝟭 (C ⥤ H)).map φ).app x✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
x✝ : C
⊢ ((L.ran ⋙ (whiskeringLeft C D H).obj L).map φ ≫ L.rightKanExtensionCounit F₂).app x✝ =
    (L.rightKanExtensionCounit F₁ ≫ (𝟭 (C ⥤ H)).map φ).app x✝
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₁ (η ≫ μ) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₁ μ ∘ map₁ η) x✝²).fst.app x✝¹)).toFun x✝

pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (H.map (eqToHom ⋯))) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd

Tactic:
;

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₁ (η ≫ μ) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₁ μ ∘ map₁ η) x✝²).fst.app x✝¹)).toFun x✝

case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (H.map (eqToHom ⋯))) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (𝟙 X) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((id x✝²).fst.app x✝¹)).toFun x✝

pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd

Tactic:
;

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (𝟙 X) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((id x✝²).fst.app x✝¹)).toFun x✝

case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd