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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (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 : ι
x : G i
ne : ⟦⟨i, x⟩⟧ ≠ 0
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (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
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]

Tactic:
rcases s with ⟨l⟩
  simpa using listSum_map (l := l) h

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

Goal state before:
pp: α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]

Tactic:
rcases s with ⟨l⟩
  simpa using listSum_map (l := l) h

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

Goal state before:
pp: case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α 0
⊢ m = ∅ → ∀ a ∈ m, a ∈ s

Tactic:
rintro rfl

Goal state after:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ a ∈ ∅, a ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
⊢ (s ∩ t).sym n = s.sym n ∩ t.sym n

Tactic:
ext m

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ (↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f'' = LinearMap.id

Tactic:
· ext x
    change (g <| (1 : S) • f x).down = _
    rw [one_smul, hg]
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
| (lift f ∘ map g) p

Tactic:
comp_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
| lift f (map g p)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mpr
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = s(x, y) → x ∈ z ∧ y ∈ z

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∈ s(x, y) ∧ y ∈ s(x, y)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case f
α : 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 β := ⋯
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
⊢ p = q → f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯

Tactic:
rintro rfl

Goal state after:
case f
α : 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 : α × α
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
hpq✝ : Rel α p p
hpq : p = p ∨ p = p.swap
Hq : ∀ a ∈ Quot.mk (Rel α) p, P a
⊢ f p.1 ⋯ = f p.1 ⋯ ∧ f p.2 ⋯ = f p.2 ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case g
α : 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 β := ⋯
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
⊢ p = q.swap → (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
rintro rfl

Goal state after:
case g
α : 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 ⋯)
q : α × α
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
hpq✝ : Rel α q.swap q
hpq : q.swap = q ∨ q.swap = q.swap
Hp : ∀ a ∈ s(q.swap.1, q.swap.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(q.swap.1, q.swap.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g q.swap) e H = g q.swap Hp
⊢ (f q.swap.1 ⋯, f q.swap.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
P : α → Prop
s : Sym2 α
h : ∀ a ∈ s, P a
⊢ map Subtype.val (pmap Subtype.mk s h) = s

Tactic:
cases s; rfl

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

Goal state before:
pp: α : Type u_1
s : Sym2 α
P : α → Prop
h : ∀ a ∈ s, P a
⊢ map Subtype.val (s.attachWith h) = s

Tactic:
cases s; rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
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'
x✝² : R'
x : R' ⊗[R] S
x✝¹ : R'
x✝ : S
⊢ ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝² • x✝¹ ⊗ₜ[R] x✝) =
    (RingHom.id R') x✝² •
      ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝¹ ⊗ₜ[R] x✝)

Tactic:
simp [equiv_tmul, Algebra.smul_def, mul_left_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
← inv_hom_id f,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso ((inv f ≫ f) ≫ g)
Module: Mathlib.CategoryTheory.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : (fun f ↦ ⇑(hom f)) f = (fun f ↦ ⇑(hom f)) g
⊢ f = g

Tactic:
← ofHom_hom f,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : (fun f ↦ ⇑(hom f)) f = (fun f ↦ ⇑(hom f)) g
⊢ ofHom (hom f) = g
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i

Tactic:
by
  ext X
  simp [← NatTrans.naturality]

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsRightAdjoint
iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
  G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G ≪≫ F.asEquivalence.inverse.associator F.asEquivalence.functor G
⊢ G.IsRightAdjoint

Tactic:
exact isRightAdjoint_of_iso iso.symm

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
h : (F ⋙ G).IsRightAdjoint
iso : F ≅ (F ⋙ G) ⋙ G.asEquivalence.inverse :=
  F.rightUnitor.symm ≪≫
    F.isoWhiskerLeft G.asEquivalence.unitIso ≪≫ (F.associator G.asEquivalence.functor G.asEquivalence.inverse).symm
⊢ F.IsRightAdjoint

Tactic:
exact isRightAdjoint_of_iso iso.symm

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

Goal state before:
pp: case mpr
X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
⊢ a = b → IsIso f

Tactic:
rintro rfl

Goal state after:
case mpr
X : Type u
inst✝ : PartialOrder X
a : X
f : a ⟶ a
⊢ IsIso f
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: case h
C : Cat
x : Quotient (isIsomorphicSetoid ↑C)
⊢ ∀ (a b : ↑C) (p : (isIsomorphicSetoid ↑C) a b), ⋯ = ⋯

pp: case f
C : Cat
x : Quotient (isIsomorphicSetoid ↑C)
⊢ ∀ (a : ↑C),
    (ConcreteCategory.hom (↾Quot.map (𝟙 C).toFunctor.obj ⋯)).toFun (Quot.mk (⇑(isIsomorphicSetoid ↑C)) a) =
      (ConcreteCategory.hom (𝟙 (Quotient (isIsomorphicSetoid ↑C)))).toFun (Quot.mk (⇑(isIsomorphicSetoid ↑C)) a)

Tactic:
all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: case h
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (isIsomorphicSetoid ↑C)
⊢ ∀ (a b : ↑C) (p : (isIsomorphicSetoid ↑C) a b), ⋯ = ⋯

pp: case f
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (isIsomorphicSetoid ↑C)
⊢ ∀ (a : ↑C),
    (ConcreteCategory.hom (↾Quot.map (f ≫ g).toFunctor.obj ⋯)).toFun (Quot.mk (⇑(isIsomorphicSetoid ↑C)) a) =
      (ConcreteCategory.hom (↾Quot.map f.toFunctor.obj ⋯ ≫ ↾Quot.map g.toFunctor.obj ⋯)).toFun
        (Quot.mk (⇑(isIsomorphicSetoid ↑C)) a)

Tactic:
all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
intro T

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
T : C
⊢ Function.Bijective fun x ↦ x ≫ f
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
coyonedaEquiv_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app Y)) (coyonedaEquiv (coyoneda.map g.op)) = (ConcreteCategory.hom (f.app Y)) g
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⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
intro T

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
T : C
⊢ Function.Bijective fun x ↦ f ≫ x
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✝ F G : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Epi (α.app j)
Z : C
u v : colimit G ⟶ Z
h : colimMap α ≫ u = colimMap α ≫ v
j : J
⊢ α.app j ≫ colimit.ι G j ≫ u = α.app j ≫ colimit.ι G j ≫ v

Tactic:
simpa using colimit.ι _ j ≫= h

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₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasProduct F.obj
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ limit F
h : x✝¹ ≫ Pi.lift (limit.π F) = x✝ ≫ Pi.lift (limit.π F)
⊢ x✝¹ = x✝

Tactic:
by
    refine limit.hom_ext fun j => ?_
    simpa using h =≫ Pi.π _ j

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 A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Tactic:
by
  rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]

Goal state after:
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:
by
    cases f <;> apply Quiver.Hom.op
    exacts [left, right, WalkingParallelPairHom.id _]

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:
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 f
⊢ pushout.inl f g ≫ inv (pushout.inr f g) = inv f ≫ g

Tactic:
rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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:
simp [← s.condition]

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

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

Tactic:
cases i <;> cases j <;> cases g

Goal state after:
case op.op.zero.zero.id
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero))))

case op.op.one.zero.left
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op left)

case op.op.one.zero.right
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op right)

case op.op.one.one.id
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one)))) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one))))
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map left ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map right ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ WalkingParallelPair.casesOn X✝ p q =
    WalkingParallelPair.casesOn X✝ p q ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
all_goals cat_disch

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

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map left ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map right ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ p q).hom =
    (WalkingParallelPair.casesOn X✝ p q).hom ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
all_goals cat_disch

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

Goal state before:
pp: case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F

Tactic:
refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }

Goal state after:
case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), G.map f ≫ ⋯.from_ (G.obj Y) = ⋯.from_ (G.obj X) ≫ F.map f
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
⊢ ∀ (a b : PreservesLimit K F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

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
a b : ∀ {c : Cone K} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
⊢ ⋯ = ⋯
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
⊢ ∀ (a b : PreservesColimit K F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

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
a b : ∀ {c : Cocone K} (hc : IsColimit c), Nonempty (IsColimit (F.mapCocone c))
⊢ ⋯ = ⋯
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 : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : PreservesLimitsOfShape J F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

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 : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : ∀ {K : J ⥤ C}, PreservesLimit K F
⊢ ⋯ = ⋯
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 : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : PreservesColimitsOfShape J F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

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 : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : ∀ {K : J ⥤ C}, PreservesColimit K F
⊢ ⋯ = ⋯
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 : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

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 : J ⥤ C
F : C ⥤ D
a b : ∀ {J : Type w} [inst : Category.{w', w} J], PreservesLimitsOfShape J F
⊢ ⋯ = ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero

Tactic:
have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
    apply J.comp_zero (I.zero X Y).zero Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
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 : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

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 : J ⥤ C
F : C ⥤ D
a b : ∀ {J : Type w} [inst : Category.{w', w} J], PreservesColimitsOfShape J F
⊢ ⋯ = ⋯