mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ 𝔼 _i ∈ s, a = a

Tactic:
rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
  exact mod_cast hs.card_ne_zero

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : Semiring M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
⊢ ↑(#s) * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
rw [← nsmul_eq_mul, card_smul_expect]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-↑N) ↑N ∪ {-(↑N + 1), ↑N + 1}, f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0

Tactic:
prod_union (by simp),

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ (∏ x ∈ Icc (-↑N) ↑N, f x) * ∏ x ∈ {-(↑N + 1), ↑N + 1}, f x = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ ∏ x ∈ Ico (-↑b) ↑b ∪ {-(↑b + 1), ↑b}, f x / f (x + 1) = f (-(↑b + 1)) / f (↑b + 1)

Tactic:
prod_union (by simp),

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ (∏ x ∈ Ico (-↑b) ↑b, f x / f (x + 1)) * ∏ x ∈ {-(↑b + 1), ↑b}, f x / f (x + 1) = f (-(↑b + 1)) / f (↑b + 1)
Module: Mathlib.Data.Int.Interval

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

Tactic:
refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind
    · calc
        i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ (assocAux f hf g hg) ((f x₁) x₂ ⊗ₜ[S] x₃) = x₁ ⊗ₜ[R] (g x₂) x₃

Tactic:
by
  have : hf.equiv.symm (f x₁ x₂) = x₁ ⊗ₜ x₂ := hf.equiv_symm_apply _ _
  simp [IsTensorProduct.assocAux, this]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m + ∑ x ∈ Ico (m + 1) n, (f x • ∑ i ∈ range (x + 1), g i - f x • ∑ i ∈ range x, g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
sum_sub_distrib,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m + (∑ x ∈ Ico (m + 1) n, f x • ∑ i ∈ range (x + 1), g i - ∑ x ∈ Ico (m + 1) n, f x • ∑ i ∈ range x, g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
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 ∈ s, Nat.card { a // f a = b }

Tactic:
show ∑ b ∈ s, Nat.card {a //f a = b} = ∑ b ∈ t, Nat.card {a | f a = b} by
    exact (Finset.sum_subset (by simp [t]) (by aesop)).symm

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
⊢ Nat.card ↑(f ⁻¹' ↑t) = ∑ b ∈ t, Nat.card ↑{a | f a = b}
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ (AlgebraTensorModule.rid R S S) (1 ⊗ₜ[R] x) = (Algebra.linearMap R S) x

Tactic:
by
    simpa using (Algebra.algebraMap_eq_smul_one x).symm

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
← val_eq_zero,

Goal state after:
α : Type u_1
s : Finset α
⊢ s.sym2.val = 0 ↔ s = ∅
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ (s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
dedup_cons_of_mem hm,

Goal state after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ (s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2)).dedup = xs.dedup.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∏ i ∈ s, i ^ Multiset.count i ↑k = ∏ d ∈ s, d ^ Multiset.count d ↑k

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s

Tactic:
· apply Finset.prod_congr rfl (by simp)

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹³ : CommSemiring R'
inst✝¹² : CommSemiring S'
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra R' S'
inst✝⁸ : Algebra R S'
inst✝⁷ : IsScalarTower R R' S'
inst✝⁶ : IsScalarTower R S S'
h : IsPushout R R' S S'
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
⊢ IsPushout R R' S T

Tactic:
rw [isPushout_iff] at h ⊢

Goal state after:
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 : IsBaseChange R' (toAlgHom R S S').toLinearMap
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
⊢ IsBaseChange R' (toAlgHom R S T).toLinearMap
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.hom = β.inv ↔ β.hom = α.inv

Tactic:
rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
⊢ ofObj Subtype.val X → P X

Tactic:
rintro ⟨X, hX⟩; exact hX

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

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z → X = Z ∨ Y = Z

pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z

Tactic:
· rintro ⟨_ | _⟩ <;> tauto

Goal state after:
case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
refine (em p).imp ?_ ?_

Goal state after:
case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ p → f True

case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ ¬p → f False
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
⊢ (P.ι ⋙ F).essImage = P.map F

Tactic:
by
  ext Y
  constructor
  · rintro ⟨X, ⟨e⟩⟩
    exact ⟨X.1, X.2, ⟨e⟩⟩
  · rintro ⟨X, hX, ⟨e⟩⟩
    exact ⟨⟨X, hX⟩, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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 H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f

Tactic:
Functor.comp_map,

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 : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f
Module: Mathlib.CategoryTheory.Whiskering

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 H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f

Tactic:
Functor.comp_map,

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 : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ H.map (F.map f)
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f

Tactic:
Functor.comp_map,

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f

Tactic:
Functor.comp_map,

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ F.map (H.map f)
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 (𝟙 Y) = 𝟙 (F.obj Y)

Tactic:
Functor.map_id

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
se : SplitEpi f
F : C ⥤ D
⊢ 𝟙 (F.obj Y) = 𝟙 (F.obj Y)
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: case h₂
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'
inst✝¹ : F₁.Faithful
inst✝ : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.right = g.right

Tactic:
· exact F₂.map_injective (congr_arg CommaMorphism.right h)

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f g : (End X)ˣ
⊢ { hom := ↑(f * g), inv := (f * g).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := ↑f, inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } *
      { hom := ↑g, inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
cases f; cases g; rfl

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

Tactic:
rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]

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
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ (e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫ G.map ((e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsLeftAdjoint
⊢ G.IsLeftAdjoint

Tactic:
let iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
    (Functor.leftUnitor _).symm ≪≫ Functor.isoWhiskerRight (F.asEquivalence.counitIso).symm _ ≪≫
      Functor.associator _ _ _

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 : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsLeftAdjoint
iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
  G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G ≪≫ F.asEquivalence.inverse.associator F.asEquivalence.functor G
⊢ G.IsLeftAdjoint
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsRightAdjoint
⊢ G.IsRightAdjoint

Tactic:
let iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
    (Functor.leftUnitor _).symm ≪≫ Functor.isoWhiskerRight (F.asEquivalence.counitIso).symm _ ≪≫
      Functor.associator _ _ _

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 : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsRightAdjoint
iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
  G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G ≪≫ F.asEquivalence.inverse.associator F.asEquivalence.functor G
⊢ G.IsRightAdjoint
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Tactic:
rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]
  simp

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
a₁✝ b₁✝ a₂✝ b₂✝ : C
i₁ : a₁✝ ≅ a₂✝
i₂ : b₁✝ ≅ b₂✝
⊢ Nonempty (a₁✝ ⟶ b₁✝) = Nonempty (a₂✝ ⟶ b₂✝)

Tactic:
exact
            propext
              ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom,
                Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩

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
l : sq.LiftStruct
⊢ i ≫ (adj.homEquiv B X) l.l = (adj.homEquiv A X) u

Tactic:
← adj.homEquiv_naturality_left,

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
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
l : sq.LiftStruct
⊢ (adj.homEquiv A X) (G.map i ≫ l.l) = (adj.homEquiv A X) u
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✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
k : K
⊢ pre F E ≫ π (E ⋙ F) k = π F (E.obj k)

Tactic:
simp [limit.pre]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ s.ι.app none ≫ i.hom = t.ι.app none

Tactic:
simp_rw [← h₁, Category.assoc, w₁, h₂]

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow F Y.left
f : X✝ ⟶ Y✝
⊢ Over.Hom.left ((toOver F X).map (homMk f.left ⋯) ≫ (mk (Over.homMk Y✝.hom ⋯)).hom) =
    Over.Hom.left (mk (Over.homMk X✝.hom ⋯)).hom

Tactic:
exact CostructuredArrow.w f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f

Tactic:
· simp [fst_eq_snd_of_mono_eq]

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f

Tactic:
· simp [fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.fst

Tactic:
refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd

Tactic:
· simp [fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasLimit F

Tactic:
have := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
this : HasLimit (Functor.empty D)
⊢ HasLimit F
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case invFun
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0 → (X ≅ 0) × (Y ≅ 0)

pp: case left_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam (Function.LeftInverse ?invFun ⋯) Equiv.left_inv._autoParam

pp: case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam (Function.RightInverse ?invFun ⋯) Equiv.right_inv._autoParam

Tactic:
· rintro ⟨hX, hY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X) hX
    · exact (idZeroEquivIsoZero Y) hY

Goal state after:
case left_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.LeftInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.left_inv._autoParam

case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.RightInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.right_inv._autoParam