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

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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG : IsIso (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
← colimit.pre_pre

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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG :
  IsIso
    (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor) ≫
      colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫
      pullback.snd f₁ f₂ ≫ f₃ =
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄

Tactic:
rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
⊢ (map α).Final

Tactic:
let F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
⊢ (map α).Final
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
    IsPullback f' g' g f → P.pullbacks g → P.pullbacks g'

Tactic:
by
    rintro _ _ _ _ _ _ _ _ h ⟨_, _, _, _, _, hp, hq⟩
    exact P.pullbacks_mk (h.paste_horiz hq) hp

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom g)

Tactic:
by
    convert! hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H
    simp [← CommRingCat.hom_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ pullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅ pullback f g

Tactic:
refine ?_ ≪≫
    pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv (pullback.fst _ _)) (g ≫ inv (pullback.fst _ _)) ≪≫ ?_

Goal state after:
case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ pullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅
    pullback (diagonal i)
      (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)

case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ pullback (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i

Tactic:
rw [Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
⊢ f ≫ i₁ = 𝟙 S ≫ f'

Tactic:
by simp [e₁]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ f ≫ i₁ = 𝟙 S ≫ f'

Tactic:
by simp [e₁]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) = fst f g ≫ f

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.comp_id (pullback.fst _ _), ← diagonal_fst i,
    pullback.condition_assoc]
  simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.limitsOfShape J ≤ W → W.IsStableUnderLimitsOfShape J

Tactic:
rintro h
    constructor
    intro X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ
    exact h _ (limitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

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

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
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X : C
p : P.LimitOfShape J X
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (StructuredArrow.mk (p.π.app X✝)).right.obj ⟶ (StructuredArrow.mk (p.π.app Y✝)).right.obj

Tactic:
exact p.diag.map f

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
        (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
      lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ =
    𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂))

Tactic:
by
    -- We could use `ext` here to immediately descend to the leaf goals,
    -- but it only obscures the structure.
    apply pullback.hom_ext
    · apply pullback.hom_ext
      · apply pullback.hom_ext
        · simp only [Category.assoc, lift_fst, lift_fst_assoc, Category.id_comp]
          rw [condition]
        · simp [Category.assoc, condition]
      · simp only [Category.assoc, lift_snd, lift_fst, Category.id_comp]
    · apply pullback.hom_ext
      · apply pullback.hom_ext
        · simp only [Category.assoc, lift_snd_assoc, lift_fst_assoc, lift_fst, Category.id_comp]
          rw [← condition_assoc, condition]
        · simp only [Category.assoc, lift_snd, lift_fst_assoc, lift_snd_assoc, Category.id_comp]
          rw [condition]
      · simp only [Category.assoc, lift_snd, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m ≫ fst (fst f g) (fst f h) = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)

Tactic:
by simpa

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

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
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X : C
p : P.ColimitOfShape J X
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (CostructuredArrow.mk (p.ι.app X✝)).left.obj ⟶ (CostructuredArrow.mk (p.ι.app Y✝)).left.obj

Tactic:
exact p.diag.map f

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
h : P.diagonal g
⊢ P (Over.Hom.left (Over.homMk (pullback.diagonal g) ⋯))

Tactic:
by simpa

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
rw [Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.IsClosedUnderLimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderColimitsOfShape J

Tactic:
by
  rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_op, op_monotone_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ B
g : A ⟶ 𝟙_ C
⊢ lift f (g ≫ η) ≫ μ = f

Tactic:
have := lift f g ≫= mul_one B
  rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) = 𝟙 (X ⊗ Y)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ (h ⊗ₘ k) = lift (f ≫ h) (g ≫ k)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') = g ⊗ₘ g'

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
⊢ (F ⋙ forget MonCat).IsRepresentable → yonedaMon.essImage F

Tactic:
rintro ⟨X, ⟨e⟩⟩
    let := MonObj.ofRepresentableBy X F e
    exact ⟨Mon.mk X, ⟨yonedaMonObjIsoOfRepresentableBy X F e⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
f g h : WithConv (C →ₗ[R] A)
⊢ (f + g) * h = f * h + g * h

Tactic:
ext; simp [map_add_left]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ prodComparisonIso (𝟭 C) A B = Iso.refl ((𝟭 C).obj (A ⊗ B))

Tactic:
by ext <;> simp

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

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
⊢ raise' (lower' (m :: l) n) n = m :: l

Tactic:
have : n ≤ m := h₁ _ List.mem_cons_self

Goal state after:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i

Tactic:
map_smul,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (f x • b.toDual (b x)) (b i) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i

Tactic:
map_smul,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, f x • (b.toDual (b i)) (b x) = f i
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M

Tactic:
← f.quotKerEquivRange.rank_eq,

Goal state after:
R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
⊢ Module.rank R (M ⧸ f.ker) + Module.rank R ↥f.ker = Module.rank R M
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
⊢ ∀ (s : Cocone (Discrete.functor Z)) (m : (coproductCocone Z).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ m = s.ι.app j) →
      m = ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))

Tactic:
rintro s f h

Goal state after:
R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ f = s.ι.app j
⊢ f = ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

Tactic:
rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
⊢ ℵ₀ ≤ lift.{u_4, u_5} (Module.rank K V)

Tactic:
by simpa

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ G.map (coequalizer.π f g) ≫ h = G.map (coequalizer.π f g) ≫ k → h = k

Tactic:
rw [← ι_comp_coequalizerComparison]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) ≫ h =
      (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) ≫ k →
    h = k
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : P ⟶ Q := ⋯
t : P ⟶ Q := ⋯
I : C := ⋯
i : I ⟶ P := ⋯
⊢ Fork (G.map s) (G.map t)

Tactic:
apply Fork.ofι (G.map i)
      rw [← G.map_comp, ← G.map_comp]
      apply congrArg G.map
      exact equalizer.condition s t

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
⊢ (NormalEpi.g ≫ g) ≫ h' = 0 ≫ h'

Tactic:
eq_whisker gn.w

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
⊢ 0 ≫ h' = 0 ≫ h'
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
⊢ ∀ [FinCategory J], PreservesColimitsOfShape J G

Tactic:
fJ

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J G
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ b ≫ b' ≫ cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ = b ≫ s.inr

Tactic:
have reassoced' {W : C} (h : cokernel (coprod.desc f g) ⟶ W) : b ≫ b' ≫ h
                = cokernel.π (coprod.desc f g) ≫ h := by rw [← Category.assoc, eq_whisker hb']

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
reassoced' : ∀ {W : C} (h : cokernel (coprod.desc f g) ⟶ W), b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h
⊢ b ≫ b' ≫ cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ = b ≫ s.inr
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i

Tactic:
rw [Category.comp_id, Category.id_comp]

Goal state after: