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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
by simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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 H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ H.map (F.map f)

Tactic:
α.naturality

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 H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ α.app (F.obj X) ≫ H.map (F.map f) = α.app (F.obj X) ≫ H.map (F.map f)
Module: Mathlib.CategoryTheory.Whiskering

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

Tactic:
α.naturality

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ F.map (α.app X ≫ H.map f) = F.map (α.app X ≫ H.map f)
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 : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

Tactic:
simpa using Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)) (f := e.unit.app _)

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u_1
𝒞 : Category.{?u.22, u_1} C
D : Type u
inst✝ : Groupoid D
F : C ⥤ D
h : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ h.preimage (inv (F.map f)) ≫ f = 𝟙 Y✝

Tactic:
by
      apply h.map_injective
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u_1
𝒞 : Category.{?u.22, u_1} C
D : Type u
inst✝ : Groupoid D
F : C ⥤ D
h : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ f ≫ h.preimage (inv (F.map f)) = 𝟙 X✝

Tactic:
by
      apply h.map_injective
      simp

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

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

Tactic:
by simp only [← op_comp, p.w]

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F G : J ⥤ Type w
φ : F ⟶ G
x : ↑F.sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (G.map f)) ((fun j ↦ (ConcreteCategory.hom (φ.app j)) (↑x j)) j) =
    (fun j ↦ (ConcreteCategory.hom (φ.app j)) (↑x j)) j'

Tactic:
by simp [← NatTrans.naturality_apply, x.2 f]

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
inst✝ : sq.HasLift
⊢ ⋯.HasLift

Tactic:
by
  rw [right_adjoint_hasLift_iff]
  infer_instance

Goal state after:
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 : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfDiagramTerminal tX F).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app X

Tactic:
simp [← w X]

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

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePushoutShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
constructor
  intro a b
  casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)
  repeat rfl

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
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
⊢ (∀ (j : J), g ≫ π arrows j = fs j) → g ≫ base arrows = f → g = lift f fs w

Tactic:
intro h1

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
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
⊢ g ≫ base arrows = f → g = lift f fs w
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
⊢ (∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2

Tactic:
intro h1

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
⊢ g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2
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_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
by simp [w]

Goal state after:
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_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
by simp [w]

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) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g = fs j) → head arrows ≫ g = f → g = desc f fs w

Tactic:
intro h1

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
⊢ head arrows ≫ g = f → g = desc f fs w
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) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2

Tactic:
intro h1

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
⊢ head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := left } = t.π.app { as := left }

Tactic:
exact hl₁ _ _

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

Goal state before:
pp: β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
b : β
⊢ Sigma.ι f b ≫ (coproductUniqueIso f).hom = eqToHom ⋯

Tactic:
by
  obtain rfl := Subsingleton.allEq b default
  symm
  simp [← Iso.comp_inv_eq]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso c.inl

Tactic:
rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
    refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
    rw [Category.comp_id]
    have e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c := congrArg (· ≫ inl c) hl
    rwa [Category.assoc, Category.id_comp] at e

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (prod.rightUnitor X).inv ≫ prod.map f (𝟙 (⊤_ C)) = f ≫ (prod.rightUnitor Y).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
H : C ⥤ D
inst✝ : HasBinaryProduct (H.obj A) (H.obj B)
α : F ⟶ H
⊢ prod.lift (α.app (A ⨯ B) ≫ H.map prod.fst) (α.app (A ⨯ B) ≫ H.map prod.snd) =
    prod.lift (α.app (A ⨯ B) ≫ H.map prod.fst) (F.map prod.snd ≫ α.app B)

Tactic:
α.naturality

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
H : C ⥤ D
inst✝ : HasBinaryProduct (H.obj A) (H.obj B)
α : F ⟶ H
⊢ prod.lift (α.app (A ⨯ B) ≫ H.map prod.fst) (α.app (A ⨯ B) ≫ H.map prod.snd) =
    prod.lift (α.app (A ⨯ B) ≫ H.map prod.fst) (α.app (A ⨯ B) ≫ H.map prod.snd)
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
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst✝³ : G.Faithful
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).Full

Tactic:
apply Comma.full_map

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 : D
T : C ⥤ D
f✝ : StructuredArrow S T
h : f✝.IsUniversal
g : StructuredArrow S T
f : f✝.right ⟶ g.right
w : (fun η ↦ f✝.hom ≫ T.map η = g.hom) f
⊢ f✝.hom ≫ T.map f = f✝.hom ≫ T.map (h.desc g)

Tactic:
by simp [w]

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
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝³ : G.Faithful
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).Full

Tactic:
apply Comma.full_map

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).hom ≫ prod.fst = pullback.fst f prod.fst

Tactic:
by
  simp [pullbackProdFstIsoProd]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).hom ≫ prod.snd = pullback.snd f prod.fst ≫ prod.snd

Tactic:
by
  simp [pullbackProdFstIsoProd]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).inv ≫ pullback.fst f prod.fst = prod.fst

Tactic:
by
  simp [pullbackProdFstIsoProd]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).inv ≫ pullback.snd f prod.fst ≫ prod.fst = prod.fst ≫ f

Tactic:
by
  simp [pullbackProdFstIsoProd]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).inv ≫ pullback.snd f prod.fst ≫ prod.snd = prod.snd

Tactic:
by
  simp [pullbackProdFstIsoProd]

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

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

Tactic:
rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s : PushoutCocone f g
H : IsColimit s
⊢ IsColimit (mk s.inl s.inr ⋯)

Tactic:
apply PushoutCocone.isColimitAux'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s : PushoutCocone f g
H : IsColimit s
⊢ (s_1 : PushoutCocone (h ≫ f) (h ≫ g)) →
    { l //
      (mk s.inl s.inr ⋯).inl ≫ l = s_1.inl ∧
        (mk s.inl s.inr ⋯).inr ≫ l = s_1.inr ∧
          ∀ {m : (mk s.inl s.inr ⋯).pt ⟶ s_1.pt},
            (mk s.inl s.inr ⋯).inl ≫ m = s_1.inl → (mk s.inl s.inr ⋯).inr ≫ m = s_1.inr → m = l }
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
g : CostructuredArrow S T
f : g.left ⟶ f✝.left
w : (fun η ↦ S.map η ≫ f✝.hom = g.hom) f
⊢ S.map f ≫ f✝.hom = S.map (h.lift g) ≫ f✝.hom

Tactic:
by simp [w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
l : image f ⟶ F'.I
w : l ≫ F'.m = image.ι f
⊢ l ≫ F'.m = image.lift F' ≫ F'.m

Tactic:
by simp [w]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : X ⟶ M
⊢ f = default

Tactic:
by
    ext x
    subsingleton

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 : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ factorThruImage f ≫ image.ι f = 0

Tactic:
w,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ factorThruImage f ≫ 0 = 0
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
⊢ map = map'

Tactic:
by
  have : map ≫ image.ι g.hom = map' ≫ image.ι g.hom := by rw [map_ι, map_ι']
  apply (cancel_mono (image.ι g.hom)).1 this

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = 0

Tactic:
have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp]
  simpa using h

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

Goal state before:
pp: case toFun.left
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 X = 0

Tactic:
exact (idZeroEquivIsoZero X).symm eX

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 : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ kernel.lift f g h ≫ kernel.ι f = 0

Tactic:
w,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ kernel.lift f g h ≫ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ cokernel.π f ≫ cokernel.desc f g h = 0

Tactic:
w,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ 0 ≫ cokernel.desc f g h = 0
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
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0

Tactic:
by simp [w]

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
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0

Tactic:
by simp [w]

Goal state after:
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
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
have := preservesSmallestLimits_of_preservesLimits F
    exact preservesLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h
  congr <;> injection h

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

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

Tactic:
Fork.condition,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ Fork.ι s ≫ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

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

Tactic:
w,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
⊢ 0 = ι ≫ 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (piComparison G f)

Tactic:
← PreservesProduct.iso_hom

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (PreservesProduct.iso G f).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

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

Tactic:
w,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
π : Y ⟶ Z
w : f ≫ π = 0
⊢ 0 = 0 ≫ π
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : f ≫ cokernel.π f = 0
| f ≫ cokernel.π f = 0

Tactic:
lhs
          congr
          rw [← image.fac f]

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : f ≫ cokernel.π f = 0
| factorThruImage f ≫ image.ι f

case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : f ≫ cokernel.π f = 0
| cokernel.π 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✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| f ≫ cokernel.π (image.ι f) = 0

Tactic:
lhs
          congr
          rw [← image.fac f]

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| factorThruImage f ≫ image.ι f

case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| cokernel.π (image.ι f)
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
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
by simp [w]

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

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
inst✝ : Preadditive D
F G : C ⥤ D
ι : Type u_3
s : Finset ι
X : C
α : ι → (F ⟶ G)
⊢ (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X

Tactic:
by
  simp only [← appHom_apply, map_sum]

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

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

Tactic:
simp [biproduct.ι_π_ne _ h, biproduct.ι_π_ne _ this]

Goal state after: