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

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (limit.lift
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    s.π.app j

Tactic:
· simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫ 𝟙 ((StructuredArrow.right E).obj Y)

Tactic:
← CostructuredArrow.w φ

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map (L.map φ.left ≫ g₂.hom)) ≫
      𝟙 ((StructuredArrow.right E).obj Y)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
X : C
h : E.IsPointwiseLeftKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((StructuredArrow.hom E).app X)

Tactic:
simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E✝ E'✝ : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫ (CostructuredArrow.hom E).app G.right

Tactic:
← CostructuredArrow.w φ

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E✝ E'✝ : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫
      (((whiskeringLeft C D H).obj L).map φ.left ≫ CostructuredArrow.hom E').app G.right
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
this✝ : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
this : HasKernel (G.map (F.map f) ≫ i.hom.app Y)
⊢ HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)

Tactic:
apply Limits.hasKernel_iso_comp

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
    ext : 1
    apply uliftYonedaEquiv.injective
    simp [← StructuredArrow.w φ, uliftYonedaEquiv, uliftYonedaMap]

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:
obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective h
    simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
      H _ (P.strictMap_obj _ hZ) h']

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: case refine_2
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)
⊢ homMk (Subobject.ofMkLEMk (Hom.right (MonoOver.mk f).arrow) (Hom.right (MonoOver.mk g).arrow) h) ⋯ ≫ g = f

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:
· simp

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
⊢ { 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)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
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 : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (Hom.id i) ≫
      WalkingParallelFamily.casesOn i ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (Hom.id i)

pp: case line
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₂
k : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (line k) ≫
      WalkingParallelFamily.casesOn one ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn zero ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (line k)

Tactic:
· simp

Goal state after:
case line
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₂
k : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (line k) ≫
      WalkingParallelFamily.casesOn one ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn zero ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (line k)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

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

pp: case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
k : J
⊢ (parallelFamily f).map (line k) ≫ WalkingParallelFamily.casesOn one (f (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn zero (f (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map (line k)

Tactic:
· simp

Goal state after:
case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
k : J
⊢ (parallelFamily f).map (line k) ≫ WalkingParallelFamily.casesOn one (f (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn zero (f (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map (line k)
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
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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        (F.op.lan.map f ≫ (F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        ((F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P) ≫ G.map f)

Tactic:
have eq := F.op.lanUnit.naturality f

Goal state after:
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
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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max w v₁ v₂))).map f ≫ F.op.lanUnit.app Q =
    F.op.lanUnit.app P ≫ (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w v₁ v₂))).obj F.op).map f
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        (F.op.lan.map f ≫ (F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        ((F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P) ≫ G.map f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
⊢ HasInitial C

Tactic:
have := hasFiniteLimits_of_hasLimitsOfSize C
  have := hasProductsOfShape_of_small C (Subtype P)
  have := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)
  let := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : Subtype P → C)))
  suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
    exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)
  have := hP.mono_productTo
  refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
  · let s : ∏ᶜ (Subtype.val (p := P)) ⟶ ∏ᶜ P.productToFamily A :=
      Pi.lift (fun f ↦ Pi.π Subtype.val ⟨f.right.obj, f.right.property⟩)
    exact Subobject.ofLEMk _
      (pullback.fst _ _ : pullback s (P.productTo A) ⟶ _) bot_le ≫ pullback.snd _ _
  · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
      apply this
    intro g
    suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
    exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
      ext
      simp⟩

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

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
P : ObjectProperty C
hP : P.IsCoseparating
⊢ (P.inverseImage (proj S T)).IsCoseparating

Tactic:
refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)
  exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))

Tactic:
let G := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj X

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))

Tactic:
let c := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsColimit (BinaryCofan.mk f (↾Subtype.val))

Tactic:
apply Nonempty.some

Goal state after:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Nonempty (IsColimit (BinaryCofan.mk f (↾Subtype.val)))
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
⊢ f (↑0 * c) = 0

Tactic:
by rwa [Nat.cast_zero, zero_mul]

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inl.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inl.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inl.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
· exact Or.inl (Or.inl ⟨hab, hbc⟩)

Goal state after:
case inl.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

case inl.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inl.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a