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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
      [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
refine ⟨fun _ ↦ lTensor_exact _, fun H ↦ iff_lTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ L hL ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝³ : AddCommGroup N'
x✝² : AddCommGroup N''
x✝¹ : Module R N'
x✝ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x : M ⊗[R] N'
hx : (lTensor M L) x = 0
⊢ x ∈ ⊥
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: ι : Type u_1
H : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup G
inst✝⁴ : Module ℚ≥0 G
inst✝³ : AddCommGroup H
inst✝² : Module ℚ≥0 H
inst✝¹ : FunLike F G H
inst✝ : LinearMapClass F ℚ≥0 G H
g : F
f : ι → G
a : ι
⊢ g (balance f a) = balance (⇑g ∘ f) a

Tactic:
simp [balance, map_expect]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype β
s : Finset α
t : α → Finset β
h : (↑s).PairwiseDisjoint t
⊢ (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens

Tactic:
by
  simp [dens, sum_div]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂

Tactic:
apply h.equiv.injective
  refine (h.equiv.apply_symm_apply _).trans ?_
  simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) x✝ + (TensorProduct.lift f) y✝)

Tactic:
apply add <;> assumption

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ ∀ x ∈ s, x ∉ t → Nat.card { a // f a = x } = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ ∀ b ∈ ↑t, (f ⁻¹' {b}).Finite

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ m ∈ s

Tactic:
aesop

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

Goal state before:
pp: case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ a ∈ x :: xs

Tactic:
rw [mem_cons]

Goal state after:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
⊢ (insert a s).sym2 = image (fun b ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
simpa [map_eq_image] using! sym2_cons a s ha

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

Goal state before:
pp: α : Type u_1
xs : List α
⊢ List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs

Tactic:
induction xs with
  | nil => simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]
  | cons x xs ih =>
    rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]

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

Goal state before:
pp: case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α)) (x :: xs).sym2 = List.sym 2 (x :: xs)

Tactic:
rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]

Goal state after:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α) ∘ fun y ↦ s(x, y)) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p ↦ x ::ₛ p) ∘ fun x ↦ x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2
Module: Mathlib.Algebra.BigOperators.Sym

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∀ (i : { p // p.1 ≤ p.2 }),
    i ∈ Finset.subtype (fun i ↦ i.1 ≤ i.2) s.offDiag ↔ Sym2.sortEquiv.symm i ∈ {i ∈ s.sym2 | ¬i.IsDiag}

Tactic:
aesop

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∀ i ∈ Finset.subtype (fun i ↦ i.1 ≤ i.2) s.offDiag, p s((↑i).1, (↑i).2) = p (Sym2.sortEquiv.symm i)

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)

Tactic:
by
  rw [Finset.offDiag_filter_lt_eq_filter_le]
  conv_rhs => rw [← Finset.sum_subtype_eq_sum_filter]
  refine (Finset.sum_equiv Sym2.sortEquiv.symm ?_ ?_).symm
  all_goals aesop

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

Goal state before:
pp: case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Tactic:
rw [mem_cons]

Goal state after:
case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ y✝ : α
⊢ map g (map f s(x✝, y✝)) = map (g ∘ f) s(x✝, y✝)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c

Tactic:
aesop

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

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : True ∨ x = y ↔ x = x' ∨ x = y'
hy : y = x ∨ True ↔ y = x' ∨ y = y'
hx' : x' = x ∨ x' = y ↔ True ∨ x' = y'
hy' : y' = x ∨ y' = y ↔ y' = x' ∨ True
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
aesop

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

Goal state before:
pp: case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ (x = x✝ ∨ x = y✝) ∧ (y = x✝ ∨ y = y✝) → s(x✝, y✝) = s(x, y)

Tactic:
aesop

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
b : β
x✝ y✝ : α
⊢ b ∈ map f s(x✝, y✝) ↔ ∃ a ∈ s(x✝, y✝), f a = b

Tactic:
aesop

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

Goal state before:
pp: α : 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 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
⊢ Eq.ndrec (motive := fun x ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq

Tactic:
refine h.trans (Quot.sound ?_)

Goal state after:
α : 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 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
⊢ Rel β (f p.1 ⋯, f p.2 ⋯) (f q.1 ⋯, f q.2 ⋯)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
b : β
x y : α
h : ∀ a ∈ Quot.mk (Rel α) (x, y), P a
⊢ b ∈ s(f x ⋯, f y ⋯) ↔ ∃ a, ∃ (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
h : ∀ a ∈ z, P a
b : β
⊢ b ∈ pmap f z h ↔ ∃ a, ∃ (ha : a ∈ z), b = f a ⋯

Tactic:
obtain ⟨x, y⟩ := z
  rw [pmap_pair f x y h]
  aesop

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : ∀ (a : α), ¬r a a
⊢ ∀ (x y : α), s(x, y) ∈ fromRel sym → ¬s(x, y).IsDiag

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X Z✝ : C
g h : X ⟶ Z✝
w : 𝟙 X ≫ g = 𝟙 X ≫ h
⊢ g = h

Tactic:
aesop

Goal state after:
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 e : α
h : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
this :
  ∀ {f : Sym2 α} {g : s(b, c) = f} {h : a ∈ f},
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) g h = if a = b then c else b
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ hy = if a = d then e else d

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ {x ∈ image (uncurry Sym2.mk) (s ×ˢ s) | x.IsDiag} = image (uncurry Sym2.mk) s.diag

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ {x ∈ image (uncurry Sym2.mk) (s ×ˢ s) | ¬x.IsDiag} = image (uncurry Sym2.mk) s.offDiag

Tactic:
aesop

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

Goal state before:
pp: case mk
α : Type u_1
s : Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ s.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ uncurry Sym2.mk '' s ×ˢ s

Tactic:
aesop

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

Goal state before:
pp: case mk
α : Type u_1
a : α
s : Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (insert a s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ (fun b ↦ s(a, b)) '' insert a s ∪ s.sym2

Tactic:
aesop

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj' : C → D
map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj', map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj', map := map', map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
obtain rfl : obj = obj' := congr_arg Prefunctor.obj h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (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) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj, map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj, map := map', map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P Q : ObjectProperty C
h : P ≤ Q
F : C ⥤ D
⊢ P.map F ≤ Q.map F

Tactic:
rintro X ⟨Y, hY, ⟨e⟩⟩

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P Q : ObjectProperty C
h : P ≤ Q
F : C ⥤ D
X : D
Y : C
hY : P Y
e : F.obj Y ≅ X
⊢ Q.map F X
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF h₂ : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
⊢ { preimage := f₁, map_preimage := hf₁, preimage_map := preimage_map✝ } = h₂

Tactic:
cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

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

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
v w : V
p q : Path v w
a✝² x✝³ : V
x✝² : Path a✝² x✝³
b✝ : V
a✝¹ : Path a✝² b✝
a✝ : b✝ ⟶ x✝³
x✝¹ x✝ : BoundedPaths a✝² x✝³ 0
hp : x✝².length ≤ 0
hq : (a✝¹.cons a✝).length ≤ 0
⊢ ⟨x✝², hp⟩ = ⟨a✝¹.cons a✝, hq⟩

Tactic:
by simp [Quiver.Path.length] at hq

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
h : P.isoClosure = P
⊢ P.IsClosedUnderIsomorphisms

Tactic:
by rw [← h]; infer_instance

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.map F ≤ (P.strictMap F).isoClosure

Tactic:
rintro X ⟨Y, hY, ⟨e⟩⟩

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : D
Y : C
hY : P Y
e : F.obj Y ≅ X
⊢ (P.strictMap F).isoClosure X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯

Tactic:
by
  subst h
  simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
x✝ : Fun X Y
⊢ ∀ ⦃a₂ : Fun X Y⦄, (fun f x ↦ f.toFun x) x✝ = (fun f x ↦ f.toFun x) a₂ → x✝ = a₂

Tactic:
aesop

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
P : MorphismProperty C
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.map F).inverseImage F = P

Tactic:
by
  erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]

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

Goal state before:
pp: α : Type u
⊢ Iso.toEquiv 1 = 1

Tactic:
aesop

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

Goal state before:
pp: α : Type u
⊢ ∀ (x y : Aut α), Iso.toEquiv (x * y) = Iso.toEquiv x * Iso.toEquiv y

Tactic:
aesop

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

Goal state before:
pp: α : Type u
⊢ Equiv.toIso 1 = 1

Tactic:
aesop

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

Goal state before:
pp: α : Type u
⊢ ∀ (x y : Equiv.Perm α), Equiv.toIso (x * y) = Equiv.toIso x * Equiv.toIso y

Tactic:
aesop

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

Goal state before:
pp: X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget SemiRingCat).map f)

Goal state after:
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
unit✝¹ : 𝟭 C ⟶ F ⋙ G
counit✝¹ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝¹ : ∀ (X : C), F.map (unit✝¹.app X) ≫ counit✝¹.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝¹ : ∀ (Y : D), unit✝¹.app (G.obj Y) ≫ G.map (counit✝¹.app Y) = 𝟙 (G.obj Y)
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.unit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit
h' :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.counit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit
⊢ { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
      right_triangle_components := right_triangle_components✝¹ } =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ }

Tactic:
aesop

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
t : Cone F
h : IsLimit t
W W' : C
f : (const J).obj W ⟶ F
g : W' ⟶ W
⊢ h.homEquiv (h.homEquiv.symm ((const J).map g ≫ f)) = h.homEquiv (g ≫ h.homEquiv.symm f)

Tactic:
aesop

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y'))) ≫ g'

Tactic:
he'' e he,

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (e (G_obj Y) Y').symm ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ 𝟙 (G_obj Y')) ≫ g'
Module: Mathlib.CategoryTheory.Thin

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
x✝¹ x✝ : D ⥤ C
α β : x✝¹ ⟶ x✝
⊢ α.app = β.app

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

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✝ : C
⊢ { hom := (fromSkeletonToSkeletonIso x✝).hom ≫ 𝟙 x✝ ≫ (fromSkeletonToSkeletonIso x✝).inv } = 𝟙 (toSkeleton x✝)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : LocallySmall.{w, v', u'} A
C : Type w
inst✝ : SmallCategory C
P Q : C ⥤ A
f g : P ⟶ Q
h : f.app = g.app
⊢ f = g

Tactic:
aesop

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono ((adj.homEquiv X Y).symm ((adj.homEquiv X Y) f))
inst✝ : F.ReflectsMonomorphisms
⊢ Mono (F.map ((adj.homEquiv X Y) f))

Tactic:
exact mono_of_mono_fac (adj.homEquiv_counit _ _ _).symm

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi f

Tactic:
rw [StrongEpi.iff_of_arrow_iso e]

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g = lift (g ≫ base arrows) (fun j ↦ g ≫ π arrows j) ⋯

Tactic:
aesop

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
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ ∀ (s : Fan K.obj) (j : J),
    hc.lift { pt := s.pt, π := { app := fun j ↦ s.proj j, naturality := ⋯ } } ≫ (Fan.mk c.pt c.π.app).proj j = s.proj j

Tactic:
by subsingleton

Goal state after: