mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ ⟦⟨i, r • x✝⟩⟧ = (map₀ f fun i ↦ (algebraMap R (G i)) r) * ⟦⟨i, x✝⟩⟧

Tactic:
map₀_algebraMap i,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ ⟦⟨i, r • x✝⟩⟧ = ⟦⟨i, (algebraMap R (G i)) r⟩⟧ * ⟦⟨i, x✝⟩⟧
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
⊢ Function.Even (r • g)

Tactic:
intro a
  simp only [Pi.smul_apply, hg a]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-(↑N + ↑1)) (↑N + ↑1), f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0

Tactic:
Nat.cast_one,

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-(↑N + 1)) (↑N + 1), f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
⊢ ∏ m ∈ Icc (-(↑0 + 1)) (↑0 + 1), f m = f (↑0 + 1) * f (-(↑0 + 1)) * ∏ m ∈ Icc (-↑0) ↑0, f m

Tactic:
rw [Icc_succ_succ]
    grind

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

Goal state before:
pp: case mp
α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs

pp: case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2

Tactic:
· intro h
    exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩

Goal state after:
case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α n
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Tactic:
induction n with
  | zero =>
    refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
    rintro rfl
    exact fun a ha ↦ (Finset.notMem_empty _ ha).elim
  | succ n ih => ?_
  refine mem_sup.trans ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨a, ha, he⟩ b hb
    rw [mem_image] at he
    obtain ⟨m, he, rfl⟩ := he
    rw [Sym.mem_cons] at hb
    obtain rfl | hb := hb
    · exact ha
    · exact ih.1 he _ hb
  · obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ
    exact
      ⟨a, h _ <| Sym.mem_cons_self _ _,
        mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩

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

Goal state before:
pp: case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ x ∈ s(x✝, y✝) ∧ y ∈ s(x✝, y✝) → s(x✝, y✝) = s(x, y)

Tactic:
rw [mem_iff, mem_iff]

Goal state after:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ (x = x✝ ∨ x = y✝) ∧ (y = x✝ ∨ y = y✝) → s(x✝, y✝) = s(x, y)
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
rw [w]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ x) = x

Tactic:
refine x.recOnSubsingleton fun x => ?_
    obtain ⟨x, hx⟩ := x
    obtain - | ⟨-, x⟩ := x
    · simp at hx
    rcases x with - | ⟨_, x⟩
    · simp at hx
    rcases x with - | ⟨_, x⟩
    swap
    · exfalso
      simp at hx
    rfl

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Reassoc

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
rw [w]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.IsoReassoc

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ≅ Y
w : f = g
Z : C
h : Y ≅ Z
⊢ f ≪≫ h = g ≪≫ h

Tactic:
rw [w]

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

Goal state before:
pp: case cons.zero
V : Type u
inst✝ : Quiver V
a b d : V
q : a ⟶ d
h : ∀ {n : ℕ}, nil.length = n + 1 → ∃ c f q x, nil = f.toPath.comp q
hp : nil.length = 0
⊢ ∃ c f q_1 x, nil.cons q = f.toPath.comp q_1

Tactic:
exact ⟨d, q, nil, rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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 : C
p : X = Y
⊢ F.mapIso (eqToIso p) = eqToIso ⋯

Tactic:
ext; cases p; simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
f : D ≌ E
X : C
⊢ f.functor.map
        (e.functor.map
          (e.unitIso.hom.app X ≫
            e.inverse.map
                (𝟙 (e.functor.obj X) ≫
                  f.unitIso.hom.app (e.functor.obj X) ≫ 𝟙 (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
              𝟙 (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
      𝟙 (f.functor.obj (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
        f.functor.map
            (𝟙 (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫
              e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))) ≫
                𝟙 (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
          f.counitIso.hom.app (f.functor.obj (e.functor.obj X)) =
    𝟙 (f.functor.obj (e.functor.obj X))

Tactic:
simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
      functor_unit_comp_assoc, assoc]

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
e : C ≌ D
f : D ≌ E
X : C
⊢ f.functor.map (f.unitIso.hom.app (e.functor.obj X)) ≫
      f.functor.map (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
        f.functor.map (e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
          f.counitIso.hom.app (f.functor.obj (e.functor.obj X)) =
    𝟙 (f.functor.obj (e.functor.obj X))
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f ≫ (NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom.op =
    (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom.op ≫
      Quiver.Hom.op { app := fun X ↦ f.unop.app X, naturality := ⋯ }

Tactic:
show f = f.unop.op by simp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f.unop.op ≫ (NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom.op =
    (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom.op ≫
      Quiver.Hom.op { app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ }
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ ofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i)

Tactic:
constructor
  · rintro ⟨i⟩
    exact ⟨i, rfl⟩
  · rintro ⟨i, h⟩
    rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]
    constructor

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : Arrow C
f : X ⟶ Y
⊢ F.map (Arrow.Hom.left f) ≫ (Arrow.mk (F.map Y.hom)).hom = (Arrow.mk (F.map X.hom)).hom ≫ F.map (Arrow.Hom.right f)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ P f

Tactic:
exact (P.arrow_mk_iso_iff e).1 hf'

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : C ⥤ D
G✝ : D ⥤ C
F G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
⊢ ∀ (Y : D),
    (adj.unit ≫ whiskerRight iso.hom H).app (H.obj Y) ≫ H.map ((H.whiskerLeft iso.inv ≫ adj.counit).app Y) = 𝟙 (H.obj Y)

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
⊢ eqToHom η ▷ h = eqToHom ⋯

Tactic:
by
  cases η
  simp only [id_whiskerRight, eqToHom_refl]

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ Skeletal (Skeleton C)

Tactic:
rintro X Y ⟨h⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
⊢ X = Y
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ F.map (h.i ≫ h.r) = 𝟙 (F.obj X)

Tactic:
h.retract,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ F.map (𝟙 X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.left (Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.right (Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (τ.app X)))

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ (adj.homEquiv B X).symm l.l ≫ p = v

Tactic:
by
        rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]
        apply (adj.homEquiv _ _).left_inv

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

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
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝² : F'.PreservesMonomorphisms
inst✝¹ : F.PreservesEpimorphisms
inst✝ : StrongEpi f
X Y : D
Z : X ⟶ Y
⊢ ∀ [Mono Z], HasLiftingProperty (F.map f) Z

Tactic:
intro
    rw [adj.hasLiftingProperty_iff]
    infer_instance

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
⊢ StrongEpi f

Tactic:
have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
      Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi f
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ ((Functor.const J).obj (F.obj X)).map k ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k

Tactic:
by
        dsimp
        rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasCoproduct F.obj
Z✝ : C
x✝¹ x✝ : colimit F ⟶ Z✝
h : Sigma.desc (colimit.ι F) ≫ x✝¹ = Sigma.desc (colimit.ι F) ≫ x✝
⊢ x✝¹ = x✝

Tactic:
refine colimit.hom_ext fun j => ?_
    simpa using Sigma.ι _ j ≫= h

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
X✝ Y✝ : StructuredArrow S F
f : X✝ ⟶ Y✝
⊢ (mk (G.map X✝.hom)).hom ≫ (F ⋙ G).map (Hom.right f) = (mk (G.map Y✝.hom)).hom

Tactic:
simp [← Functor.map_comp]

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
f g : Over X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x✝ : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x✝ ≫ (liftCone D s c p hp).π.app j = t.π.app j
⊢ x✝ = homMk (hc.lift ((forget X).mapCone t)) ⋯

Tactic:
by
    ext
    refine hc.hom_ext (fun j ↦ ?_)
    simp [dsimp% hc.fac ((forget X).mapCone t) j, ← hm]

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ (F ⋙ G).map (pullback.fst f g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ (F ⋙ G).map (pullback.snd f g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
inst✝¹ : S.Full
inst✝ : S.Faithful
⊢ ∀ (s : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))) (m : s.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt),
    (∀ (j : Discrete PEmpty.{1}), m ≫ (asEmptyCone (mk (𝟙 (S.obj Y)))).π.app j = s.π.app j) →
      m = homMk (S.preimage s.pt.hom) ⋯

Tactic:
rintro c m -
    ext
    apply S.map_injective
    simpa only [homMk_left, S.map_preimage, ← w m] using! (Category.comp_id _).symm

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

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

Tactic:
map_ι'

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0

Tactic:
change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default
    rw [← Category.assoc]
    congr
    simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X : C
⊢ IsIso 0 ≃ 𝟙 X = 0

Tactic:
by simpa using isIsoZeroEquiv X X

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

Goal state before:
pp: case h₀.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inl ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.fst =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inl ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.snd =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h₁.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inr ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.fst =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inr ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.snd =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app zero = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app zero

Tactic:
exact (Iso.eq_inv_comp i).2 h

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
⊢ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) = 𝟙 (⨁ f ∘ ⇑ε)

Tactic:
ext b b'

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b b' : β
⊢ ι (f ∘ ⇑ε) b' ≫ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) ≫ π (f ∘ ⇑ε) b =
    ι (f ∘ ⇑ε) b' ≫ 𝟙 (⨁ f ∘ ⇑ε) ≫ π (f ∘ ⇑ε) b
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
⊢ matrix m ≫ π g k = desc fun j ↦ m j k

Tactic:
ext
  simp [biproduct.matrix]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ x = 0

Tactic:
dsimp [x]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ f ≫ inv f ≫ biprod.fst = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ (filter (fun x ↦ x = 0) l).sum = 0

Tactic:
simp [sum_eq_zero_iff]

Goal state after: