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

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
⊢ ∀ (f : Y ⟶ Z),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
⊢ ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
      ((evaluation C (Type v₁) ⋙
                (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
            X).map
        f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
⊢ ∀ (f : Y ⟶ Z),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
⊢ (coyoneda.rightOp ⋙ coyoneda).map f ≫
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation C (Type v₁) ⋙
            (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
        f
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.21 + 1} ⥤ C
X Y : Discrete PUnit.{?u.21 + 1}
⊢ ∀ (f : X ⟶ Y),
    (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).map f ≫
        match Y with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
      (match X with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
        F.map f

Tactic:
f

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.21 + 1} ⥤ C
X Y : Discrete PUnit.{?u.21 + 1}
f : X ⟶ Y
⊢ (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).map f ≫
      match Y with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
    (match X with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
      F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
X Y : C
⊢ ∀ (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫
        coyonedaEquiv.toIso.hom =
      coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
X Y : C
f : X ⟶ Y
⊢ ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫ coyonedaEquiv.toIso.hom =
    coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map
X✝ : Type u
X Y : Discrete X✝
⊢ ∀ (f : X ⟶ Y),
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map f =
      eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map f ≫ eqToHom ⋯

Tactic:
f

Goal state after:
case h_map
X✝ : Type u
X Y : Discrete X✝
f : X ⟶ Y
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map f =
    eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map y.down)) x, naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) { down := 𝟙 (unop X) }) τ) =
    τ

Tactic:
ext Y ⟨x⟩
    simp [← comp_apply, ← τ.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
x y : ↑(typeToCat.obj X✝)
⊢ ∀ (f : x ⟶ y),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
      eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯

Tactic:
f

Goal state after:
X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
x y : ↑(typeToCat.obj X✝)
f : x ⟶ y
⊢ (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
⊢ ∀ (f : A ⟶ B) [IsIso ((functoriality K F).map f)], IsIso f

Tactic:
f

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
f : A ⟶ B
⊢ ∀ [IsIso ((functoriality K F).map f)], IsIso f
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
⊢ ∀ (f : i ⟶ j), ((Functor.const J).obj (F.obj X)).map f ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f

Tactic:
f

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ ((Functor.const J).obj (F.obj X)).map f ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
⊢ ∀ (f : i ⟶ j), F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ ((Functor.const J).obj (F.obj X)).map f

Tactic:
f

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ ((Functor.const J).obj (F.obj X)).map f
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
⊢ post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ post G H

Tactic:
ext
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
  rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none

Tactic:
have h₂ := t.π.naturality WalkingCospan.Hom.inl

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app one = t.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
X : StructuredArrow L R
⊢ ((map₂ α β).obj X).hom ≫ R'.map (e₁.app X.right).hom = ((map₂ α' β').obj X).hom

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
⊢ ∀ {X Y : StructuredArrow L R} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.right) ⋯).hom = (isoMk (e₁.app X.right) ⋯).hom ≫ (map₂ α' β').map f

Tactic:
· subst hα
    simp [dsimp% congr($(hβ).app X.right)]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
⊢ ∀ {X Y : StructuredArrow L R} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.right) ⋯).hom = (isoMk (e₁.app X.right) ⋯).hom ≫ (map₂ α' β').map f
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow (toOver F X) Y
f : X✝ ⟶ Y✝
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y✝.hom)).hom = (mk (Over.Hom.left X✝.hom)).hom

Tactic:
← CostructuredArrow.w f

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow (toOver F X) Y
f : X✝ ⟶ Y✝
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y✝.hom)).hom = (mk (Over.Hom.left ((toOver F X).map f.left ≫ Y✝.hom))).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
s : PullbackCone f g
⊢ s.fst ≫ (pullbackConeOfRightIso f g).fst = s.fst ∧
    s.fst ≫ (pullbackConeOfRightIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfRightIso f g).pt},
        m ≫ (pullbackConeOfRightIso f g).fst = s.fst → m ≫ (pullbackConeOfRightIso f g).snd = s.snd → m = s.fst

Tactic:
simp [s.condition_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
s : S
s₀ : S₀
n : ↑M
⊢ s • (algebraMap S₀ S) s₀ • n = (algebraMap S₀ S) s₀ • s • n

Tactic:
← smul_assoc,

Goal state after:
R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (s • (algebraMap S₀ S) s₀) • n = (algebraMap S₀ S) s₀ • s • n
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝ : Category.{v, u} C
f✝ g✝ : X✝ ⟶ Y✝
X Y : C
f g : X ⟶ Y
t : Cofork f g
ht : IsColimit t
Z : C
k : t.pt ⟶ Z
⊢ f ≫ t.π ≫ k = g ≫ t.π ≫ k

Tactic:
simp only [← Category.assoc, t.condition]

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

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app zero ≫ k = t.ι.app zero

pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one

Tactic:
· simp [Cofork.app_zero_eq_comp_π_left, w]

Goal state after:
case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
⊢ f ≫ s.π = g ≫ s.π

Tactic:
apply hm.left_cancellation

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
⊢ h ≫ f ≫ s.π = h ≫ g ≫ s.π
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toCommMonoid M)

Tactic:
rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h
  grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)
⊢ ∀ {K : Discrete WalkingPair ⥤ C}, PreservesColimit K G

Tactic:
by
    intro K
    have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesColimitPair.of_iso_coprod_comparison ..
    apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
cc : CokernelCofork f
hf : IsColimit cc
cc' : CokernelCofork f'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ f ≫ Arrow.Hom.right φ ≫ Cofork.π cc' = 0

Tactic:
erw [← Arrow.w_assoc φ, condition, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : (factorThruImage f ≫ image.ι f) ≫ cokernel.π f = 0
⊢ image.ι f ≫ cokernel.π f = 0

Tactic:
rw [← HasZeroMorphisms.comp_zero (Limits.factorThruImage f), Category.assoc,
          cancel_epi] at w

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : image.ι f ≫ cokernel.π f = 0
⊢ image.ι f ≫ cokernel.π f = 0
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
X Y : C
⊢ ∀ {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g

Tactic:
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✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
X Y : C
f : X ⟶ Y
⊢ ∀ {g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : rightExactFunctor C D F
⊢ additiveFunctor C D F

Tactic:
simp only [rightExactFunctor_iff] at h
    exact Functor.additive_of_preservesBinaryBiproducts F

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (splitEpiOfIdempotentOfIsColimitCofork C ⋯
          (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))).section_ ≫
      retraction f =
    0

Tactic:
splitEpiOfIdempotentOfIsColimitCofork_section_,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)).desc
        (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) ≫
      retraction f =
    0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
k : K
⊢ components (matrix m) j k = m j k

Tactic:
simp [biproduct.components]

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

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (matrix fun j k ↦ components m j k) ≫ π g j✝¹ = ι f j✝ ≫ m ≫ π g j✝¹

Tactic:
simp [biproduct.components]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
s : S
s₀ : S₀
n : ↑M
⊢ s • (algebraMap S₀ S) s₀ • n = (algebraMap S₀ S) s₀ • s • n

Tactic:
← smul_assoc,

Goal state after:
R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (s • (algebraMap S₀ S) s₀) • n = (algebraMap S₀ S) s₀ • s • n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ n

Tactic:
by
  rw [← c.blocks_sum]
  exact List.le_sum_of_mem h

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
⊢ (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
    ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
      (∀ a_2 ∈ insert a s, x ∉ (f a_2).support) → x ∉ ((insert a s).noncommProd f comm).support

Tactic:
ih

Goal state after:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
⊢ ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
    (∀ a_1 ∈ insert a s, x ∉ (f a_1).support) → x ∉ ((insert a s).noncommProd f comm).support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
rcases (c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderIsoOfFin ⋯) i = ⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)

Tactic:
exact Fintype.card_congr (compositionEquiv n)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case h
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := ⋯
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := ⋯
σ₁ : Perm m := ⋯
σ₂ : Perm n := ⋯
⊢ (sumCongrHom m n) (σ₁, σ₂) = σ

Tactic:
rw [Perm.sumCongrHom_apply]

Goal state after:
case h
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
⊢ (σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
⊢ ∀ {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ (n + 1)) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
f

Goal state after:
case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
⊢ (swap x (f x) * f) b ≠ b → (f ^ (n + 1)) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -(swap (e x) (e (f x)) * (e.symm.trans f).trans e).signAux

Tactic:
signAux_mul,

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -((swap (e x) (e (f x))).signAux * signAux ((e.symm.trans f).trans e))
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : ℕ
s : ι → ℕ
⊢ x.Coprime (∏ i, s i) ↔ ∀ (i : ι), x.Coprime (s i)

Tactic:
by
  simp [coprime_prod_right_iff]

Goal state after: