mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α)) (map (fun y ↦ s(x, y)) (x :: xs)) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p ↦ x ::ₛ p) ∘ fun x ↦ x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2

Tactic:
map_map

Goal state after:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α) ∘ fun y ↦ s(x, y)) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p ↦ x ::ₛ p) ∘ fun x ↦ x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ ∅, f i = ⊤ ↔ ∃ i ∈ ∅, f i = ⊤

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊤ ↔ ∃ i ∈ s✝, f i = ⊤
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊤ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊤

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ ∅, f i = ⊥ ↔ ∃ i ∈ ∅, f i = ⊥

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊥ ↔ ∃ i ∈ s✝, f i = ⊥
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊥ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊥

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
x✝ y✝ : α
⊢ ↑(map f s(x✝, y✝)) = f '' ↑s(x✝, y✝)

Tactic:
simp [Set.image_pair]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.coe_nil, Multiset.cons_zero,
        Multiset.cons_eq_cons, Multiset.singleton_inj, ne_eq, Multiset.singleton_eq_cons_iff,
        exists_eq_right_right, and_true]

Goal state after:
α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x✝ : R'
x : R' ⊗[R] S
⊢ ∀ (x y : R' ⊗[R] S),
    ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • x) =
        (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun x →
      ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • y) =
          (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun y →
        ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • (x + y)) =
          (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x + y)

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
⊢ Nonempty F.FullyFaithful

Tactic:
have : F.Faithful := ⟨fun h ↦ (hF _ _).injective h⟩
    have : F.Full := ⟨(hF _ _).surjective⟩
    exact ⟨.ofFullyFaithful _⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ⇑(hom (f ≫ g)) = ⇑(hom g) ∘ ⇑(hom f)

Tactic:
by
  ext
  simp [ConcreteCategory.comp_apply]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : nil.toList = (p.cons f).toList
⊢ nil = p.cons f

Tactic:
by cases h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : (p.cons f).toList = nil.toList
⊢ p.cons f = nil

Tactic:
by cases h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))

Tactic:
· exact hΦinv (Sum.inl _)

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ reverse (reverse (PushQuiver.arrow f)) = PushQuiver.arrow f

Tactic:
dsimp [reverse]

Goal state after:
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f)) = PushQuiver.arrow f
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : F.ReflectsIsomorphisms
X Y : C ⥤ D
f : X ⟶ Y
x✝ : IsIso (((whiskeringRight C D E).obj F).map f)
⊢ IsIso f

Tactic:
NatTrans.isIso_iff_isIso_app

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : F.ReflectsIsomorphisms
X Y : C ⥤ D
f : X ⟶ Y
x✝ : IsIso (((whiskeringRight C D E).obj F).map f)
⊢ ∀ (X_1 : C), IsIso (f.app X_1)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ P f → ofHoms P.homFamily f

Tactic:
· intro hf
    exact ⟨(⟨f, hf⟩ : P.toSet)⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (⨅ i, W i).RespectsLeft Q

Tactic:
← sInf_range

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsLeft Q
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (⨅ i, W i).RespectsRight Q

Tactic:
← sInf_range

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsRight Q
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ (⨅ i, W i).RespectsIso

Tactic:
← sInf_range

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsIso
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
⊢ P.map F = P.map G

Tactic:
revert F G e

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D} (e : F ≅ G), P.map F = P.map G
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.inverseImage F).map F = P

Tactic:
P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.map F.asEquivalence.inverse).map F = P
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
⊢ post F G ≫ G.map (desc F c) = desc (F ⋙ G) (G.mapCocone c)

Tactic:
by
  ext
  rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]
  rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f j'

Tactic:
simp [*]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ ∀ {X Y : WalkingSpan} (f : X ⟶ Y), F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingCospan} (f_1 : X_1 ⟶ Y_1),
    (cospan f g ⋙ F).map f_1 ≫
        (Option.casesOn Y_1 (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
            WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
              (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
      (Option.casesOn X_1 (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
            WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
              (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
        (cospan (F.map f) (F.map g)).map f_1

Tactic:
by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingSpan} (f_1 : X_1 ⟶ Y_1),
    (span f g ⋙ F).map f_1 ≫
        (Option.casesOn Y_1 (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
            WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
              (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
      (Option.casesOn X_1 (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
            WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
              (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
        (span (F.map f) (F.map g)).map f_1

Tactic:
by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ i₁ ≫ f' ≫ j₃ = (i₁ ≫ j₁) ≫ f''

Tactic:
e₃,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ i₁ ≫ f' ≫ j₂ = (i₁ ≫ j₁) ≫ f''

Tactic:
e₃,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ ∃ a, (post F).map a = f

Tactic:
exact ⟨Under.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by ext; simpa⟩

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Over X)ᵒᵖ
f : Z ⟶ Y
⊢ (mk (unop Z).hom.op).hom ≫ (Over.Hom.left f.unop).op = (mk (unop Y).hom.op).hom

Tactic:
by dsimp; rw [← Over.w f.unop, op_comp]

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

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ data.mapZ (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯) ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      data.mapZ (Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

Tactic:
← data.mapZ_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ data.mapZ
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      data.mapZ (Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)
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]
  rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
⊢ g = 0 → f ≫ g = 0

Tactic:
by simp +contextual

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ 0 ≫ f = 0

Tactic:
zero_comp

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ 0 = 0
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
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocone.precompose h.hom).obj c)
⊢ IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))

Tactic:
apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)

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
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocone.precompose h.hom).obj c)
⊢ F.mapCocone ((Cocone.precompose h.hom).obj c) ≅
    (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map 0 = F.map (0 ≫ F.preimage 0)

Tactic:
zero_comp

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map 0 = F.map 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

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

Tactic:
zero_comp

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
⊢ 0 = 0
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
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := mono_of_isLimit_fork i
⊢ c.ι ≫ f = c.ι

Tactic:
← c.condition

Goal state after:
C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := mono_of_isLimit_fork i
⊢ c.ι ≫ 𝟙 X = c.ι
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 : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m✝ = s.π
⊢ m✝ = ↑l

Tactic:
apply Cofork.IsColimit.hom_ext i

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := ⋯
l : { l // c.π ≫ l = s'.π } := ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m✝ = s.π
⊢ c.π ≫ m✝ = c.π ≫ ↑l
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✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : Y ⟶ Z
⊢ (rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom).toFun ((leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom) x) = x

Tactic:
by
      simp only [Iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, rightComp_apply,
        leftComp_apply, LinearMap.toFun_eq_coe, Iso.inv_hom_id_assoc, Category.assoc,
        Iso.inv_hom_id, Category.comp_id]

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 : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ : (coforkOfCokernelCofork c).pt ⟶ s.pt
h : (coforkOfCokernelCofork c).π ≫ m✝ = s.π
⊢ m✝ = i.desc (cokernelCoforkOfCofork s)

Tactic:
apply Cofork.IsColimit.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 : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ : (coforkOfCokernelCofork c).pt ⟶ s.pt
h : (coforkOfCokernelCofork c).π ≫ m✝ = s.π
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ i.desc (cokernelCoforkOfCofork s)
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 : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ : (cokernelCoforkOfCofork c).pt ⟶ s.pt
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = s.π
⊢ m✝ = i.desc (coforkOfCokernelCofork s)

Tactic:
apply Cofork.IsColimit.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 : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ : (cokernelCoforkOfCofork c).pt ⟶ s.pt
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = s.π
⊢ c.π ≫ m✝ = c.π ≫ i.desc (coforkOfCokernelCofork s)
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
by
        have := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
        exact preservesLimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Goal state after: