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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s ≅ t

Tactic:
by
  apply Cone.ext i _
  rintro (⟨⟩ | ⟨⟨⟩⟩)
  · have h₁ := s.π.naturality WalkingCospan.Hom.inl
    dsimp at h₁
    simp only [Category.id_comp] at h₁
    have h₂ := t.π.naturality WalkingCospan.Hom.inl
    dsimp at h₂
    simp only [Category.id_comp] at h₂
    simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]
  · exact w₁
  · exact w₂

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m ≫ s.π.app { as := WalkingPair.right } = (BinaryFan.assocInv P t).π.app { as := WalkingPair.right }

Tactic:
replace w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app ⟨.right⟩ := by
        simpa using! w ⟨.right⟩
      simp [← w]

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

Goal state before:
pp: case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Under Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1

Tactic:
simp [Under.map, Comma.mapLeft]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
⊢ Mono t.fst

Tactic:
refine ⟨fun {W} h k i => IsLimit.hom_ext ht i ?_⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.snd = k ≫ t.snd
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ → W₁.HasFactorization W₂

Tactic:
intro h
    refine ⟨fun f => ?_⟩
    have : W₁.comp W₂ f := by simp only [h, top_apply]
    exact ⟨this.some⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ Arrow.leftToRight.app f = f.hom

Tactic:
Arrow.leftToRight_app

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ f.hom = f.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst✝ : Epi f
s : PushoutCocone f f
⊢ 𝟙 Y ≫ s.inl = s.inr

Tactic:
← cancel_epi f,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst✝ : Epi f
s : PushoutCocone f f
⊢ f ≫ 𝟙 Y ≫ s.inl = f ≫ s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)

Tactic:
let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
  have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
  let e : F ≅ G := hF.iso hG
  exact (isZero_zero _).of_iso (e.app X)

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 f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f'

Tactic:
simp only [image.fac]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
cases f; cases g; simpa using! h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
X Y : SemimoduleCat R
i : X ≅ Y
⊢ Hom.hom i.hom ∘ₗ Hom.hom i.inv = LinearMap.id

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
X Y : SemimoduleCat R
i : X ≅ Y
⊢ Hom.hom i.inv ∘ₗ Hom.hom i.hom = LinearMap.id

Tactic:
by aesop

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
t : Fork f g
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s
s : Cone (parallelPair f g)
m : s.pt ⟶ t.pt
j : ∀ (j : WalkingParallelPair), m ≫ t.π.app j = s.π.app j
⊢ m = lift s

Tactic:
by aesop

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
t : Cofork f g
desc : (s : Cofork f g) → t.pt ⟶ s.pt
fac : ∀ (s : Cofork f g), t.π ≫ desc s = s.π
uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt), t.π ≫ m = s.π → m = desc s
⊢ ∀ (s : Cocone (parallelPair f g)) (m : t.pt ⟶ s.pt),
    (∀ (j : WalkingParallelPair), t.ι.app j ≫ m = s.ι.app j) → m = desc s

Tactic:
by aesop

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
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor c)

Tactic:
apply isColimitOfReflects F

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ f ≫ g = 0 ↔ g = 0

Tactic:
rw [← IsIso.eq_inv_comp, Limits.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
j j' : WalkingParallelPair
⊢ ∀ (x : WalkingParallelPairHom j j'),
    x ∈
      WalkingParallelPair.recOn j
        (WalkingParallelPair.recOn j' [WalkingParallelPairHom.id zero].toFinset [left, right].toFinset)
        (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)

Tactic:
by aesop

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

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

Tactic:
by_cases h : some j' = j
      · rw [h]
        exact {Hom.id j}
      · exact ∅

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
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
⊢ ι ≫ f = ι ≫ 0

Tactic:
by rw [w, HasZeroMorphisms.comp_zero]

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
s : Fork f 0
⊢ ∀ (j : WalkingParallelPair), s.π.app j = (Iso.refl s.pt).hom ≫ (Fork.ofι s.ι ⋯).π.app j

Tactic:
by aesop

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✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ e ≫ g = 0

Tactic:
simp [← h, he]

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 Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
⊢ m = ↑(h k hk)

Tactic:
rw [← cancel_epi p, (h k hk).2, hm]

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 : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ 0 = Cofork.π s

Tactic:
← cancel_epi f,

Goal state after:
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
⊢ f ≫ 0 = f ≫ Cofork.π s
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 : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ Cofork.π c ≫ 𝟙 c.pt = Cofork.π c ≫ 0

Tactic:
← cancel_epi f,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ f ≫ Cofork.π c ≫ 𝟙 c.pt = f ≫ Cofork.π c ≫ 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
inst✝² : HasCokernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
e : Y ⟶ Z
he : f ≫ e = 0
⊢ g ≫ e = 0

Tactic:
simp [← h, he]

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✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Epi f
inst✝ : HasCokernel g
⊢ g ≫ cokernel.π (f ≫ g) = 0

Tactic:
← cancel_epi f,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Epi f
inst✝ : HasCokernel g
⊢ f ≫ g ≫ cokernel.π (f ≫ g) = 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
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
j : WalkingParallelPair
⊢ s.ι.app j ≫ i.hom = (CokernelCofork.ofπ l ⋯).ι.app j

Tactic:
by
      cases j
      · dsimp; rw [← h]; simp
      · exact h

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
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map (kernel.lift f h w) ≫ kernelComparison f G = kernel.lift (G.map f) (G.map h) ⋯

Tactic:
ext; simp [← G.map_comp]

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
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ cokernelComparison f G ≫ G.map (cokernel.desc f h w) = cokernel.desc (G.map f) (G.map h) ⋯

Tactic:
ext; simp [← G.map_comp]

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 : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : BinaryBicone P Q
f : X✝ ⟶ Y✝
⊢ F.map f.hom ≫
      { pt := F.obj Y✝.pt, fst := F.map Y✝.fst, snd := F.map Y✝.snd, inl := F.map Y✝.inl, inr := F.map Y✝.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.snd =
    { pt := F.obj X✝.pt, fst := F.map X✝.fst, snd := F.map X✝.snd, inl := F.map X✝.inl, inr := F.map X✝.inr,
        inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.snd

Tactic:
simp [-BinaryBiconeMorphism.wsnd, ← f.wsnd]

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 : 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 (X✝.inl ≫ F.preimage t.hom) = F.map Y✝.inl

Tactic:
by simpa using! t.winl

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 : Fork (π f i) 0
⊢ ∀ {m : s.pt ⟶ (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯).pt},
    m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι → m = s.ι ≫ toSubtype f fun j ↦ j ≠ i

Tactic:
by
      intro m hm
      rw [← hm, KernelFork.ι_ofι, Category.assoc, biproduct.fromSubtype_toSubtype]
      exact (Category.comp_id _).symm

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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ ∀ {W' : C} (g' : W' ⟶ ⨁ f),
    g' ≫ biproduct.toSubtype f p = 0 → (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'

Tactic:
intro W' g' w

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
⊢ (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'
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
Z : C
f : Z ⟶ X ⊞ Y
⊢ f = (f ≫ fst) ≫ inl + (f ≫ snd) ≫ inr

Tactic:
by aesop

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
Z : C
f : X ⊞ Y ⟶ Z
⊢ f = fst ≫ inl ≫ f + snd ≫ inr ≫ f

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
cases f; cases g; simpa using! h

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
⊢ Hom.hom i.hom ∘ₗ Hom.hom i.inv = LinearMap.id

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
⊢ Hom.hom i.inv ∘ₗ Hom.hom i.hom = LinearMap.id

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : Type u
x✝ : AlgCat R
f : (free R).obj x✝¹ ⟶ x✝
⊢ (fun f ↦ ofHom ((FreeAlgebra.lift R) ⇑(ConcreteCategory.hom f)))
      ((fun f ↦ ↾(FreeAlgebra.lift R).symm (Hom.hom f)) f) =
    f

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : Type u
x✝ : AlgCat R
f : x✝¹ ⟶ (forget (AlgCat R)).obj x✝
⊢ (fun f ↦ ↾(FreeAlgebra.lift R).symm (Hom.hom f))
      ((fun f ↦ ofHom ((FreeAlgebra.lift R) ⇑(ConcreteCategory.hom f))) f) =
    f

Tactic:
by aesop

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

Goal state before:
pp: μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (x₁, x₂) ∈ (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) ↔ (x₁, x₂) ∈ antidiagonal n

Tactic:
simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk,
    ← Equiv.eq_symm_apply]

Goal state after:
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (∃ a ∈ univ.piAntidiag n, a = (Equiv.boolArrowEquivProd μ).symm (x₁, x₂)) ↔ (x₁, x₂) ∈ antidiagonal n
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ (addRightEmbedding fun t ↦ if t = i then f i else 0) (update f i 0) = f

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case e_a
n : ℕ
⊢ ∀ x ∈ range n, map (fun x_1 ↦ Fin.cons x x_1) (antidiagonalTuple 0 (n - x)) = []

Tactic:
List.mem_range,

Goal state after:
case e_a
n : ℕ
⊢ ∀ x < n, map (fun x_1 ↦ Fin.cons x x_1) (antidiagonalTuple 0 (n - x)) = []
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
⊢ j < c.sizeUpTo (c.length.pred + 1)

Tactic:
have : c.length - 1 + 1 = c.length := Nat.succ_pred_eq_of_pos length_pos

Goal state after:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
this : c.length - 1 + 1 = c.length
⊢ j < c.sizeUpTo (c.length.pred + 1)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.sizeUpTo ↑(c.index j) + c.blocksFun (c.index j)

pp: n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j

Tactic:
← sizeUpTo_succ'

Goal state after:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.sizeUpTo (↑(c.index j) + 1)

n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j < c.sizeUpTo ↑i + c.blocksFun i

pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ c.sizeUpTo ↑i ≤ ↑j

Tactic:
← sizeUpTo_succ'

Goal state after:
case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j < c.sizeUpTo (↑i + 1)

case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ c.sizeUpTo ↑i ≤ ↑j
Module: Mathlib.Data.Fintype.Inv

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
⊢ (Set.range f).domRestrict (invFun f) = hf.invOfMemRange

Tactic:
ext ⟨b, h⟩
  apply hf
  simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]

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

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑((c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩) = ↑(c.boundary ⟨i, i_lt''⟩)

Tactic:
c.orderEmbOfFin_boundaries

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑(c.boundary ⟨i, i_lt''⟩) = ↑(c.boundary ⟨i, i_lt''⟩)
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
⊢ g x ≠ x

Tactic:
eq_inv_mul_iff_mul_eq.2 hg₂,

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
⊢ ((Equiv.swap a y)⁻¹ * f) x ≠ x
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
by_cases h : f = 1
  · exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one
  · exact ne_of_gt (one_lt_card_support_of_ne_one h)

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (a a' : α ≃ β),
    ∀ b ∈ if h : ∀ (a_1 b : α), a (a_1 * b) = a a_1 * a b then some { toEquiv := a, map_mul' := h } else none,
      (b ∈ if h : ∀ (a b : α), a' (a * b) = a' a * a' b then some { toEquiv := a', map_mul' := h } else none) → a = a'

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd < a.fst

Tactic:
by
  simp only [finPairsLT, Fin.lt_def, true_and, mem_attachFin, mem_range, mem_univ,
    mem_sigma]

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

Goal state before:
pp: case neg
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₁ < f b₂
h✝ : f b₁ ≤ f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂

pp: case pos
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₂ ≤ f b₁
h✝ : f b₂ < f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂

Tactic:
· exact absurd this (not_le.mpr ha)

Goal state after:
case pos
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₂ ≤ f b₁
h✝ : f b₂ < f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂