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

Goal state before:
pp: case id.id.id
X : WalkingParallelPair
⊢ ((id X).comp (id X)).comp (id X) = (id X).comp ((id X).comp (id X))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Over X
⊢ Hom.left (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝

Tactic:
rfl

Goal state after:
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 (homMk Y.hom ⋯) = Y.hom

Tactic:
rfl

Goal state after:
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
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left (Hom.left κ ≫ Y✝.hom)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Under X
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Under X
⊢ Hom.right (homMk Y.hom ⋯) = Y.hom

Tactic:
rfl

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inl f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp [← pushout.condition]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
val✝ : Z ⟶ (mk (𝟙 X) (𝟙 X) ⋯).pt
eq : (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst) ≫ f = (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd) ≫ f
⊢ val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst = val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
val✝ : (mk (𝟙 Y) (𝟙 Y) ⋯).pt ⟶ Z
eq : f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝
⊢ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ (𝟭 WalkingParallelPair).obj zero = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj zero

Tactic:
rfl

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

Goal state before:
pp: case one
⊢ (𝟭 WalkingParallelPair).obj one = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one

Tactic:
rfl

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

Goal state before:
pp: case op
X : WalkingParallelPair
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op X) = (𝟭 WalkingParallelPairᵒᵖ).obj (op X)

Tactic:
| _ X
             => 

Goal state after:
case op
X : WalkingParallelPair
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op X) = (𝟭 WalkingParallelPairᵒᵖ).obj (op X)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.zero
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) = (𝟭 WalkingParallelPairᵒᵖ).obj (op zero)

Tactic:
rfl

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

Goal state before:
pp: case op.one
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) = (𝟭 WalkingParallelPairᵒᵖ).obj (op one)

Tactic:
rfl

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

Goal state before:
pp: case h₀
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
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ s.inl ≫ m✝ = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)

pp: case h₁
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
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ s.inr ≫ m✝ = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
· simp only [PushoutCocone.mk_inl, PushoutCocone.mk_inr] at hr hr' ⊢
          simp only [hr]
          symm
          exact hs.fac _ WalkingSpan.left

Goal state after:
case h₁
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
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ s.inr ≫ m✝ = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op.zero.zero.id
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero))))

Tactic:
rfl

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

Goal state before:
pp: case op.op.one.zero.left
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op left)

Tactic:
rfl

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

Goal state before:
pp: case op.op.one.zero.right
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op right)

Tactic:
rfl

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

Goal state before:
pp: case op.op.one.one.id
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one))))

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app zero) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj zero) =
    𝟙 (walkingParallelPairOp.obj zero)

Tactic:
rfl

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

Goal state before:
pp: case one
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app one) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj one) =
    𝟙 (walkingParallelPairOp.obj one)

Tactic:
rfl

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ (parallelPair (F.map left) (F.map right)).obj zero = F.obj zero

Tactic:
rfl

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ (parallelPair (F.map left) (F.map right)).obj one = F.obj one

Tactic:
rfl

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 : WalkingParallelPair ⥤ C
⊢ F.obj zero = (parallelPair (F.map left) (F.map right)).obj zero

Tactic:
rfl

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

Goal state before:
pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.obj one = (parallelPair (F.map left) (F.map right)).obj one

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
X : Type v
inst✝¹ : Semiring X
inst✝ : Module R X
⊢ ↑(of R X) = X

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
⊢ of R ↑M = M

Tactic:
rfl

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)
⊢ image.lift F'.ofCompIso ≫ F'.m = ((Image.monoFactorisation f).compMono g).m

Tactic:
← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m),

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)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ 𝟙 Z = ((Image.monoFactorisation f).compMono g).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
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝

Tactic:
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 : C
inst✝ : Mono 0
⊢ IsZero X

Tactic:
apply of_mono_zero X Y

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✝
X Y : C
f g : X ⟶ Y
X' Y' : C
c : Cofork f g
f' g' : X' ⟶ Y'
c' : Cofork f' g'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
e : c.pt ≅ c'.pt
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
comm₃ : e₁.inv ≫ c.π ≫ e.hom = c'.π
i : parallelPair f g ≅ parallelPair f' g' := parallelPair.ext e₀ e₁ ⋯ ⋯
⊢ π ((Cocone.precompose i.inv).obj c) ≫ e.hom = (e₁.inv ≫ c.π) ≫ e.hom

Tactic:
rfl

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 X

Tactic:
by
    have P := P.some
    rw [← P.hom_inv_id, ← Category.id_comp P.inv]
    apply Eq.symm
    simp only [id_comp, Iso.hom_inv_id, comp_zero]
    apply (idZeroEquivIsoZero X).invFun P

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteLimits C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
by cases nonempty_fintype J; exact HasFiniteLimits.out _

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X

Tactic:
rintro (hY | hY)

Goal state after:
case mpr.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X

case mpr.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
toIsLeftCancelMul✝¹ : IsLeftCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
mul_comm✝ : ∀ (a b : M), a * b = b * a
toIsLeftCancelMul✝ : IsLeftCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, mul_comm := mul_comm✝¹,
        toIsLeftCancelMul := toIsLeftCancelMul✝¹ }.toCommMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, mul_comm := mul_comm✝,
        toIsLeftCancelMul := toIsLeftCancelMul✝ }.toCommMonoid
⊢ { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
      npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, mul_comm := mul_comm✝¹,
      toIsLeftCancelMul := toIsLeftCancelMul✝¹ } =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
      npow_zero := npow_zero✝, npow_succ := npow_succ✝, mul_comm := mul_comm✝, toIsLeftCancelMul := toIsLeftCancelMul✝ }

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
toDivInvMonoid✝ : DivInvMonoid G
inv_mul_cancel✝¹ inv_mul_cancel✝ : ∀ (a : G), a⁻¹ * a = 1
⊢ { toDivInvMonoid := toDivInvMonoid✝, inv_mul_cancel := inv_mul_cancel✝¹ } =
    { toDivInvMonoid := toDivInvMonoid✝, inv_mul_cancel := inv_mul_cancel✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ { toGroup := toGroup✝, mul_comm := mul_comm✝¹ } = { toGroup := toGroup✝, mul_comm := mul_comm✝ }

Tactic:
rfl

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
inst✝² : HasCokernel f✝
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ parallelPair g 0 ≅ parallelPair g 0

Tactic:
rfl

Goal state after:
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
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono (map p)

Tactic:
rw [show biproduct.map p = (biproduct.isoProduct _).hom ≫ Pi.map p ≫
    (biproduct.isoProduct _).inv by aesop]
  infer_instance

Goal state after:
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
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
⊢ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π = s.π

Tactic:
apply biproduct.hom_ext'; intro j
      rw [CokernelCofork.π_ofπ, biproduct.toSubtype_fromSubtype_assoc, biproduct.ι_map_assoc]
      rcases Classical.em (i = j) with (rfl | h)
      · rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]
      · rw [if_pos (Ne.symm h), Category.id_comp]

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
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m - (f ≫ b.inl + g ≫ b.inr) = 0

Tactic:
← hq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ q ≫ b.inl = 0
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
X : Type v
inst✝¹ : Ring X
inst✝ : Module R X
⊢ ↑(of R X) = X

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ of R ↑M = M

Tactic:
rfl

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
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m - (f ≫ b.inl + g ≫ b.inr) = 0

Tactic:
← hq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ q ≫ b.inr = 0
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
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝

Tactic:
rfl

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

Goal state before:
pp: R✝ : Type u
inst✝¹ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
inst✝ : CommRing R
A : AlgCat R
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (RingHom.id R)).obj A))
      ((algebraMap R ↑((restrictScalars (RingHom.id R)).obj A)) x✝) =
    (algebraMap R ↑A) x✝

Tactic:
rfl

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

Goal state before:
pp: R✝ : Type u
inst✝³ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
A : AlgCat T
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (g.comp f)).obj A)) ((algebraMap R ↑((restrictScalars (g.comp f)).obj A)) x✝) =
    (algebraMap R ↑((restrictScalars f).obj ((restrictScalars g).obj A))) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
x✝² x✝¹ : R
x✝ : ↑(mkOfSMul' φ)
⊢ (ConcreteCategory.hom (φ x✝² + φ x✝¹)) x✝ = (ConcreteCategory.hom (φ x✝²)) x✝ + (ConcreteCategory.hom (φ x✝¹)) x✝

Tactic:
rfl

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
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m - (b.fst ≫ f + b.snd ≫ g) = 0

Tactic:
← hq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ b.fst ≫ q = 0
Module: Mathlib.Algebra.Group.TypeTags.Finite

Goal state before:
pp: α : Type u
inst✝ : Finite α
⊢ α ≃ Additive α

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Finite

Goal state before:
pp: α : Type u
inst✝ : Finite α
⊢ α ≃ Multiplicative α

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
⊢ r a (f 0) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f ↔ (∀ (i : Fin (n + 1)), r a (f i)) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
simp only [forall_iff_succ, and_congr_left_iff, iff_self_and]

Goal state after:
α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f → r a (f 0) → ∀ (i : Fin n), r a (f i.succ)
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
h : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
r0 : r a (f 0)
i : Fin n
⊢ (fun x1 x2 ↦ x1 < x2) 0 i.succ

Tactic:
grind

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
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m - (b.fst ≫ f + b.snd ≫ g) = 0

Tactic:
← hq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ b.snd ≫ q = 0
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ (fun i ↦ if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f

Tactic:
grind

Goal state after: