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

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

Tactic:
cases g

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

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

Tactic:
cases g

Goal state after:
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)

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)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

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

Tactic:
cases g

Goal state after:
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))))
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : CostructuredArrow G e
X✝ Y✝ : CostructuredArrow (pre F G e) f
φ : X✝ ⟶ Y✝
⊢ F.map φ.left.left ≫ (mk Y✝.hom.left).hom = (mk ((pre F G e).map φ.left ≫ Y✝.hom).left).hom

Tactic:
comp_left

Goal state after:
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 : C ⥤ D
G : D ⥤ E
e : E
f : CostructuredArrow G e
X✝ Y✝ : CostructuredArrow (pre F G e) f
φ : X✝ ⟶ Y✝
⊢ F.map φ.left.left ≫ (mk Y✝.hom.left).hom = (mk (((pre F G e).map φ.left).left ≫ Y✝.hom.left)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: case mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

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
X : C
hX : 𝟙 X = 0
⊢ 𝟙 (F.obj X) = 0

Tactic:
← F.map_id,

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
X : C
hX : 𝟙 X = 0
⊢ F.map (𝟙 X) = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
⊢ 0 ≫ 0 = 𝟙 (F.obj 0)

Tactic:
← F.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
⊢ 0 ≫ 0 = F.map (𝟙 0)
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ g = g'

Tactic:
rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • g = r • g'
⊢ g = g'
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
exact Or.inr ⟨Y, hY, ⟨e⟩⟩

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

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

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

Goal state after:
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✝ }
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this✝ : ZPow.zpow = ZPow.zpow
this : Div.div = Div.div
⊢ m₁ = m₂

Tactic:
rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩, ⟨_⟩⟩

Goal state after:
M : Type u_1
m₂ : DivInvMonoid M
toMonoid✝ : Monoid M
inv✝ : M → M
div✝ : M → M → M
div_eq_mul_inv✝ : ∀ (a b : M), a / b = a * b⁻¹
zpow✝ : ℤ → M → M
zpow_zero'✝ : ∀ (a : M), a ^ 0 = 1
zpow_succ'✝ : ∀ (n : ℕ) (a : M), a ^ ↑n.succ = a ^ ↑n * a
zpow_neg'✝ : ∀ (n : ℕ) (a : M), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon :
  { toMonoid := toMonoid✝, inv := inv✝, div := div✝, zpow := zpow✝, div_eq_mul_inv := div_eq_mul_inv✝,
        zpow_zero' := zpow_zero'✝, zpow_succ' := zpow_succ'✝, zpow_neg' := zpow_neg'✝ }.toMonoid =
    m₂.toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this✝ : ZPow.zpow = ZPow.zpow
this : Div.div = Div.div
⊢ { toMonoid := toMonoid✝, inv := inv✝, div := div✝, zpow := zpow✝, div_eq_mul_inv := div_eq_mul_inv✝,
      zpow_zero' := zpow_zero'✝, zpow_succ' := zpow_succ'✝, zpow_neg' := zpow_neg'✝ } =
    m₂
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
c : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ Cofork.π c ≫ 0 = Cofork.π s

Tactic:
by rw [comp_zero, ← cancel_epi f, comp_zero, s.condition]

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✝ : HasKernel f
F : MonoFactorisation f
⊢ kernel.ι f ≫ f = 0

Tactic:
kernel.condition

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
F : MonoFactorisation f
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom = g.hom
⊢ { hom := hom✝, wπ := wπ✝, wι := wι✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
hom✝¹ : c.pt ⟶ c'.pt
wπ✝¹ : ∀ (j : J), hom✝¹ ≫ c'.π j = c.π j
wι✝¹ : ∀ (j : J), c.ι j ≫ hom✝¹ = c'.ι j
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝¹, wπ := wπ✝¹, wι := wι✝¹ }.hom = { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom
⊢ { hom := hom✝¹, wπ := wπ✝¹, wι := wι✝¹ } = { hom := hom✝, wπ := wπ✝, wι := wι✝ }
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
inst✝ : HasZeroObject C
⊢ 𝟙 (F.obj 0) = 0

Tactic:
← F.map_id,

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
inst✝ : HasZeroObject C
⊢ F.map (𝟙 0) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
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 : f j
j' : ι
y : f j'
h : ¬⟨j, x⟩ = ⟨j', 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 [Sigma.mk.inj_iff, not_and] at h
            by_cases w : j = j'
            · cases w
              simp only [heq_eq_eq, forall_true_left] at h
              simp [biproduct.ι_π_ne _ h]
            · simp [biproduct.ι_π_ne_assoc _ w]

Goal state after:
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
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ F.map (∑ a, b✝.π a ≫ b✝.ι a) = 𝟙 (F.mapBicone b✝).pt

Tactic:
← F.map_id,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ F.map (∑ a, b✝.π a ≫ b✝.ι a) = F.map (𝟙 b✝.pt)
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : ↑i = j then eqToHom ⋯ else 0) =
    ι (Subtype.restrict p f) i ≫ if h : p j then π (Subtype.restrict p f) ⟨j, h⟩ else 0

pp: case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : ↑i = j then eqToHom ⋯ else 0) =
    ι (Subtype.restrict p f) i ≫ if h : p j then π (Subtype.restrict p f) ⟨j, h⟩ else 0

Tactic:
· rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Goal state after:
case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : ↑i = j then eqToHom ⋯ else 0) =
    ι (Subtype.restrict p f) i ≫ if h : p j then π (Subtype.restrict p f) ⟨j, h⟩ else 0
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w : { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom = g.hom
⊢ { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
hom✝¹ : c.pt ⟶ c'.pt
wfst✝¹ : hom✝¹ ≫ c'.fst = c.fst
wsnd✝¹ : hom✝¹ ≫ c'.snd = c.snd
winl✝¹ : c.inl ≫ hom✝¹ = c'.inl
winr✝¹ : c.inr ≫ hom✝¹ = c'.inr
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w :
  { hom := hom✝¹, wfst := wfst✝¹, wsnd := wsnd✝¹, winl := winl✝¹, winr := winr✝¹ }.hom =
    { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom
⊢ { hom := hom✝¹, wfst := wfst✝¹, wsnd := wsnd✝¹, winl := winl✝¹, winr := winr✝¹ } =
    { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom ⋯ else 0) =
    (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i

pp: case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : j = ↑i then eqToHom ⋯ else 0) =
    (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i

Tactic:
· rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Goal state after:
case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : j = ↑i then eqToHom ⋯ else 0) =
    (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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
P Q : C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ F.map (F.preimage t.hom ≫ Y✝.fst) = F.map X✝.fst

Tactic:
simpa using! t.wfst

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

Goal state before:
pp: case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g

Tactic:
cases g

Goal state after:
case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk._private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) = 0

Tactic:
apply biprod.hom_ext

Goal state after:
case mpr.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) ≫ biprod.fst = 0 ≫ biprod.fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) ≫ biprod.snd = 0 ≫ biprod.snd
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_3
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f.support.erase a ⊆ s

Tactic:
← subset_insert_iff

Goal state after:
case mp.refine_3
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f.support ⊆ insert a s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
this : (c.embedding (c.index j)) (c.invEmbedding j) ∈ Set.range ⇑(c.embedding (c.index j))
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Tactic:
c.embedding_comp_inv j

Goal state after:
n : ℕ
c : Composition n
j : Fin n
this : j ∈ Set.range ⇑(c.embedding (c.index j))
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ⁻¹.support = σ.support

Tactic:
simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]

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
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)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ ((insert a s).noncommProd f comm).support

Tactic:
rw [Finset.noncommProd_insert_of_notMem s a f comm ha]

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)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a * s.noncommProd f ⋯).support
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
⊢ Disjoint (sq \ sp) (sp ∪ sq)ᶜ

Tactic:
simp [Set.disjoint_left]

Goal state after:
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
⊢ ∀ ⦃a : α⦄, a ∈ sq → a ∉ sp → a ∈ sq
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
epc : ↑spᶜ ≃ ↑(sq \ sp) ⊕ ↑(sp ∪ sq)ᶜ := (setCongr hpc).trans (Set.union ⋯)
⊢ Disjoint (sp \ sq) (sp ∪ sq)ᶜ

Tactic:
simp [Set.disjoint_left]

Goal state after:
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
epc : ↑spᶜ ≃ ↑(sq \ sp) ⊕ ↑(sp ∪ sq)ᶜ := (setCongr hpc).trans (Set.union ⋯)
⊢ ∀ ⦃a : α⦄, a ∈ sp → a ∉ sq → a ∉ sp → a ∈ sq
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)

Tactic:
rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
    · exact hf x (Finset.mem_coe.2 hx)

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : x = y
⊢ x ∈ l

Tactic:
hxy

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : x = y
⊢ y ∈ l