mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
⊢ False

Tactic:
obtain ⟨D, hD⟩ := exists_fg_and_mem_baseChange x

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
D : Subalgebra R A
hD : D.FG ∧ x ∈ Subalgebra.baseChange C D
⊢ False
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✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
i : ι
ne : ⟦⟨i, 0⟩⟧ ≠ 0
⊢ False

Tactic:
exact ne (zero_def i).symm

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 ∈ range (N + 1), f ↑m) ^ 2 / f 0 * (f (↑N + 1) * f (↑N + 1)) =
    ((∏ x ∈ range (N + 1), f ↑x) * f ↑(N + 1)) ^ 2 / f 0

Tactic:
← pow_two,

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 ∈ range (N + 1), f ↑m) ^ 2 / f 0 * f (↑N + 1) ^ 2 = ((∏ x ∈ range (N + 1), f ↑x) * f ↑(N + 1)) ^ 2 / f 0
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
⊢ map (fun y ↦ s(x, y)) (x' :: xs) <+ (x' :: xs).sym2

Tactic:
simp only [map_cons, List.sym2, cons_append]
    cases h with
    | head =>
      exact (sublist_append_left _ _).cons_cons _
    | tail _ h =>
      refine .cons _ ?_
      rw [← singleton_append]
      refine .append ?_ (ih h)
      rw [singleton_sublist, mem_map]
      exact ⟨_, h, Sym2.eq_swap⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ Rel β (f p.1 ⋯, f p.2 ⋯) (f q.1 ⋯, f q.2 ⋯)

Tactic:
rw [rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
⊢ homOfEq f hX hY = g ↔ f = homOfEq g ⋯ ⋯

Tactic:
by
  subst hX hY; simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
⊢ f = homOfEq g hX hY ↔ homOfEq f ⋯ ⋯ = g

Tactic:
by
  subst hX hY; simp

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

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 ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ inv (α.app X) ≫ F.map f = G.map f ≫ inv (α.app Y)

Tactic:
by
  rw [IsIso.inv_comp_eq, ← Category.assoc, IsIso.eq_comp_inv]
  exact α.naturality f

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 G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom ⋯)

Tactic:
rw [α.naturality_assoc]

Goal state after:
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 : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
rw [ofHoms_iff] at hf

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ i, Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : C ⥤ D
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ ∀ {X_1 Y : Cᵒᵖ ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
intro Y Z f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type v₁
f : Y ⟶ Z
⊢ ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
      ((evaluation Cᵒᵖ (Type v₁) ⋙
                (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
            X).map
        f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
intro Y Z f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation Cᵒᵖ (Type v₁) ⋙
            (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
        f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
intro Y Z f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
⊢ ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
      ((evaluation C (Type v₁) ⋙
                (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
            X).map
        f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
intro Y Z f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
⊢ (coyoneda.rightOp ⋙ coyoneda).map f ≫
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation C (Type v₁) ⋙
            (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
        f
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v, u} C ↔ EssentiallySmall.{w, v', u'} D

Tactic:
by
  fconstructor
  · rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.symm.trans f)
  · rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.trans f)

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
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z

Tactic:
adj.hasLiftingProperty_iff

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
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
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
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'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono f
inst✝ : F.ReflectsMonomorphisms
⊢ Mono (F.map ((adj.homEquiv X Y) f))

Tactic:
← (homEquiv adj X Y).symm_apply_apply f

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
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono ((adj.homEquiv X Y).symm ((adj.homEquiv X Y) f))
inst✝ : F.ReflectsMonomorphisms
⊢ Mono (F.map ((adj.homEquiv X Y) f))
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})

Tactic:
· rintro ⟨⟨p⟩, h⟩
    have := fun x y => (h x y).some
    refine
      Nonempty.intro
        (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.punitExt))
    exact
      NatIso.ofComponents fun _ =>
        { hom := default
          inv := default }

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ limMap (α ≫ β) = limMap α ≫ limMap β

Tactic:
apply Limits.limit.hom_ext; intro j
    simp [assoc]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 = g2

Tactic:
apply limit.hom_ext

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ ∀ (j : WidePullbackShape J),
    g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j =
      g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ i₁ ≫ fst = i₂ ≫ fst

Tactic:
← cancel_mono f

Goal state after:
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ (i₁ ≫ fst) ≫ f = (i₂ ≫ fst) ≫ f
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 : D
T : C ⥤ D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ η = η'

Tactic:
h.hom_desc η,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ h.desc (mk (f.hom ≫ T.map η)) = η'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ G.map (pullback.lift h k w) ≫ pullbackComparison G f g = pullback.lift (G.map h) (G.map k) ⋯

Tactic:
by
  ext <;> simp [← G.map_comp]

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 : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map f ≫ G.map (pushout.inl f g) = G.map g ≫ G.map (pushout.inr f g)

Tactic:
by simp only [← G.map_comp, pushout.condition]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushoutComparison G f g ≫ G.map (pushout.desc h k w) = pushout.desc (G.map h) (G.map k) ⋯

Tactic:
by
  ext <;> simp [← G.map_comp]

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 f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.fst = k ≫ t.fst

Tactic:
← cancel_mono f,

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 f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ (h ≫ t.fst) ≫ f = (k ≫ t.fst) ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
⊢ s.fst ≫ 𝟙 X = s.snd

Tactic:
← cancel_mono f,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
⊢ (s.fst ≫ 𝟙 X) ≫ f = s.snd ≫ f
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 : D
S : C ⥤ D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ η = η'

Tactic:
h.hom_desc η,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ h.lift (mk (S.map η ≫ f.hom)) = η'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case e'_4.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
f : X ⟶ Y
⊢ h = h ≫ 𝟙 X

Tactic:
exact (Category.comp_id _).symm

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

Goal state before:
pp: case e'_5.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
f : X ⟶ Y
e_3✝ : Y = (span (h ≫ f) (h ≫ 𝟙 X)).obj WalkingSpan.left
e_4✝ : pushout (h ≫ f) h = colimit (span (h ≫ f) (h ≫ 𝟙 X))
⊢ h = h ≫ 𝟙 X

Tactic:
exact (Category.comp_id _).symm

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

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

Tactic:
exact (Category.comp_id _).symm

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

Goal state before:
pp: case calc_1
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.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ 𝟙 (F.obj Y)

Tactic:
exact (Category.comp_id _).symm

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)

Tactic:
apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit

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✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := ⋯
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ IsZero X

Tactic:
by
  rw [IsZero.iff_id_eq_zero]
  apply hX.hom_ext

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
hX : IsInitial X
⊢ IsZero X

Tactic:
by
  rw [IsZero.iff_id_eq_zero]
  apply hX.hom_ext

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : P Y ∨ Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
obtain hY | hY := hY

Goal state after:
case mp.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : P Y
⊢ P.isoClosure X ∨ Q.isoClosure X

case mp.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 = Fork.ι s

Tactic:
← cancel_mono 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 : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 ≫ f = Fork.ι s ≫ f
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 : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c

Tactic:
← cancel_mono f,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
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
F : MonoFactorisation f
⊢ kernel.ι f ≫ F.e = 0

Tactic:
← cancel_mono F.m,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
F : MonoFactorisation f
⊢ (kernel.ι f ≫ F.e) ≫ F.m = 0 ≫ F.m
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
hm : m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι
⊢ m = m ≫ 𝟙 (⨁ Subtype.restrict (fun j ↦ j ≠ i) f)

Tactic:
exact (Category.comp_id _).symm

Goal state after: