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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := left } ≫ desc (inl t) (inr t) = t.ι.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }

Tactic:
· exact hd₁ _ _

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
⊢ ι (f ∘ ⇑ε) b ≫
      (HasColimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun x ↦ Iso.refl (f (ε x.as)))).hom =
    ι f (ε b)

Tactic:
simp only [HasColimit.ι_isoOfEquivalence_hom, Functor.id_obj, Discrete.functor_obj,
    Function.comp_apply, Discrete.equivalence_functor, Discrete.equivalence_inverse,
    Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]

Goal state after:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
⊢ (Discrete.functor (f ∘ ⇑ε)).map ((Discrete.equivalence ε).unit.app { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) } =
    ι f (ε b)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Over X
⊢ Hom.left (mkIdTerminal.from Y) = Y.hom

Tactic:
by
  rw [mkIdTerminal.hom_ext (mkIdTerminal.from Y) (homMk Y.hom)]
  rfl

Goal state after:
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
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ ∀ (X : StructuredArrow L R),
    (map₂ α β).map
          (((map₂IdIso L (𝟙 L) (R.rightUnitor.hom ≫ R.leftUnitor.inv) ⋯ ⋯).symm ≪≫
                  map₂Congr (𝟙 L) (R.rightUnitor.hom ≫ R.leftUnitor.inv) F.unitIso G.unitIso (α' ≫ G.inverse.map α)
                      ((R.associator G.functor G.inverse).inv ≫
                        Functor.whiskerRight β G.inverse ≫
                          (F.functor.associator R' G.inverse).hom ≫
                            F.functor.whiskerLeft β' ≫ (F.functor.associator F.inverse R).inv)
                      ?m.563 ?m.564 ≪≫
                    (map₂CompMap₂Iso α' β' α β).symm).hom.app
            X) ≫
        (map₂CompMap₂Iso α β α' β' ≪≫
                map₂Congr (α ≫ G.functor.map α')
                    ((R'.associator G.inverse G.functor).inv ≫
                      Functor.whiskerRight β' G.functor ≫
                        (F.inverse.associator R G.functor).hom ≫
                          F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv)
                    F.counitIso G.counitIso (𝟙 L') (R'.rightUnitor.hom ≫ R'.leftUnitor.inv) ?m.659 ?m.660 ≪≫
                  map₂IdIso L' (𝟙 L') (R'.rightUnitor.hom ≫ R'.leftUnitor.inv) ⋯ ⋯).hom.app
          ((map₂ α β).obj X) =
      𝟙 ((map₂ α β).obj X)

Tactic:
· simp [map₂Congr]

Goal state after:
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
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
hβ : β = e₂.hom.app T ≫ β'
X : CostructuredArrow S T
⊢ U.map (e₁.app X.left).hom ≫ ((map₂ α' β').obj X).hom = ((map₂ α β).obj X).hom

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

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

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
hβ : β = e₂.hom.app T ≫ β'
⊢ ∀ {X Y : CostructuredArrow S T} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.left) ⋯).hom = (isoMk (e₁.app X.left) ⋯).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
X : T
Z Y : (Over X)ᵒᵖ
f : Z ⟶ Y
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op

Tactic:
← Over.w f.unop,

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Over X)ᵒᵖ
f : Z ⟶ Y
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (Over.Hom.left f.unop ≫ (unop Z).hom).op
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ (Iso.refl (Arrow.mk h.i).left).hom ≫ (Arrow.mk (F.map (F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv)))).hom =
    (Arrow.mk h.i).hom ≫ (F.objObjPreimageIso h.Z).symm.hom

Tactic:
simp [F.map_preimage]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ (F.objObjPreimageIso h.Z).symm.hom ≫ (Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)))).hom =
    (Arrow.mk h.p).hom ≫ (Iso.refl (Arrow.mk h.p).right).hom

Tactic:
simp [F.map_preimage]

Goal state after:
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
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
⊢ ∀ (X : CostructuredArrow S T),
    (map₂ α β).map
          (((map₂IdIso (S.leftUnitor.hom ≫ S.rightUnitor.inv) T (𝟙 ((𝟭 D).obj T)) ⋯ ⋯).symm ≪≫
                  map₂Congr (S.leftUnitor.hom ≫ S.rightUnitor.inv) (𝟙 ((𝟭 D).obj T)) F.unitIso G.unitIso
                      ((F.functor.associator F.inverse S).hom ≫
                        F.functor.whiskerLeft α' ≫
                          (F.functor.associator U G.inverse).inv ≫
                            Functor.whiskerRight α G.inverse ≫ (S.associator G.functor G.inverse).hom)
                      (G.inverse.map β ≫ β') ?m.565 ?m.566 ≪≫
                    (map₂CompMap₂Iso α' β' α β).symm).hom.app
            X) ≫
        (map₂CompMap₂Iso α β α' β' ≪≫
                map₂Congr
                    ((F.inverse.associator F.functor U).hom ≫
                      F.inverse.whiskerLeft α ≫
                        (F.inverse.associator S G.functor).inv ≫
                          Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom)
                    (G.functor.map β' ≫ β) F.counitIso G.counitIso (U.leftUnitor.hom ≫ U.rightUnitor.inv)
                    (𝟙 ((𝟭 B).obj V)) ?m.661 ?m.662 ≪≫
                  map₂IdIso (U.leftUnitor.hom ≫ U.rightUnitor.inv) V (𝟙 ((𝟭 B).obj V)) ⋯ ⋯).hom.app
          ((map₂ α β).obj X) =
      𝟙 ((map₂ α β).obj X)

Tactic:
· simp [map₂Congr]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
⊢ f ≫ t.inl = g ≫ t.inr

Tactic:
rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.condition]

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

Goal state before:
pp: case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ e✝¹ ≫ Fm = e✝ ≫ Fm

Tactic:
rw [Ffac, hm, Ffac']

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
this : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = image.lift F'.ofCompIso ≫ F'.ofCompIso.m
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m

Tactic:
this,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
this : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = image.lift F'.ofCompIso ≫ F'.ofCompIso.m
⊢ image.lift F'.ofCompIso ≫ F'.ofCompIso.m = (Image.monoFactorisation f).m
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
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
rw [Algebra.smul_def, mul_smul]; rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ f = 0

Tactic:
rw [← zero_comp, cancel_mono] at h
  exact h

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) ⋯

Tactic:
by
  apply equalizer.hom_ext
  simp [← G.map_comp]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasProduct f
b : β
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ f b
e : x✝¹ ≫ Pi.ι f b = x✝ ≫ Pi.ι f b
⊢ x✝¹ = x✝

Tactic:
by simpa using congrArg (· ≫ Pi.π f b) e

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
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
⊢ IsZero c.pt

Tactic:
have := Fork.IsLimit.mono hc
  rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j) ≫ F.map (b.π j') = if h : j = j' then eqToHom ⋯ else 0

Tactic:
rw [← F.map_comp]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos.refl
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x y : f j
h : j = j → ¬x ≍ y
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j, y⟩.fst ≫ biproduct.π (g ⟨j, y⟩.fst) ⟨j, y⟩.snd =
    0

Tactic:
simp only [heq_eq_eq, forall_true_left] at h

Goal state after:
case pos.refl
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x y : f j
h : ¬x = y
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j, y⟩.fst ≫ biproduct.π (g ⟨j, y⟩.fst) ⟨j, y⟩.snd =
    0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.fst = BinaryCofan.IsColimit.desc ht (𝟙 X) 0

Tactic:
by
  apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)
  rintro ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
this,

Goal state after:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = inv inl ≫ inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).hom ≫ desc b.ι = 𝟙 b.pt

Tactic:
←
      biproduct.conePointUniqueUpToIso_inv f hb,

Goal state after:
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).hom ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv = 𝟙 b.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ desc b.ι ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).hom = 𝟙 (⨁ f)

Tactic:
←
      biproduct.conePointUniqueUpToIso_inv f hb,

Goal state after:
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).hom = 𝟙 (⨁ f)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero (A ⊞ B) → IsZero A ∧ IsZero B

pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)

Tactic:
· intro h
    simp only [IsZero.iff_id_eq_zero] at h ⊢
    simp only [show 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst by simp,
      show 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd by simp, h, zero_comp, comp_zero,
      and_self]

Goal state after:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)
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
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
rw [Algebra.smul_def, mul_smul]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: n k : ℕ
a✝ : Fin k → ℕ
⊢ a✝ ∈ univ.piAntidiag n ↔ a✝ ∈ Nat.antidiagonalTuple k n

Tactic:
simp [Nat.mem_antidiagonalTuple]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks[i]

Tactic:
simp only [sizeUpTo]

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take (i + 1) c.blocks).sum = (take i c.blocks).sum + c.blocks[i]
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ x = (f ^ (n + 1)) x ∨ (f ^ (n + 1))⁻¹ x = f x

Tactic:
← f.injective.eq_iff,

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ f x = f ((f ^ (n + 1)) x) ∨ (f ^ (n + 1))⁻¹ x = f x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), σ a = a) ↔ σ = 1

Tactic:
Equiv.Perm.ext_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), σ a = a) ↔ ∀ (x : α), σ x = 1 x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ replicate c.blocks.length 1 = (ones n).blocks

Tactic:
this,

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ replicate n 1 = (ones n).blocks
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ∈ c.support
ha' : a ∉ s
⊢ False

Tactic:
rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ≠ a
ha' : a ∉ s
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ (False ∨ ↑i + 1 = n ∨ ∃ j ∈ s, ↑i + 1 = ↑j + 1) ↔ i ∈ s

Tactic:
this,

Goal state after:
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ (False ∨ False ∨ ∃ j ∈ s, ↑i + 1 = ↑j + 1) ↔ i ∈ s