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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (a : Fin (n + 1)) → ↥(s.sym (n - ↑a)) → Sym α (n - ↑(id a))

pp: case refine_3
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ s.sym (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine_2 i)

pp: case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id ?refine_2
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩

Tactic:
swap

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ s.sym (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine_2 i)

case refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (a : Fin (n + 1)) → ↥(s.sym (n - ↑a)) → Sym α (n - ↑(id a))

case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id ?refine_2
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case inl
α : Type ?u.3
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
simp [h]

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

Goal state before:
pp: case inr
α : Type ?u.3
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
simp [h]

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

Goal state before:
pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)

pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
swap

Goal state after:
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[], hy⟩)

pp: case cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
y : List α
hy : (head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨head✝ :: y, hy⟩)

Tactic:
· simp at hy

Goal state after:
case cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
y : List α
hy : (head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨head✝ :: y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
hy : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨[head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨[head✝], hy⟩)

pp: case cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
y : List α
hy : (head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨head✝¹ :: head✝ :: y, hy⟩)

Tactic:
· simp at hy

Goal state after:
case cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
y : List α
hy : (head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨head✝¹ :: head✝ :: y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

pp: case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)

Tactic:
swap

Goal state after:
case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)

case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝¹, head✝], hx⟩⟧) = ⟦⟨[head✝¹, head✝], hx⟩⟧

pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧

Tactic:
swap

Goal state after:
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧

case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝¹, head✝], hx⟩⟧) = ⟦⟨[head✝¹, head✝], hx⟩⟧
Module: Mathlib.Combinatorics.Quiver.Symmetric

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

Tactic:
simp [h]

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

Goal state before:
pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b c : V
p' : a ⟶ c
e : Path c b
h : (p'.toPath.comp e).length = e.length + 1
⊢ (p'.toPath.comp e).length ≠ 0

Tactic:
simp [h]

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

Goal state before:
pp: case cons
V : Type u₁
inst✝² : Quiver V
W : Type u₂
inst✝¹ : Quiver W
F : V ⥤q W
U : Type u₃
inst✝ : Quiver U
G : W ⥤q U
a b b✝ c✝ : V
x : Path a b✝
y : b✝ ⟶ c✝
h : (F ⋙q G).mapPath x = G.mapPath (F.mapPath x)
⊢ (F ⋙q G).mapPath (x.cons y) = G.mapPath (F.mapPath (x.cons y))

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : g = eqToHom ⋯ ≫ f
⊢ eqToHom p ≫ g = f

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

Tactic:
rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
    dsimp only [Functor.id_obj]
    rw [map_id, map_id]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α : Type u_1
p : Discrete α → Prop
⊢ (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }

Tactic:
rw [iff_iff_eq, discreteEquiv.forall_congr_left]
  simp only [discreteEquiv, Equiv.symm_mk, Equiv.coe_fn_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop Y).rightOpLeftOpIso.op.hom =
      (unop X).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f

Tactic:
intro F G η
        dsimp
        rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]
        congr 1
        cat_disch

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

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

Tactic:
simp [h]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
y : F.obj j
⊢ (⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f))) ((e j) y) =
    (⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm) ((e j) y)

Tactic:
apply (e j').injective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
y : F.obj j
⊢ (e j') ((⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f))) ((e j) y)) =
    (e j') ((⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm) ((e j) y))
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)

Tactic:
rw [assoc, assoc, ← Functor.comp_map, α.naturality_assoc, ← Functor.comp_map,
          ← β.naturality]

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f

Tactic:
rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: R S : GrpCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ (ConcreteCategory.hom i) r = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: R S : CommGrpCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ (ConcreteCategory.hom i) r = 1

Tactic:
simp [h]

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 : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : f = F.map g ≫ adj.counit.app B
⊢ adj.unit.app A ≫ G.map f = g

Tactic:
simp [h]

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 : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = adj.unit.app A ≫ G.map f
⊢ F.map g ≫ adj.counit.app B = f

Tactic:
simp [h]

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ h.homEquiv (h.homEquiv.symm { pt := s_pt, ι := s_ι }.ι) = s_ι

Tactic:
exact h.homEquiv.apply_symm_apply s_ι

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

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

Tactic:
refine Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))
  exact
    ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
      ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩

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

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝¹⁰ : Category.{w, u₂} D
E : Type u₃
inst✝⁹ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
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')
inst✝⁴ : HasBinaryProduct (G.obj (F.obj A✝)) (G.obj (F.obj B))
inst✝³ : HasBinaryProduct ((F ⋙ G).obj A✝) ((F ⋙ G).obj B)
inst✝² : HasBinaryProducts C
inst✝¹ : HasBinaryProducts D
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ prod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A)

Tactic:
refine { @asIso _ _ _ _ _ (?_) with hom := prodComparisonNatTrans F A }

Goal state after:
C : Type u
inst✝¹¹ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝¹⁰ : Category.{w, u₂} D
E : Type u₃
inst✝⁹ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
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')
inst✝⁴ : HasBinaryProduct (G.obj (F.obj A✝)) (G.obj (F.obj B))
inst✝³ : HasBinaryProduct ((F ⋙ G).obj A✝) ((F ⋙ G).obj B)
inst✝² : HasBinaryProducts C
inst✝¹ : HasBinaryProducts D
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ IsIso { app := fun B ↦ prodComparison F A B, naturality := ⋯ }
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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = ι ≫ g
w' : ι' ≫ f = ι' ≫ g
h : ι = ι'
⊢ (Iso.refl (Fork.ofι ι w).pt).hom ≫ (Fork.ofι ι' w').ι = (Fork.ofι ι w).ι

Tactic:
simp [h]

Goal state after:
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
P : C
π π' : Y ⟶ P
w : f ≫ π = g ≫ π
w' : f ≫ π' = g ≫ π'
h : π = π'
⊢ (Cofork.ofπ π w).π ≫ (Iso.refl (Cofork.ofπ π w).pt).hom = (Cofork.ofπ π' w').π

Tactic:
simp [h]

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ section_ f ≫ f = 0

Tactic:
simp [h]

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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImage f)
h : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = 0

Tactic:
simp [h]

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

Tactic:
simp [h]

Goal state after:
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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (G.mapCocone (F.mapCocone c))

Tactic:
apply isColimitOfPreserves (F ⋙ G) 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✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ e ≫ f = 0

Tactic:
by simp [h, he]

Goal state after: