mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
⊢ L.IsLeftKanExtension α ↔
    IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ L.IsLeftKanExtension e.hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X)) ≫
      ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map
        (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X)) ≫
      ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map
        (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y

Tactic:
by
        ext Z f
        convert! (Y.hom.naturality_apply f.op _).symm
        simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
φ : Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ φ = StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X)) ≫
      ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
φ : Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X) ⟶ Y
⊢ φ = StructuredArrow.homMk (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y))) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
h✝ : P.IsSeparating
D : Type u_1
inst✝ : Category.{v_1, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : P Z
h : Z ⟶ α.inverse.obj X
⊢ h ≫ α.inverse.map f = h ≫ α.inverse.map g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
h✝ : P.IsCoseparating
D : Type u_1
inst✝ : Category.{v_1, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : P Z
h : α.inverse.obj Y ⟶ Z
⊢ α.inverse.map f ≫ h = α.inverse.map g ≫ h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ Subobject A → Subobject A.right

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)).inv) ≫
      T.map (projectSubobject (Subobject.mk f)).arrow =
    A.hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
⊢ P.op.IsSeparating ↔ P.IsCoseparating

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
t : zero = one
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
t : one = zero
⊢ False

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
⊢ P.op.IsCoseparating ↔ P.IsSeparating

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
⊢ (F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
      ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).leftKanExtensionUnique (uliftYonedaMap F Y)
          (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj Y))
          (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).hom =
    ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).leftKanExtensionUnique (uliftYonedaMap F X)
          (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
          (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).hom ≫
      (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (hom ((uliftYonedaMap F X).app (op X))) { down := 𝟙 X } = { down := 𝟙 (F.obj X) }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
⊢ uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd) =
    uliftYonedaEquiv (uliftYonedaEquiv.symm y.snd)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ ((mk q).hom ≫ T.map (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)).hom) ≫ T.map (Hom.right f) =
    P.hom ≫ T.map (Hom.right f)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' ↦ f.unop ≫ h' = h) y
⊢ (y.op ≫ f).unop = h.op.unop

Tactic:
simpa only using! hy

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' ↦ f.unop ≫ h' = h) y
⊢ (y.op ≫ f).unop = h.op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
⊢ P.op.IsDetecting ↔ P.IsCodetecting

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ Hom.right ((isoMk (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)) ⋯).hom ≫ f) =
    Hom.right (homMk (projectSubobject (Subobject.mk f)).arrow hq)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun h' ↦ h' ≫ f.unop = h) y
⊢ (f ≫ y.op).unop = h.op.unop

Tactic:
simpa only using! hy

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ ∀ ⦃A_1 : StructuredArrow S T⦄ (f : A_1 ⟶ A) [inst : Mono f]
    {q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))}
    (hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom),
    liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun h' ↦ h' ≫ f.unop = h) y
⊢ (f ≫ y.op).unop = h.op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
⊢ P.op.IsCodetecting ↔ P.IsDetecting

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : HasCoequalizers C
⊢ P.IsCodetecting → P.IsCoseparating

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
P : { P // ∃ q, q ≫ T.map P.arrow = A.hom }
⊢ ↑((fun P ↦ ⟨projectSubobject P, ⋯⟩) ((fun P ↦ liftSubobject ↑P ⋯) P)) = ↑P

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
x✝⁴ : Mono f
x✝³ : C
x✝² : P x✝³
x✝¹ x✝ : x✝³ ⟶ X
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (g₁ g₂ : G ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ = g₂
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
h : g₁ ≫ f = g₂ ≫ f
G : C
hG : P G
h' : G ⟶ Z✝
⊢ (h' ≫ g₁) ≫ f = (h' ≫ g₂) ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : C
f : X ⟶ Y
x✝⁴ : Epi f
x✝³ : C
x✝² : P x✝³
x✝¹ x✝ : Y ⟶ x✝³
h : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (g₁ g₂ : Y ⟶ G), f ≫ g₁ = f ≫ g₂ → g₁ = g₂
Z✝ : C
g₁ g₂ : Y ⟶ Z✝
h : f ≫ g₁ = f ≫ g₂
G : C
hG : P G
h' : Z✝ ⟶ G
⊢ f ≫ g₁ ≫ h' = f ≫ g₂ ≫ h'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X_1 Y_1 Z : WalkingParallelFamily J} (f_1 : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    (match X_1, Z, f_1 ≫ g with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) =
      (match X_1, Y_1, f_1 with
        | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
        | .(zero), .(one), line j => f j) ≫
        match Y_1, Z, g with
        | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
        | .(zero), .(one), line j => f j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ ∀ {X Y : WalkingParallelFamily J} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
⊢ P.IsDetecting

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
X : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj X =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      X

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h :
  { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)
⊢ (P.hom ≫ T.map (Subobject.ofMkLEMk (Hom.right (MonoOver.mk f).arrow) (Hom.right (MonoOver.mk g).arrow) h)) ≫
      T.map (Hom.right g) =
    Q.hom ≫ T.map (Hom.right g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X Y : WalkingParallelFamily (ULift.{w, 0} Bool)} (f : X ⟶ Y),
    (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map f ≫ (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
              parallelPair (line { down := true }) (line { down := false })).map
          f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
X : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      X =
    (𝟭 WalkingParallelPair).obj X

Tactic:
by

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)

Tactic:
refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_

Goal state after:
case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Hom.right (Subobject.ofMkLEMk f g h) ≫ Hom.right (MonoOver.mk g).arrow = Hom.right (MonoOver.mk f).arrow
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ IsIso f ↔ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (parallelPair (line { down := true }) (line { down := false }) ⋙
              parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          f ≫
        (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ ∀ {a b : Subobject A},
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ (X : WalkingParallelFamily (ULift.{w, 0} Bool)),
    (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
            X) ≫
        (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
          ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
            X) =
      𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
⊢ s.π.app zero ≫ f j = s.π.app one

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = s.ι.app zero

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
⊢ Subobject (op A) → Subobject (op A.left)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f✝ j₁ = ι ≫ f✝ j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map f ≫
      WalkingParallelFamily.casesOn j ι (ι ≫ f✝ (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f✝ (Classical.arbitrary J)) ≫ (parallelFamily f✝).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫
      S.map (Subobject.underlyingIso (MonoOver.mk f).arrow.unop.left.op).unop.inv ≫ (unop P).hom =
    A.hom

Tactic:
by

Goal state after: