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

Goal state before:
pp: case tmul.add
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : CommSemiring R
inst✝³⁰ : CommSemiring S
inst✝²⁹ : Algebra R S
inst✝²⁸ : Module R M
inst✝²⁷ : Module R N
inst✝²⁶ : Module S N
inst✝²⁵ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
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'
a : S
b : R'
x y : S ⊗[R] R'
a✝¹ : ⋯.equiv (a ⊗ₜ[R] b * x) = ⋯.equiv (a ⊗ₜ[R] b) * ⋯.equiv x
a✝ : ⋯.equiv (a ⊗ₜ[R] b * y) = ⋯.equiv (a ⊗ₜ[R] b) * ⋯.equiv y
⊢ ⋯.equiv (a ⊗ₜ[R] b * (x + y)) = ⋯.equiv (a ⊗ₜ[R] b) * ⋯.equiv (x + y)

Tactic:
| add x y _ _ =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (fun x ↦ uncurry Sym2.mk (f x.1, f x.2)) '' s ×ˢ s = (fun x ↦ Sym2.map f (uncurry Sym2.mk x)) '' s ×ˢ s

Tactic:
uncurry,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (fun x ↦ s(f x.1, f x.2)) '' s ×ˢ s = (fun x ↦ Sym2.map f s(x.1, x.2)) '' s ×ˢ s
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ (α.symm ≪≫ α) ≪≫ β = β

Tactic:
symm_self_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ refl Y ≪≫ β = β
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
ι : Type u'
X : ι → C
F : C ⥤ D
⊢ (ofObj X).strictMap F = ofObj (F.obj ∘ X)

Tactic:
by
  ext Y
  simp [ofObj_iff, strictMap_iff]

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
F₁ : C ⥤ D
⊢ ∀ {F₂ : C ⥤ D} (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.map f)

Tactic:
F₂

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
⊢ ∀ (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.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
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
have := (F.mapIso <| η.app X).hom_inv_id

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj ((𝟭 C).obj X))
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left

Tactic:
by
  rw [← comp_left, e.inv_hom_id, id_left]

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ Epi (f ≫ g) ↔ Epi f

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  simpa using (inferInstance : Epi ((f ≫ g) ≫ inv g))

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
adj : CoreHomEquivUnitCounit F G
x✝² : C
x✝¹ : D
x✝ : F.obj x✝² ⟶ x✝¹
⊢ (mk' adj).unit.app x✝² ≫ G.map x✝ = (adj.homEquiv x✝² x✝¹) x✝

Tactic:
adj.homEquiv_unit,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
x✝² : C
x✝¹ : D
x✝ : F.obj x✝² ⟶ x✝¹
⊢ (mk' adj).unit.app x✝² ≫ G.map x✝ = adj.unit.app x✝² ≫ G.map x✝
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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
⊢ ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ (rightAdjointOfEquiv e he).obj Y),
    (e X' Y).symm (f ≫ g) = F.map f ≫ (e X Y).symm g

Tactic:
by
        intro X X' Y f g; rw [Equiv.symm_apply_eq]; simp [he]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.map g.op)) (yonedaEquiv f) = (ConcreteCategory.hom (f.app (op Y))) g

Tactic:
yonedaEquiv_naturality,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ yonedaEquiv (yoneda.map g ≫ f) = (ConcreteCategory.hom (f.app (op Y))) g
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
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi (F.map f) ↔ StrongEpi f

Tactic:
constructor
  · intro
    have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
      Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
    rw [StrongEpi.iff_of_arrow_iso e]
    infer_instance
  · intro
    infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl ↦ isLimitChangeEmptyCone C hl c₁ h.symm) fun hl ↦ isLimitChangeEmptyCone C hl c₂ h

Tactic:
by
    dsimp [Function.LeftInverse, Function.RightInverse]; intro
    simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl ↦ isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl ↦
    isColimitChangeEmptyCocone C hl c₂ h

Tactic:
by
    dsimp [Function.LeftInverse, Function.RightInverse]; intro
    simp only [eq_iff_true_of_subsingleton]

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
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j = 𝟙 s.pt
⊢ (adj.homEquiv s.pt F) s.π ≫ (adj.counit.app F).app j = s.π.app j

Tactic:
adj.homEquiv_unit,

Goal state after:
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
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j = 𝟙 s.pt
⊢ (adj.unit.app s.pt ≫ L.map s.π) ≫ (adj.counit.app F).app j = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ lift t ≫ s.π.app none = t.π.app none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)

Tactic:
· exact facbase t

Goal state after:
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

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

Tactic:
intro
    exact
      ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
          (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
          (IsIso.eq_inv_comp _).mpr e⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app j =
      (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
        (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app j

Tactic:
rintro (_ | (_ | _))

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app none =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app none

case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app (some WalkingPair.left) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app (some WalkingPair.right) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app j ≫
        (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
      (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app j

Tactic:
rintro (_ | (_ | _))

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app none ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app none

case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.left) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.right) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

Tactic:
apply Quiver.Hom.op

Goal state after:
case left
⊢ (match one with
    | zero => one
    | one => zero) ⟶
    match zero with
    | zero => one
    | one => zero
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case right
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

Tactic:
apply Quiver.Hom.op

Goal state after:
case right
⊢ (match one with
    | zero => one
    | one => zero) ⟶
    match zero with
    | zero => one
    | one => zero
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case id
X✝ : WalkingParallelPair
⊢ op
      (match X✝ with
      | zero => one
      | one => zero) ⟶
    op
      (match X✝ with
      | zero => one
      | one => zero)

Tactic:
apply Quiver.Hom.op

Goal state after:
case id
X✝ : WalkingParallelPair
⊢ (match X✝ with
    | zero => one
    | one => zero) ⟶
    match X✝ with
    | zero => one
    | one => zero
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✝ : Mono g
h : f ≫ g = 0
⊢ f = 0

Tactic:
← zero_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h✝ : f ≫ g = 0
h : f ≫ g = 0 ≫ ?m.28
⊢ f = 0

C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ C

C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ ?m.26 ⟶ Z
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso f
⊢ PreservesLimit (Functor.empty C) G

Tactic:
rw [Subsingleton.elim f (terminalComparison G)] at i
  exact PreservesTerminal.of_iso_comparison G

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✝ : Mono f
i : IsZero Y
⊢ IsZero X

Tactic:
obtain rfl := i.eq_zero_of_tgt f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X
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 Y : C
i : IsIso 0
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0

Tactic:
rw [← IsIso.hom_inv_id (0 : X ⟶ Y)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
i : IsIso 0
⊢ 0 ≫ inv 0 = 0 ∧ 𝟙 Y = 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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) ⋯

Tactic:
apply equalizer.hom_ext

Goal state after:
C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) =
    equalizer.lift (G.map h) ⋯ ≫ equalizer.ι (G.map f) (G.map g)
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasCoproduct f
b c : β
h : b ≠ c
⊢ ι f b ≫ π f c = 0

Tactic:
simp [Sigma.π, Function.update_of_ne 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✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : ?m.112 s ⟶ kernel (?m.117 s)
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯

Tactic:
apply equalizer.hom_ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : s.pt ⟶ kernel g
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m ≫ equalizer.ι g 0 = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯ ≫ equalizer.ι g 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ g ≫ f ≫ s.π = g ≫ 0 ≫ s.π

Tactic:
rw [← Category.assoc, ← hh, s.condition]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ 0 ≫ s.π = g ≫ 0 ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ ι f j✝ ≫ map p ≫ π g j✝¹ = ι f j✝ ≫ map' p ≫ π g j✝¹

Tactic:
simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
    ← Bicone.toCone_π_app_mk, ← Bicone.toCocone_ι_app_mk]

Goal state after:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ (bicone f).toCocone.ι.app { as := j✝ } ≫ (bicone f).toCone.π.app { as := j✝¹ } ≫ p j✝¹ =
    p j✝ ≫ (bicone g).toCocone.ι.app { as := j✝ } ≫ (bicone g).toCone.π.app { as := j✝¹ }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr

Tactic:
by
        have hₗ := h ⟨.left⟩
        have hᵣ := h ⟨.right⟩
        dsimp at hₗ hᵣ
        simpa [← hₗ, ← hᵣ] using m ≫= total.symm

Goal state after:
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✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ lift b.π ≫ desc b.ι = 𝟙 b.pt

Tactic:
rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ ((∀ (j : Fin n.succ), j < 0 → cons x₀ x j = cons y₀ y j) ∧ s (cons x₀ x 0) (cons y₀ y 0) ∨
      ∃ i, (∀ (j : Fin n.succ), j < i.succ → cons x₀ x j = cons y₀ y j) ∧ s (cons x₀ x i.succ) (cons y₀ y i.succ)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)

Tactic:
Fin.cons_succ,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ ((∀ (j : Fin n.succ), j < 0 → cons x₀ x j = cons y₀ y j) ∧ s (cons x₀ x 0) (cons y₀ y 0) ∨
      ∃ i, (∀ (j : Fin n.succ), j < i.succ → cons x₀ x j = cons y₀ y j) ∧ s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ (map (fun a ↦ count a ↑s) (↑s).dedup).sum = n

Tactic:
change ∑ a ∈ s.1.toFinset, count a s.1 = n

Goal state after:
n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ ∑ a ∈ (↑s).toFinset, count a ↑s = n
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ p.toFinsuppAntidiag ∈ (Finset.Icc 1 n).finsuppAntidiag n

Tactic:
suffices ∑ m ∈ Finset.Icc 1 n, Multiset.count m p.parts * m = n by simpa [toFinsuppAntidiag, hp]

Goal state after:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g :: l).prod

Tactic:
List.prod_cons

Goal state after:
case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ (c.reverse.append (single (k + 1) ⋯)).cast ⋯ ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
apply cast_heq

Goal state after: