mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h✝ : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ∀ (x : F j),
    (↑⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ?k ⟨↑⟨k, hk⟩, ?hl⟩) (f h x) =
      piLTProj h (((piLTLim hi).symm ⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ⟨j, hj⟩) x)

pp: case k
ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h✝ : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ↑(Iio i)

pp: case hl
ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h✝ : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ↑⟨k, hk⟩ < ↑?k

Tactic:
exacts [(e _).nat _ _ _, h.trans_lt (hi.mid _).2.1]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharZero R
x y : ℕ
hxy : ↑x = ↑y
⊢ x = y

Tactic:
by rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
G : Type u_6
inst✝¹ : DistribSMul G M
inst✝ : SMulCommClass G ℚ≥0 M
a : G
s : Finset ι
f : ι → M
⊢ a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i

Tactic:
by
  simp only [expect, smul_sum, smul_comm]

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ [], f x ≡ g x [MOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [MOD n]

Tactic:
aesop (add unsafe ModEq.mul)

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [MOD n]) → (List.map f tail✝).prod ≡ (List.map g tail✝).prod [MOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [MOD n]
⊢ (List.map f (head✝ :: tail✝)).prod ≡ (List.map g (head✝ :: tail✝)).prod [MOD n]

Tactic:
aesop (add unsafe ModEq.mul)

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

Goal state before:
pp: case nil
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ [], f x ≡ g x [ZMOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]

Tactic:
aesop (add unsafe ModEq.mul)

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

Goal state before:
pp: case cons
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [ZMOD n]) → (List.map f tail✝).prod ≡ (List.map g tail✝).prod [ZMOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [ZMOD n]
⊢ (List.map f (head✝ :: tail✝)).prod ≡ (List.map g (head✝ :: tail✝)).prod [ZMOD n]

Tactic:
aesop (add unsafe ModEq.mul)

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2.Nonempty ↔ s.Nonempty

Tactic:
contrapose!

Goal state after:
α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ a ::ₛ m
⊢ b ∈ s

Tactic:
rw [Sym.mem_cons] at hb

Goal state after:
case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Tactic:
contrapose!

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : (b : β) × ↑(fromRel ⋯)
⊢ (fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯)
      ((fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩) z) =
    z

Tactic:
by
    rcases z with ⟨b, ⟨⟨a₁, rfl⟩, ⟨a₂, ha₂⟩⟩, h⟩
    rfl

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

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z → X = Z ∨ Y = Z

Tactic:
rintro ⟨_ | _⟩ <;> tauto

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
h : p₁.comp q₁ = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁ = q₂

Tactic:
induction q₁ with

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

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ (a✝¹.cons a✝).reverse.reverse = a✝¹.cons a✝

Tactic:
rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
    rfl

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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ X✝.map (f.app x✝) ≫ τ.app (Y.obj x✝) = τ.app (X.obj x✝) ≫ Y✝.map (f.app x✝)

Tactic:
← NatTrans.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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ X✝.map (f.app x✝) ≫ τ.app (Y.obj x✝) = X✝.map (f.app x✝) ≫ τ.app (Y.obj x✝)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (𝟙 Y).op = 𝟙 (op Y)

Tactic:
op_id

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ 𝟙 (op Y) = 𝟙 (op Y)
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
⊢ IsIso f

Tactic:
have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h✝ : ⋯ = ⋯
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e_8
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ coconeOfHom h m = s

Tactic:
rw [coconeOfHom_fac]

Goal state after:
case e_8
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ (colimitCocone h).extend m = s
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Tactic:
by rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
this : ∀ {X : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f
⊢ e = e'

Tactic:
obtain ⟨e, he⟩ := e

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e' : F.RepresentableBy Y
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
this : ∀ {X : C} (f : X ⟶ Y), { homEquiv := e, homEquiv_comp := he }.homEquiv f = e'.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = e'
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e e' : F.CorepresentableBy X
h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
this : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f
⊢ e = e'

Tactic:
obtain ⟨e, he⟩ := e

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e' : F.CorepresentableBy X
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
this : ∀ {Y : C} (f : X ⟶ Y), { homEquiv := e, homEquiv_comp := he }.homEquiv f = e'.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = e'
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj (unop X) ⟶ F
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) (yonedaEquiv u)) =
    yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ f ≫ x

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩
  intro T
  rw [bijective_iff_isIso_ofHom]
  exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c d : Cone F
f : c ≅ d
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt

Tactic:
by
  simp [← Cone.category_comp_hom]

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c d : Cone F
f : c ≅ d
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt

Tactic:
by
  simp [← Cone.category_comp_hom]

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

Goal state before:
pp: case right
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 := right } = t.π.app { as := right }

Tactic:
exact hl₂ _ _

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 : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app none = s.π.app none

Tactic:
rw [← s.w inl, ← t.w inl, ← Category.assoc]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

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

Tactic:
cases f <;> apply Quiver.Hom.op

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

case right
⊢ (match one with
    | zero => one
    | one => zero) ⟶
    match zero with
    | zero => one
    | one => zero

case id
X✝ : WalkingParallelPair
⊢ (match X✝ with
    | zero => one
    | one => zero) ⟶
    match X✝ with
    | zero => one
    | one => zero
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
        pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
      pullback.snd f prod.fst =
    𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst

Tactic:
apply prod.hom_ext <;> simp [pullback.condition]

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

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
        pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
      pullback.fst prod.snd f =
    𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f

Tactic:
apply prod.hom_ext <;> simp [pullback.condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
s : PushoutCocone f g
⊢ (pushoutCoconeOfLeftIso f g).inl ≫ s.inr = s.inl ∧
    (pushoutCoconeOfLeftIso f g).inr ≫ s.inr = s.inr ∧
      ∀ {m : (pushoutCoconeOfLeftIso f g).pt ⟶ s.pt},
        (pushoutCoconeOfLeftIso f g).inl ≫ m = s.inl → (pushoutCoconeOfLeftIso f g).inr ≫ m = s.inr → m = s.inr

Tactic:
by simp [← s.condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
s : PushoutCocone f g
⊢ (pushoutCoconeOfRightIso f g).inl ≫ s.inl = s.inl ∧
    (pushoutCoconeOfRightIso f g).inr ≫ s.inl = s.inr ∧
      ∀ {m : (pushoutCoconeOfRightIso f g).pt ⟶ s.pt},
        (pushoutCoconeOfRightIso f g).inl ≫ m = s.inl → (pushoutCoconeOfRightIso f g).inr ≫ m = s.inr → m = s.inl

Tactic:
by simp [← s.condition]

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 : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
⊢ f ≫ s.inl = h ≫ y ≫ s.inr

Tactic:
reassoc₂,

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 : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
⊢ f ≫ s.inl = g ≫ s.inr
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cone.postcompose h.inv).obj c)
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))

Tactic:
apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cone.postcompose h.inv).obj c)
⊢ F.mapCone ((Cone.postcompose h.inv).obj c) ≅ (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c)
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g

Tactic:
← sub_eq_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ f - Fork.ι c ≫ g = 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
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c

Tactic:
← sub_eq_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c - g ≫ Cofork.π c = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)

Tactic:
exact {Hom.id j}

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

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

Tactic:
by
  intro m₁ m₂ h
  apply CancelMonoid.ext
  exact congrArg (fun m : Monoid M => (letI := m; HMul.hMul : M → M → M)) <|
    congrArg (@RightCancelMonoid.toMonoid M) 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:
rw [Fork.condition, HasZeroMorphisms.comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.fst = prod.fst

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.snd = prod.snd

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
  simp

Goal state after:
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
P : C
g : (j : J) → f j ⟶ P
⊢ IsColimit (G.mapCocone (Cofan.mk P g)) ≃ IsColimit (Cofan.mk (G.obj P) fun j ↦ G.map (g j))

Tactic:
by
  refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
  · refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
  refine Cocone.ext (Iso.refl _) fun j => by dsimp; cases j; simp

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
F : J → C
B : Bicone F
j j' : J
h : j ≠ j'
⊢ B.ι j ≫ B.π j' = 0

Tactic:
simpa [h] using B.ι_π j j'

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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
X✝ Y✝ : Bicone F
f : X✝ ⟶ Y✝
j : J
⊢ G.map f.hom ≫ { pt := G.obj Y✝.pt, π := fun j ↦ G.map (Y✝.π j), ι := fun j ↦ G.map (Y✝.ι j), ι_π := ⋯ }.π j =
    { pt := G.obj X✝.pt, π := fun j ↦ G.map (X✝.π j), ι := fun j ↦ G.map (X✝.ι j), ι_π := ⋯ }.π j

Tactic:
by simp [-BiconeMorphism.wπ, ← f.wπ j]

Goal state after:
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 : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ fromSubtype f p ≫ π f ↑j = π (Subtype.restrict p f) j

Tactic:
classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasCoproduct f
⊢ HasBiproduct f

Tactic:
cases nonempty_fintype J
  exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

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

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
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono (map f g)

Tactic:
rw [show biprod.map f g = (biprod.isoProd _ _).hom ≫ prod.map f g ≫
    (biprod.isoProd _ _).inv by aesop]

Goal state after:
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
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono ((isoProd W X).hom ≫ prod.map f g ≫ (isoProd Y Z).inv)