mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : C ⥤ D
d : D
X Y : CostructuredArrow F d
f : op X ⟶ op Y
⊢ (𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫ (CostructuredArrow.isoMk (Iso.refl (unop (op Y)).left) ⋯).op.hom =
    (CostructuredArrow.isoMk (Iso.refl (unop (op X)).left) ⋯).op.hom ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f

Tactic:
obtain ⟨X, x, rfl⟩ := X.mk_surjective

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
Y : CostructuredArrow F d
X : C
x : F.obj X ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op Y
⊢ (𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫ (CostructuredArrow.isoMk (Iso.refl (unop (op Y)).left) ⋯).op.hom =
    (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ f = image.ι f

Tactic:
simp only [← imageMonoIsoSource_inv_ι f]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi f
⊢ Epi (image.ι f)

Tactic:
rw [← image.fac f] at E

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)
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:
with_reducible 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:
with_reducible rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.ι f.hom = image.ι f.hom ≫ 𝟙 f.right

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.ι f.hom = image.ι f.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
i : IsZero X
⊢ IsZero Y

Tactic:
obtain rfl := i.eq_zero_of_src f
  exact IsZero.of_epi_zero X Y

Goal state after:
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 : IsZero X
⊢ IsZero (F.obj X)

Tactic:
simp only [IsZero.iff_id_eq_zero] at hX ⊢

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.obj X) = 0
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 : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm✝ : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m✝ : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m✝ ≫ (Fork.ofι c.ι ⋯).ι = s.ι
⊢ m✝ = ↑l

Tactic:
apply Fork.IsLimit.hom_ext i

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm✝ : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := ⋯
l : { l // l ≫ c.ι = s'.ι } := ⋯
m✝ : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m✝ ≫ (Fork.ofι c.ι ⋯).ι = s.ι
⊢ m✝ ≫ c.ι = ↑l ≫ c.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasProduct f
b c : β
h : b ≠ c
⊢ ι f b ≫ π f c = 0

Tactic:
by
  simp [Pi.ι, Function.update_of_ne h.symm]

Goal state after:
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
    simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ : s.pt ⟶ (forkOfKernelFork c).pt
h : m✝ ≫ (forkOfKernelFork c).ι = s.ι
⊢ m✝ = i.lift (kernelForkOfFork s)

Tactic:
apply Fork.IsLimit.hom_ext i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ : s.pt ⟶ (forkOfKernelFork c).pt
h : m✝ ≫ (forkOfKernelFork c).ι = s.ι
⊢ m✝ ≫ Fork.ι c = i.lift (kernelForkOfFork s) ≫ Fork.ι c
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ : s.pt ⟶ (kernelForkOfFork c).pt
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = s.ι
⊢ m✝ = i.lift (forkOfKernelFork s)

Tactic:
apply Fork.IsLimit.hom_ext i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ : s.pt ⟶ (kernelForkOfFork c).pt
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = s.ι
⊢ m✝ ≫ c.ι = i.lift (forkOfKernelFork s) ≫ c.ι
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)
    · exact monotone_isoClosure le_sup_left _ hY
    · exact monotone_isoClosure le_sup_right _ hY

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ⊤.map P.ι = P.isoClosure

Tactic:
ext X
  constructor
  · rintro ⟨⟨Y, hY⟩, _, ⟨e⟩⟩
    exact ⟨Y, hY, ⟨e.symm⟩⟩
  · rintro ⟨Y, hY, ⟨e⟩⟩
    exact ⟨⟨Y, hY⟩, by simp, ⟨e.symm⟩⟩

Goal state after:
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
⊢ Div.div = Div.div

Tactic:
ext a b

Goal state after:
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
a b : M
⊢ Div.div a b = Div.div a b
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app zero = s.π.app zero

pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
· exact fac s

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app one = s.π.app one
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
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m✝ = ↑l

Tactic:
apply Fork.IsLimit.hom_ext i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m✝ ≫ Fork.ι c = ↑l ≫ Fork.ι c
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
W : C
g : Y ⟶ W
h✝ : X ⟶ W
c : KernelFork h✝
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h✝
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m = i.lift (KernelFork.ofι s.ι ⋯)

Tactic:
apply Fork.IsLimit.hom_ext i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h✝ : X ⟶ W
c : KernelFork h✝
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h✝
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m ≫ Fork.ι c = i.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι c
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
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) ≫ 𝟙 (F.obj (X ⊞ Y)) = F.map (lift f g)

Tactic:
Category.comp_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 Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) = F.map (lift f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app one ≫ desc s = s.ι.app one

Tactic:
· exact fac s

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

Goal state before:
pp: case pos
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
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
h : i = j
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }

Tactic:
simp_all [Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

Goal state after:
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
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
h : ¬i = j
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }

Tactic:
simp_all [Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

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

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ e j ≠ k

Tactic:
· exact Ne.symm h

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

Goal state before:
pp: 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)
j j✝ : Subtype p
⊢ ι f ↑j✝ ≫ π f ↑j = ι (Subtype.restrict p f) j✝ ≫ π (Subtype.restrict p f) j

Tactic:
biproduct.ι_π,

Goal state after:
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)
j j✝ : Subtype p
⊢ (if h : ↑j✝ = ↑j then eqToHom ⋯ else 0) = ι (Subtype.restrict p f) j✝ ≫ π (Subtype.restrict p f) j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: 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)
j j✝ : Subtype p
⊢ ι f ↑j ≫ π f ↑j✝ = ι (Subtype.restrict p f) j ≫ π (Subtype.restrict p f) j✝

Tactic:
biproduct.ι_π,

Goal state after:
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)
j j✝ : Subtype p
⊢ (if h : ↑j = ↑j✝ then eqToHom ⋯ else 0) = ι (Subtype.restrict p f) j ≫ π (Subtype.restrict p f) j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case inr
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 : Fork (π f i) 0
j : J
h : ¬i = j
⊢ s.ι ≫ π f j ≫ 𝟙 (f j) = s.ι ≫ π f j

Tactic:
Category.comp_id

Goal state after:
case inr
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 : Fork (π f i) 0
j : J
h : ¬i = j
⊢ s.ι ≫ π f j = s.ι ≫ π f j
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
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
Category.comp_id

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) = fst ≫ inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ ι f j ≫ π f j'.as = b.ι j ≫ b.toCone.π.app j'

Tactic:
biproduct.ι_π,

Goal state after:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ (if h : j = j'.as then eqToHom ⋯ else 0) = b.ι j ≫ b.toCone.π.app j'
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:
with_reducible 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:
with_reducible rfl

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

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
a b : Fin (n + 1)
hab : a < b
⊢ q.insertNth x f a < q.insertNth x f b

Tactic:
cases a using succAboveCases q

Goal state after:
case refine_4.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
hab : q < b
⊢ q.insertNth x f q < q.insertNth x f b

case refine_4.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
j✝ : Fin n
hab : q.succAbove j✝ < b
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f b
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
i : μ × μ
a✝¹ : i ∈ ↑(antidiagonal n)
j : μ × μ
a✝ : j ∈ ↑(antidiagonal n)
hij : i ≠ j
⊢ (Disjoint on fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) i j

Tactic:
simp only [Finset.disjoint_left, Finset.mem_map, Embedding.coeFn_mk]

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
i : μ × μ
a✝¹ : i ∈ ↑(antidiagonal n)
j : μ × μ
a✝ : j ∈ ↑(antidiagonal n)
hij : i ≠ j
⊢ ∀ ⦃a : Fin (d + 1) → μ⦄, (∃ a_1 ∈ ↑(aux d i.2), Fin.cons i.1 a_1 = a) → ¬∃ a_2 ∈ ↑(aux d j.2), Fin.cons j.1 a_2 = a
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ ∀ x ∈ antidiagonal n, (map (fun x_1 ↦ Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup

Tactic:
intro i _

Goal state after:
case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
a✝ : i ∈ antidiagonal n
⊢ (map (fun x ↦ Fin.cons i.1 x) (antidiagonalTuple k i.2)).Nodup
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
⊢ (Finsupp.erase a f).support ⊆ s

Tactic:
support_erase,

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.erase a ⊆ s
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange ⟨b, h⟩))

Tactic:
simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
  rw [Equiv.Perm.extendDomain_apply_subtype _ _ h]
  congr

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
⊢ ∃ σ, ∀ (a : α), σ (f a) = g a

Tactic:
have : Finite {x | x ∈ Set.range f} := .of_surjective _ (Set.codRestrict_range_surjective f)
  refine ⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩
  simp [Equiv.extendSubtype_apply_of_mem]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
h : (swap x x).support = {x, x}
⊢ False

Tactic:
simp [Finset.ext_iff] at h

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
x✝ : α
⊢ x✝ = x ∨ x✝ = y ∨ x✝ = z → x✝ ∈ (swap x y * swap y z).support

Tactic:
rintro (rfl | rfl | rfl | _)

Goal state after:
case a.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
y z x✝ : α
h : (x✝ ≠ y ∧ x✝ ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ x✝ ∈ (swap x✝ y * swap y z).support

case a.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x z x✝ : α
h : (x ≠ x✝ ∧ x ≠ z ∧ True) ∧ x✝ ≠ z ∧ True
⊢ x✝ ∈ (swap x x✝ * swap x✝ z).support

case a.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ z ∈ (swap x y * swap y z).support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 0 ↔ f = 1

Tactic:
Finset.card_eq_zero,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.support = ∅ ↔ f = 1