mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ HasPullback (f ≫ i) i

Tactic:
by
  simpa only [Category.id_comp] using hasPullback_of_comp_mono f (𝟙 Z) i

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

Goal state before:
pp: case e'_3.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }).hom ≫
      { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }.cone.π.app
        WalkingCospan.left =
    limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

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

Goal state before:
pp: case e'_5.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }).hom ≫
      { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }.cone.π.app
        WalkingCospan.left =
    limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left
e_3✝ : pullback (f ≫ i) i = limit (cospan (f ≫ i) (𝟙 Z ≫ i))
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

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

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

Tactic:
rw [Algebra.smul_def, mul_smul]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimit K F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimit K F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfShape J F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfShape J F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

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

Goal state before:
pp: case e'_2
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
h✝ : f = g
s : Cofork f g
m : (idCofork h✝).pt ⟶ s.pt
h : (idCofork h✝).π ≫ m = s.π
e_1✝ : ((idCofork h✝).pt ⟶ s.pt) = (Y ⟶ s.pt)
⊢ m = (idCofork h✝).π ≫ m

Tactic:
exact (Category.id_comp _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimit K F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimit K F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfShape J F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfShape J F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')

pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')

Tactic:
· obtain - | j' := j'
      · exact {Hom.id none}
      · exact {Hom.init j'}

Goal state after:
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure ≤ ⨆ a, (P a).isoClosure

Tactic:
rintro X ⟨Y, hY, ⟨e⟩⟩
    simp only [prop_iSup_iff] at hY ⊢
    obtain ⟨a, hY⟩ := hY
    exact ⟨a, _, hY, ⟨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✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 ≫ Fork.ι c = Fork.ι s

Tactic:
rw [zero_comp, ← cancel_mono f, zero_comp, s.condition]

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

Goal state before:
pp: case refine_4
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsColimit (c.whisker g).toCocone

Tactic:
apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm

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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsColimit
    ((Cocone.precompose (Discrete.functorComp f ⇑g).hom).obj
      (Cocone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCocone))
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (f ≫ q) = G.map p ≫ G.map g
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f) ≫ G.map f = 0

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f ≫ f) = 0
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι g) ≫ G.map g = 0

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι g ≫ g) = 0
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (f ≫ q) = G.map p ≫ G.map g
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map (coequalizer.π f 0) = 0

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (f ≫ coequalizer.π f 0) = 0
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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map g ≫ G.map (coequalizer.π g 0) = 0

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (g ≫ coequalizer.π g 0) = 0
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
m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π
⊢ m = 𝟙 (⨁ Subtype.restrict (fun j ↦ j ≠ i) f) ≫ m

Tactic:
exact (Category.id_comp _).symm

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
T U : C
f : T ⟶ X
g : T ⟶ Y
h : X ⟶ U
i : Y ⟶ U
⊢ lift f g ≫ desc h i = f ≫ h + g ≫ i

Tactic:
by simp [biprod.lift_eq, biprod.desc_eq]

Goal state after:
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 X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ biprod.fst ≫ biprod.inl = 𝟙 (X ⊞ Y)

Tactic:
by
    apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]
    apply hY.eq_of_tgt

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

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

Tactic:
rw [Algebra.smul_def, mul_smul]

Goal state after:
R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝
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
f : R →+* R
hf : f = RingHom.id R
A : AlgCat R
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars f).obj A)) ((algebraMap R ↑((restrictScalars f).obj A)) x✝) = (algebraMap R ↑A) x✝

Tactic:
subst hf; rfl

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

Goal state before:
pp: case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
⊢ f ∈ map { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n) ↔
    f ∈ map { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n)

Tactic:
simp only [mem_map, mem_finAntidiagonal]

Goal state after:
case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
⊢ (∃ a, ∑ i, a i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } a = f) ↔
    ∃ a, ∑ i, a i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ } a = f
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 + 1 = a.1 + 1 ∧ x₂ = x₁
⊢ False

Tactic:
Nat.succ_inj

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
⊢ ∅.finsuppAntidiag 0 = {0}

Tactic:
by
  ext f; simp

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

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f⁻¹ x = x ∨ g x = x

Tactic:
inv_eq_iff_eq,

Goal state after:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ x = f x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
inv_eq_iff_eq,

Goal state after:
α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ x = (f ^ (n + 1)) x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → i = c.index j

Tactic:
rw [← not_imp_not]

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ ¬i = c.index j → j ∉ Set.range ⇑(c.embedding i)
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
inv_eq_iff_eq,

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

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

Tactic:
inv_eq_iff_eq,

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = f x ∨ x = (f ^ (n + 1)) (f x)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
⊢ PreservesBiproduct f F

Tactic:
have : Epi (splitEpiBiproductComparison F f).section_ := by simpa

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this : Epi (F.splitEpiBiproductComparison f).section_
⊢ PreservesBiproduct f F
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: α : Type u_1
l : List α
ns : List ℕ
i : ℕ
hi : i < (l.splitWrtCompositionAux ns).length
⊢ (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)

Tactic:
induction ns generalizing l i with
  | nil => cases hi
  | cons n ns IH =>
    rcases i with - | i
    · simp
    · simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take,
          sum_cons, splitAt_eq, drop_take, drop_drop]
      rw [Nat.add_sub_add_left]

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

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

Tactic:
Perm.sumCongrHom_apply

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) =
    if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
by_cases h : f.symm b < f.symm a
    · simp_all [signBijAux, (mem_finPairsLT.1 hab).not_ge]
    · simp_all [signBijAux, dif_neg h, (mem_finPairsLT.1 hab).le]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ k) x = (f ^ k) x

Tactic:
refine ⟨?_, by rfl⟩

Goal state after:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f