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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
let π : N' →ₗ[R] N' ⧸ LinearMap.range f := Submodule.mkQ _
  let ι : N' ⧸ LinearMap.range f →ₗ[R] N'' :=
    Submodule.subtype _ ∘ₗ (LinearMap.quotKerEquivRange g).toLinearMap ∘ₗ
      Submodule.quotEquivOfEq (LinearMap.range f) (LinearMap.ker g)
        (LinearMap.exact_iff.mp exact).symm
  suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M) by
    rw [show g = ι.comp π from rfl, lTensor_comp]
    exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)
  exact _root_.lTensor_exact _ (fun x ↦ by simp [π]) Quotient.mk''_surjective

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
inst✝⁶ : Module.Flat R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
reg : IsSMulRegular M x
⊢ IsSMulRegular N ((algebraMap R S) x)

Tactic:
by
  have h := hf.map_id_injective_of_flat_left hf (LinearMap.lsmul R M x) reg
  rwa [hf.map_id_lsmul_eq_lsmul_algebraMap] at h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (t ∪ s).dens = (t \ s).dens + t.dens

Tactic:
← dens_sdiff_add_dens,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (t \ s).dens + s.dens = (t \ s).dens + t.dens
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✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ (map₀ f fun i ↦ (algebraMap R (G i)) r) * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧ * map₀ f fun i ↦ (algebraMap R (G i)) r

Tactic:
rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ ↑(max a b + 1 - min a b).toNat = ↑((b - a).natAbs + 1)

Tactic:
Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max),

Goal state after:
a b : ℤ
⊢ max a b + 1 - min a b = ↑((b - a).natAbs + 1)
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n

Tactic:
refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)

Goal state after:
case inr.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)
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
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : Function.Bijective ⇑(TensorProduct.lift f)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective ⇑(TensorProduct.lift ((f ∘ₗ ↑e₁).compl₂ ↑e₂))

Tactic:
rw [← TensorProduct.lift_comp_map, ← LinearMap.rTensor_comp_lTensor]

Goal state after:
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
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : Function.Bijective ⇑(TensorProduct.lift f)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective ⇑(TensorProduct.lift f ∘ₗ LinearMap.rTensor M₂ ↑e₁ ∘ₗ LinearMap.lTensor N₁ ↑e₂)
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
⊢ Nat.card ↑(f ⁻¹' ↑t) = ∑ b ∈ t, Nat.card ↑{a | f a = b}

Tactic:
have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)

Goal state after:
ι : 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
⊢ Nat.card ↑(f ⁻¹' ↑t) = ∑ b ∈ t, Nat.card ↑{a | f a = b}
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ x ∈ Ico 0 n, f x • g x =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x

Tactic:
sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn),

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ f (n - 1) • ∑ i ∈ range n, g i - f 0 • ∑ i ∈ range 0, g i -
      ∑ i ∈ Ico 0 (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Tactic:
by
  induction xs with
  | nil => simp at ha
  | cons x xs ih =>
    rw [mem_sym2_cons_iff]
    grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup

Tactic:
← Multiset.dedup_sym2,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).sym2.dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective fun p ↦ x ::ₛ p

Tactic:
intro z z'

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z z' : Sym α n
⊢ (fun p ↦ x ::ₛ p) z = (fun p ↦ x ::ₛ p) z' → z = z'
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
⊢ Injective (map f)

Tactic:
intro z z'

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a b₁✝ b₁ : α
h : b₁✝ = b₁ ∨ a = b₁ ∧ b₁✝ = a
⊢ b₁✝ = b₁

Tactic:
obtain rfl | ⟨rfl, rfl⟩ := h <;> rfl

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

Goal state before:
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:
exfalso
          simp at hy

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)
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

Tactic:
subst g

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)
hy : a ∈ s(d, e)
h : a ∈ s(b, c)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ h = if a = b then c else b
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ p₁.comp q₁ ≍ p₁.comp q₁ ∧ f₁ ≍ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₁ = q₁.cons f₂

Tactic:
rw [h.2.2.eq]

Goal state after:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ p₁.comp q₁ ≍ p₁.comp q₁ ∧ f₁ ≍ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X

pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
· rintro X
    rfl

Goal state after:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
Module: Mathlib.Combinatorics.Quiver.Path

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

Tactic:
rintro ⟨c, p', e, rfl, h⟩

Goal state after:
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
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X

pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))

Tactic:
· rintro X
    rfl

Goal state after:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))
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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
Functor.hext hobj fun _ _ => hmap

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ G.map (f ≫ g) ≍ G.map (f ≫ g)
Module: Mathlib.CategoryTheory.EqToHom

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 G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f

Tactic:
Functor.hext hobj fun _ _ => hmap

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ (G ⋙ H).map f ≍ (G ⋙ H).map f
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: 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) ≫
      e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 2 3 =>
    rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]

Goal state after:
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) ≫ e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj Y)) ≫ e.unitInv.app (e.inverse.obj Y) =
    𝟙 (e.inverse.obj Y)
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
P Q : MorphismProperty C
h : P ≤ Q
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q.map F f

Tactic:
exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ Q.isoClosure f

Tactic:
exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

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
F G : C ⥤ D
e : F ≅ G
⊢ P.map F = P.map G

Tactic:
revert F G e
  suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
    fun F G e => le_antisymm (this e) (this e.symm)
  intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩
  exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ Arrow.mk (E.inverse.map (E.functor.map f)) ≅ Arrow.mk f

Tactic:
exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)

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 adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj = adj'

Tactic:
by
  suffices h' : adj.counit = adj'.counit by cases adj; cases adj'; aesop
  ext X
  apply (adj.homEquiv _ _).injective
  rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]

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

Goal state before:
pp: case mk
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
X : C
h : F.cones.RepresentableBy X
j : J
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
h₁ : { pt := pt✝, π := π✝ }.pt = pt✝
h₂ : (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π = π✝
⊢ homOfCone h { pt := pt✝, π := π✝ } ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j

Tactic:
conv_rhs => rw [← h₂]

Goal state after:
case mk
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
X : C
h : F.cones.RepresentableBy X
j : J
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
h₁ : { pt := pt✝, π := π✝ }.pt = pt✝
h₂ : (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π = π✝
⊢ homOfCone h { pt := pt✝, π := π✝ } ≫ (limitCone h).π.app j =
    { pt := pt✝, π := (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π }.π.app j
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case mk
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
h₁ : { pt := pt✝, ι := ι✝ }.pt = pt✝
h₂ : (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) = ι✝
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt✝, ι := ι✝ } = { pt := pt✝, ι := ι✝ }.ι.app j

Tactic:
conv_rhs => rw [← h₂]

Goal state after:
case mk
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
h₁ : { pt := pt✝, ι := ι✝ }.pt = pt✝
h₂ : (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) = ι✝
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt✝, ι := ι✝ } =
    { pt := pt✝, ι := (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) }.ι.app j
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:
bijective_iff_isIso_ofHom

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
T : C
⊢ IsIso (↾fun x ↦ x ≫ f)
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:
bijective_iff_isIso_ofHom

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

Goal state before:
pp: X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (f ≫ g)))).toCatHom =
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom f))).toCatHom ≫
      (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom g))).toCatHom

Tactic:
ext
    simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.comp_toFunctor]
    apply Functor.ext
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ ⋯.HasLift

Tactic:
rw [right_adjoint_hasLift_iff]
  infer_instance

Goal state after:
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 : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
⊢ pre F E ≫ colim.map α = colim.map (E.whiskerLeft α) ≫ pre G E

Tactic:
by
  ext
  rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]
  rfl

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
⊢ post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ post G H

Tactic:
by
  ext
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
  rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]
  rfl

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

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ lift t ≫ s.π.app none = t.π.app none

Tactic:
exact facbase t

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }
⊢ eqToHom ⋯ ≫ colimit.ι (Discrete.functor f) { as := ε b } = ι f (ε b)

pp: case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }
⊢ { as := b } = { as := ε.symm (ε b) }

Tactic:
all_goals { simp }

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
h : Hom.left { left := left✝, right := b, w := w✝ } = Hom.left g
⊢ { left := left✝, right := b, w := w✝ } = g

Tactic:
let ⟨_,e,_⟩ := g

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : Hom.left { left := left✝¹, right := b, w := w✝¹ } = Hom.left { left := left✝, right := e, w := w✝ }
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map b
h : Hom.right { left := left✝, right := b, w := w✝ } = Hom.right g
⊢ { left := left✝, right := b, w := w✝ } = g

Tactic:
let ⟨_,e,_⟩ := g

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : Hom.right { left := left✝¹, right := b, w := w✝¹ } = Hom.right { left := left✝, right := e, w := w✝ }
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }
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
⊢ IsIso (pushout.inr f g)

Tactic:
refine ⟨⟨pushout.desc (inv f ≫ g) (𝟙 _) (by simp), by simp, ?_⟩⟩
  ext
  · simp [← pushout.condition]
  · simp

Goal state after: