mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
⊢ f ≫ cokernel.π (coprod.desc f g) = coprod.inl ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g)

Tactic:
by
          rw [coprod.inl_desc_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Biproducts

Goal state before:
pp: G H K : AddCommGrpCat
f : G ⟶ K
g : H ⟶ K
⊢ (G.biprodIsoProd H).inv ≫ biprod.desc f g = ofHom (AddMonoidHom.fst ↑G ↑H) ≫ f + ofHom (AddMonoidHom.snd ↑G ↑H) ≫ g

Tactic:
simp [biprod.desc_eq, ← biprodIsoProd_inv_comp_fst, ← biprodIsoProd_inv_comp_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
m : cokernel (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
x✝ : b' ≫ m = s.inr
⊢ (a ≫ a') ≫ m = a ≫ s.inl

Tactic:
rw [Category.assoc, h₁]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
congr
  nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm]
  rw [leftCoset_eq_iff, mul_one]
  exact Subgroup.inv_mem _ hb

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
by rw [hg, id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ Epi S.leftHomologyπ

Tactic:
dsimp only [leftHomologyπ]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ Epi S.leftHomologyData.π
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
⊢ S₂.LeftHomologyData

Tactic:
have hi : IsLimit (KernelFork.ofι i wi) := KernelFork.IsLimit.ofι _ _
    (fun x hx => h.liftK (x ≫ inv φ.τ₂) (by rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, hx, zero_comp]))
    (fun x hx => by simp [i]) (fun x hx b hb => by
      rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, hb])

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
⊢ S₂.LeftHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
⊢ i ≫ S₁.g = 0

Tactic:
rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (opcyclesMap φ).op ≫ S₁.cyclesOpIso.inv ≫ S₁.op.iCycles = S₂.cyclesOpIso.inv ≫ cyclesMap (opMap φ) ≫ S₁.op.iCycles

Tactic:
cyclesOpIso_inv_op_iCycles,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (opcyclesMap φ).op ≫ S₁.pOpcycles.op = S₂.cyclesOpIso.inv ≫ cyclesMap (opMap φ) ≫ S₁.op.iCycles
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (h.map F).f' = F.map h.f'

Tactic:
← cancel_mono (h.map F).i,

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (h.map F).f' ≫ (h.map F).i = F.map h.f' ≫ (h.map F).i
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h₁.IsPreservedBy F
inst✝ : h₂.IsPreservedBy F
⊢ (h₁.map F).f' ≫ F.map ψ.φK = (F.mapShortComplex.map φ).τ₁ ≫ (h₂.map F).f'

Tactic:
simpa only [LeftHomologyData.map_f', F.map_comp] using! F.congr_map ψ.commf'

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasZeroMorphisms D
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : QuasiIso φ
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
this : IsIso γ.φH
⊢ QuasiIso (F.mapShortComplex.map φ)

Tactic:
rw [(γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]

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✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasZeroMorphisms D
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : QuasiIso φ
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
this : IsIso γ.φH
⊢ IsIso (F.map γ.φH)
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesMonomorphisms
I : C
hI : Injective (F.obj I)
X✝ Y✝ : C
g : X✝ ⟶ I
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
by
    obtain ⟨h, fac⟩ := hI.factors (F.map g) (F.map f)
    exact ⟨F.preimage h, F.map_injective (by simp [fac])⟩

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃

Tactic:
by
    rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]

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 : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ ∀ {Z' : C} (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' → m = cokernel.desc (kernel.ι S.g) g' ⋯

Tactic:
intro _ _ _ _ hm

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
g'✝ : S.X₂ ⟶ Z'✝
eq'✝ : S.f ≫ g'✝ = 0
m✝ : Abelian.coimage S.g ⟶ Z'✝
hm : Abelian.coimage.π S.g ≫ m✝ = g'✝
⊢ m✝ = cokernel.desc (kernel.ι S.g) g'✝ ⋯
Module: Mathlib.CategoryTheory.Subobject.Lattice

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✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ f ≤ sInf s

Tactic:
by
  fapply le_of_comm
  · exact Limits.limit.lift _ (leInfCone s f k) ≫ (underlyingIso _).inv
  · dsimp [sInf]
    rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ : (op X ⟶ ∏ᶜ fun x ↦ op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x ↦ op (Z x)) (Pi.π fun x ↦ op (Z x))).pt)
⊢ (Pi.lift fun a ↦ (π a).op) = (productIsProduct fun x ↦ op (Z x)).lift (Cofan.mk X π).op

Tactic:
· simp [productIsProduct]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : Dᵒᵖ
⊢ (map (𝟙 d).unop).toCatHom = 𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))

Tactic:
ext
    exact Functor.ext (fun ⟨_, _, _⟩ => by simp)

Goal state after:
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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((CostructuredArrow.proj L Y).obj X)).symm) ⋯
⊢ L.HasPointwiseLeftKanExtensionAt F' Y

Tactic:
rw [HasPointwiseLeftKanExtensionAt, hasColimit_iff_of_iso e]

Goal state after:
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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((CostructuredArrow.proj L Y).obj X)).symm) ⋯
⊢ HasColimit (CostructuredArrow.proj L Y ⋙ F)
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A).map f ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down =
    (uliftYonedaEquiv (y.hom ≫ g)).down ≫
      ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E).map f

Tactic:
dsimp
        rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]

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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map
        (Iso.refl
            (CostructuredArrow.mk
                (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).hom ≫
      X.hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).hom

Tactic:
by
          ext Y x
          dsimp
          simp [← NatTrans.naturality_apply]

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
y : CostructuredArrow ((whiskeringLeft C C H).obj (𝟭 C)) F₀
m : y ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)
x : C
⊢ m.left.app x = (CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯).left.app x

Tactic:
simpa using congr_app m.w x =≫ α.inv.app x

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:
rintro (_ | (_ | _)) <;> rfl

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
t : Trident fun j ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g ≫ t.π.app j' ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map g

Tactic:
by cases g <;> cat_disch

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
P : ObjectProperty C
X : C
inst✝ : HasCoproduct (P.coproductFromFamily X)
Y : C
f : Y ⟶ X
hY : P Y
⊢ P.ι.obj { obj := Y, property := hY } ⟶ X

Tactic:
exact f

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
P : ObjectProperty C
X : C
inst✝ : HasProduct (P.productToFamily X)
Y : C
f : X ⟶ Y
hY : P Y
⊢ X ⟶ P.ι.obj { obj := Y, property := hY }

Tactic:
exact f

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
inst✝ : HasSeparator C
⊢ HasCoseparator Cᵒᵖ

Tactic:
by 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
inst✝ : HasCoseparator C
⊢ HasSeparator Cᵒᵖ

Tactic:
by 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
inst✝ : HasDetector C
⊢ HasCodetector Cᵒᵖ

Tactic:
by 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
inst✝ : HasCodetector C
⊢ HasDetector Cᵒᵖ

Tactic:
by simp [*]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))))

Tactic:
have :
      (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
        (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
      colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj u.fst) (op u) :=
    IsColimit.comp_coconePointUniqueUpToIso_inv (colimit.isColimit _) _ (op u)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
this :
  (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
      (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
    colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))))
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x - ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
simpa only [zsmul_eq_mul] using h.sub_zsmul_eq n

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (a + ↑n) (a + ↑n + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ioc_add_zsmul a (1 : α)

Goal state after:
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ List.countP (fun b ↦ decide (p b)) (List.range n) = #({x ∈ range n | p x})

Tactic:
List.countP_eq_length_filter

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (List.filter (fun b ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
⊢ ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)

Tactic:
hpa

Goal state after:
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
⊢ 0 < n → motive a → motive (p ^ n * a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
let e : { m | m < n ∧ n.Coprime m } ≃ {x ∈ range n | n.Coprime x} :=
    { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property⟩
      invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property⟩
      left_inv := fun m => by simp only [Subtype.coe_eta]
      right_inv := fun m => by simp only }

Goal state after:
n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ ↥({x ∈ range n | n.Coprime x}) :=
  { toFun := fun m ↦ ⟨↑m, ⋯⟩, invFun := fun m ↦ ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1

Tactic:
rintro ⟨⟩

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
⊢ toIocMod hp a b = b - toIocDiv hp a b • p

Tactic:
toIocMod

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
⊢ b - toIocDiv hp a b • p = b - toIocDiv hp a b • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a a = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a = a + z • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a (a + p) = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a + p = a + z • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a + -m • p) b = toIocDiv hp a b + m

Tactic:
toIocDiv_add_zsmul',

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a b - -m = toIocDiv hp a b + m
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ i, (f i).lift g ≤ g univ

Tactic:
inhabit ι
      exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)

Goal state after: