mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ (S₁.mapRightHomologyIso F).hom ≫ F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
← mapRightHomologyIso_hom_naturality_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✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapRightHomologyIso F).hom ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι g.unop).op = eqToHom ⋯ ≫ cokernel.π g ≫ (kernelUnopOp g).inv

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π g.unop).op = (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom ⋯

Tactic:
by
  simp

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₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯

Tactic:
ext
  · dsimp; rw [h.comm₁]; abel
  · dsimp; rw [h.comm₂]; abel
  · dsimp; rw [h.comm₃]; abel

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
⊢ PreservesColimit (parallelPair f g) F

Tactic:
let := preservesBinaryBiproducts_of_preservesBinaryCoproducts F

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
⊢ PreservesColimit (parallelPair f g) F
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
⊢ i.essImage A

Tactic:
have : IsIso (η.app (i.obj ((reflector i).obj A))) :=
    Functor.essImage.unit_isIso ((i.obj_mem_essImage _))

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
this : IsIso (η.app (i.obj ((reflector i).obj A)))
⊢ i.essImage A
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : i.obj ((reflector i).obj A) ⟶ B
⊢ (unitCompPartialBijective A hB').symm (f ≫ h) = (unitCompPartialBijective A hB).symm f ≫ h

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
X : D
⊢ (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
    j.map ((coreflector j).map ((coreflectorAdjunction j).counit.app X))

Tactic:
rw [← cancel_epi (j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X))),
    ← j.map_comp]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
X : D
⊢ j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X)) ≫
      (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
    j.map
      ((coreflectorAdjunction j).unit.app ((coreflector j).obj X) ≫
        (coreflector j).map ((coreflectorAdjunction j).counit.app X))
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact ↔ Mono h.g'

Tactic:
by
  constructor
  · intro hS
    exact hS.mono_g' h
  · intro
    simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_mono h.ι, ← cancel_mono h.g',
      id_comp, h.ι_g', zero_comp]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject B)

Tactic:
convert! ThinSkeleton.map_iso_eq e.counitIso

Goal state after:
case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)

case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject B) = ThinSkeleton.map (𝟭 (MonoOver B))
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
x : Subobject X
⊢ (pullback (𝟙 X)).obj x = x

Tactic:
induction x using Quotient.inductionOn' with | _ f
  exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩

Goal state after:
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 : image.obj f ⟶ g
⊢ f ⟶ (forget X).obj g

Tactic:
by
            apply Over.homMk (factorThruImage f.hom ≫ k.hom.left) _
            rw [assoc, Over.w k.hom]
            apply image.fac

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
A B : C
⊢ kernelSubobject 0 = ⊤

Tactic:
by
  simp

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
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w = (imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow

Tactic:
by
  simp

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ f ≫ cokernel.π g = 0

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (cokernel.desc f (cokernel.π g) ?refine_1).op ≫ (cokernel.π f).op = (cokernel.π g).op

Tactic:
· rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (cokernel.desc f (cokernel.π g) ⋯).op ≫ (cokernel.π f).op = (cokernel.π g).op
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ᵒᵖ
⊢ ↾(pullback (𝟙 x✝).unop).obj = 𝟙 (Subobject (Opposite.unop x✝))

Tactic:
by ext : 3; simp [pullback_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
⊢ IsLimit (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) F)

Tactic:
let S := ShortComplex.mk _ _ (kernel.condition f)

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := Limits.kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }
⊢ IsLimit (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) F)
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F, PreservesFiniteColimits F].TFAE

Tactic:
by
  tfae_have 1 → 2
  | hF, S, ⟨hS, hf⟩ => by
    have := preservesEpimorphisms_of_preserves_shortExact_right F hF
    refine ⟨?_, inferInstance⟩
    let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero)
    let φ : S.map F ⟶ T.map F :=
      { τ₁ := F.map <| Abelian.factorThruImage S.f
        τ₂ := 𝟙 _
        τ₃ := 𝟙 _
        comm₁₂ := show _ ≫ F.map (kernel.ι _) = F.map _ ≫ 𝟙 _ by
          rw [← F.map_comp, Abelian.image.fac, Category.comp_id] }
    exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1
  tfae_have 2 → 3
  | hF, X, Y, f => by
    refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_
    apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
    let S := ShortComplex.mk _ _ (cokernel.condition f)
    let hS := hF S ⟨exact_cokernel f, inferInstance⟩
    have : Epi (S.map F).g := hS.2
    exact hS.1.gIsCokernel
  tfae_have 3 → 4
  | hF => by
    exact preservesFiniteColimits_of_preservesCokernels F
  tfae_have 4 → 1
  | ⟨_⟩, S, hS => (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2
    ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩
  tfae_finish

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ IsIso (coimageImageComparison α)

Tactic:
have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) := by
    intros
    rw [coimageImageComparison_app']
    infer_instance

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
this : ∀ (X : C), IsIso ((coimageImageComparison α).app X)
⊢ IsIso (coimageImageComparison α)
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ YonedaCollection.fst (counitForward F s x).val = s.hom

Tactic:
by
  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 : 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
  constructor
  · intro
    exact ⟨inferInstance, preservesColimits_of_natIso (Functor.leftKanExtensionUnique _
      (uliftYoneda.{max w v₂}.leftKanExtensionUnit A) _ α)⟩
  · rintro ⟨_, _⟩
    apply Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
      (E := Functor.LeftExtension.mk _ α)
    intro P
    dsimp [Functor.LeftExtension.IsPointwiseLeftKanExtensionAt]
    apply IsColimit.ofWhiskerEquivalence
      (CategoryOfElements.costructuredArrowULiftYonedaEquivalence _)
    let e : (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
      CostructuredArrow.proj uliftYoneda.{max w v₂} P ⋙ A ≅
        functorToRepresentables.{max w v₂} P ⋙ L :=
      Functor.isoWhiskerLeft _ (Functor.isoWhiskerLeft _ (asIso α)) ≪≫
        Functor.isoWhiskerLeft _ (Functor.associator _ _ _).symm ≪≫
        (Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight (Iso.refl _) L
    refine (IsColimit.precomposeHomEquiv e.symm _).1 ?_
    exact IsColimit.ofIsoColimit (isColimitOfPreserves L (colimitOfRepresentable.{max w v₂} P))
      (Cocone.ext (Iso.refl _))

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:
ext Z ⟨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
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
Z : Cᵒᵖ
f : (yoneda.obj X).obj Z
⊢ (hom
          ((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)))).app
            Z)).toFun
      { down := f } =
    (hom ((StructuredArrow.hom Y).app Z)).toFun { down := f }
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
  refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
  · refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
    simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _
  · refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)
    simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _

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
  refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
  · refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
    simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _
  · refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)
    simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.limitsOfShape J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
obtain ⟨J, _, ⟨p⟩⟩ := hP Y

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.limitsOfShape J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
J : Type w
w✝ : Category.{w', w} J
p : P.LimitOfShape J Y
⊢ f = g
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✝¹ : HasWideEqualizer f
inst✝ : Nonempty J
W : C
k : W ⟶ X
h : ∀ (j₁ j₂ : J), k ≫ f j₁ = k ≫ f j₂
⊢ lift k h ≫ ι f = k

Tactic:
by
  simp

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✝¹ : HasWideCoequalizer f
inst✝ : Nonempty J
W : C
k : Y ⟶ W
h : ∀ (j₁ j₂ : J), f j₁ ≫ k = f j₂ ≫ k
⊢ π f ≫ desc k h = k

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i ↦ StructuredArrow.mk (f i)
⊢ ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')

Tactic:
intro A'

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i ↦ StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ i, Nonempty (B' i ⟶ A')
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 : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op = (MonoOver.mk f).arrow.unop.left.op

Tactic:
refine Quiver.Hom.unop_inj ?_

Goal state after:
case refine_3
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 Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op).unop =
    (MonoOver.mk f).arrow.unop.left.op.unop
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
g : (i : J) → ↑(X.obj { as := i })
j : J
⊢ Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) g j =
    (ConcreteCategory.hom
        (limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
            { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
              π :=
                Discrete.natTrans fun j ↦
                  AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) } ≫
          limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)) ≫
            (productIsProduct' Y).lift (getLimitCone Y).cone ≫
              AddCommGrpCat.ofHom
                {
                  toFun := fun x j ↦
                    (ConcreteCategory.hom
                        ((getLimitCone (Discrete.functor fun j ↦ Y.obj { as := j })).cone.π.app { as := j }))
                      x,
                  map_zero' := ⋯, map_add' := ⋯ }))
      g j

Tactic:
change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
g : (i : J) → ↑(X.obj { as := i })
j : J
⊢ Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) g j =
    (ConcreteCategory.hom
        ((productIsProduct' Y).lift (getLimitCone Y).cone ≫
          limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) { as := j }))
      ((limit.lift Y ((Cone.postcompose f).obj (Pi.cone X))).hom'
        ((limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
              { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
                π :=
                  Discrete.natTrans fun j ↦
                    AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) }).hom'
          g))
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = ↑(r • x)
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)

Tactic:
← (r • x).2.choose_spec

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ (fun m ↦ ⟨↑m, ⋯⟩) ((fun m ↦ ⟨↑m, ⋯⟩) m) = m

Tactic:
by simp only

Goal state after: