mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
i : α
⊢ ∀ (x : β) (x_1 : x ∈ d), ⋯.choose = i → i ∈ s

Tactic:
e

Goal state after:
case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
i : α
e : β
⊢ ∀ (x : e ∈ d), ⋯.choose = i → i ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs
⊢ map (fun p ↦ x ::ₛ p) [Sym.nil] ++ List.sym (0 + 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs

Tactic:
map_singleton,

Goal state after:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs
⊢ [x ::ₛ Sym.nil] ++ List.sym (0 + 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f ≍ f'

Tactic:
e

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f' ≍ f'
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d : α
⊢ ∀ (d_1 : α) (h : Rel α (b, c) (d, d_1)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = d then d_1 else d

Tactic:
e

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
⊢ ∀ (h : Rel α (b, c) (d, e)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = d then e else d
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a

Tactic:
other_eq_other'

Goal state after:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
⊢ f s' = g s' → f (s • s') = g (s • s')

Tactic:
e

Goal state after:
case refine_3
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'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f (s • s') = g (s • s')
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * f s' = g ((algebraMap S S') s) * g s'

Tactic:
e

Goal state after:
case refine_3
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'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * g s' = g ((algebraMap S S') s) * g s'
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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'
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
⊢ ∀ (x : S ⊗[R] M), ↑(cancelBaseChangeAux R S A B M).symm (s • x) = s • ↑(cancelBaseChangeAux R S A B M).symm x

Tactic:
x

Goal state after:
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'
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
x : S ⊗[R] M
⊢ ↑(cancelBaseChangeAux R S A B M).symm (s • x) = s • ↑(cancelBaseChangeAux R S A B M).symm x
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₁ F₂ : C ⥤ D
⊢ ∀ (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.map f)

Tactic:
e

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
e : F₁ ≅ F₂
⊢ IsIso (F₁.map f) → IsIso (F₂.map f)
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝

Tactic:
by rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]

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

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
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
⊢ F.Full

Tactic:
have := Full.of_iso h.symm
  exact Full.of_comp_faithful F G

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
h : X.as = Y.as
⊢ F X.as ⟶ F Y.as

Tactic:
exact eqToHom (congrArg _ h)

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

Goal state before:
pp: case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ IsIso f

Tactic:
exact ⟨fun i => inv (f i), by cat_disch, by cat_disch⟩

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ⊤ f

Tactic:
simp only [top_eq]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
⊢ Monotone fun x ↦ x.map F

Tactic:
by
  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

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

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

Tactic:
obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
f : Arrow C
hf : f ∈ P.toSet
⊢ P (P.homFamily ⟨f, hf⟩)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type u_3
ι : α → Type u_4
A B : (a : α) → ι a → C
f✝¹ : (a : α) → (i : ι a) → A a i ⟶ B a i
f Y✝ : C
f✝ : f ⟶ Y✝
⊢ (⨆ a, ofHoms (f✝¹ a)) f✝ ↔ ofHoms (fun j ↦ f✝¹ j.fst j.snd) f✝

Tactic:
simp [ofHoms_iff]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone isoClosure

Tactic:
by
  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

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

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

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

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 G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : ∃ hX hY, F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
⊢ Function.Injective f

Tactic:
x

Goal state after:
case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
x : X
⊢ ∀ ⦃a₂ : X⦄, f x = f a₂ → x = a₂
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
⊢ ∀ (x : F ≅ G), P.map F ≤ P.map G

Tactic:
e

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
⊢ P.map F ≤ P.map G
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

Tactic:
e

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ ∀ (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
e

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
⊢ ∀ (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)

Tactic:
e

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ ∀ (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)

Tactic:
e

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
⊢ ∀ (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

Tactic:
e

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ ∀ (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)

Tactic:
e

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
⊢ ∀ (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ g₁ = g₂

Tactic:
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by cat_disch
  have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
  apply asHom_injective t1

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).homEquiv x✝² x✝¹) x✝ = (adj.homEquiv x✝² x✝¹) x✝

Tactic:
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.homEquiv x✝² x✝¹) x✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
η : yoneda.obj X ⟶ F
⊢ (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ })
      ((fun η ↦ (ConcreteCategory.hom (η.app (op X))) (𝟙 X)) η) =
    η

Tactic:
ext Y f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
η : yoneda.obj X ⟶ F
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ })
                ((fun η ↦ (ConcreteCategory.hom (η.app (op X))) (𝟙 X)) η)).app
            Y)).toFun
      f =
    (ConcreteCategory.hom (η.app Y)).toFun f
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✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprod.desc (F.map coprod.inl) (F.map coprod.inr) ≫ F.map (coprod.map f g) =
    coprod.map (F.map f) (F.map g) ≫ coprod.desc (F.map coprod.inl) (F.map coprod.inr)

Tactic:
coprod.map_desc,

Goal state after:
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✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprod.desc (F.map coprod.inl) (F.map coprod.inr) ≫ F.map (coprod.map f g) =
    coprod.desc (F.map f ≫ F.map coprod.inl) (F.map g ≫ F.map coprod.inr)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k : X✝ ⟶ Y✝
g : Over A
⊢ coprod.map (Hom.left k) (𝟙 g.left) ≫ coprod.desc Y✝.hom g.hom = coprod.desc X✝.hom g.hom

Tactic:
coprod.map_desc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k : X✝ ⟶ Y✝
g : Over A
⊢ coprod.desc (Hom.left k ≫ Y✝.hom) (𝟙 g.left ≫ g.hom) = coprod.desc X✝.hom g.hom
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ data.mapZ (Arrow.homMk (f.left.map (x✝¹ ≫ x✝)) (f.right.map (x✝¹ ≫ x✝)) ⋯) =
    data.mapZ (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯) ≫
      data.mapZ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯)

Tactic:
rw [← data.mapZ_comp]
        congr <;> simp

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default

Tactic:
← cancel_mono e.hom

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom
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✝ : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfShape J F

Tactic:
exact reflectsColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

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✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m = ∑ j, s.π.app { as := j } ≫ b.ι j

Tactic:
rw [← Category.comp_id m]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m ≫ 𝟙 b.toCone.pt = ∑ j, s.π.app { as := j } ≫ b.ι 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
hₗ : m ≫ b.toCone.π.app { as := WalkingPair.left } = s.π.app { as := WalkingPair.left }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr

Tactic:
have hᵣ := h ⟨.right⟩

Goal state after:
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
hₗ : m ≫ b.toCone.π.app { as := WalkingPair.left } = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.toCone.π.app { as := WalkingPair.right } = s.π.app { as := WalkingPair.right }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr
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 : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.toCocone.ι.app { as := WalkingPair.left } ≫ m = s.ι.app { as := WalkingPair.left }
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s

Tactic:
have hᵣ := h ⟨.right⟩

Goal state after:
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 : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.toCocone.ι.app { as := WalkingPair.left } ≫ m = s.ι.app { as := WalkingPair.left }
hᵣ : b.toCocone.ι.app { as := WalkingPair.right } ≫ m = s.ι.app { as := WalkingPair.right }
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
have h₁' : ((m : T ⟶ b.pt) - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0 := by
        simpa using sub_eq_zero.2 h₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ m = f ≫ b.inl + g ≫ b.inr