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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∉ fromRel ⋯

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
z : Sym2 α
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯ ↔ s(x, y) ∈ {z | ¬z.IsDiag}

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
⊢ (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x)) 0 =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))) 0

Tactic:
by simp

Goal state after:
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'
inst✝ : IsPushout R S R' S'
a : S
⊢ (algebraMap S S') a = (equiv R S R' S') (a ⊗ₜ[R] 1)

Tactic:
equiv_tmul,

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'
inst✝ : IsPushout R S R' S'
a : S
⊢ (algebraMap S S') a = (algebraMap S S') a * (algebraMap R' S') 1
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'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (algebraMap R' S') a = (equiv R S R' S') (1 ⊗ₜ[R] a)

Tactic:
equiv_tmul,

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'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (algebraMap R' S') a = (algebraMap S S') 1 * (algebraMap R' S') a
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 S R' S'
x✝ : R'
x : R' ⊗[R] S
⊢ ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • 0) =
    (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : CommSemiring R
inst✝³⁰ : CommSemiring S
inst✝²⁹ : Algebra R S
inst✝²⁸ : Module R M
inst✝²⁷ : Module R N
inst✝²⁶ : Module S N
inst✝²⁵ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
x✝ : S
⊢ (TensorProduct.lid R S) (1 ⊗ₜ[R] x✝) = (toAlgHom R S S).toLinearMap x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ α ≪≫ α.symm ≪≫ β = β

Tactic:
rw [← trans_assoc, self_symm_id, refl_trans]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ inv f = g

Tactic:
by
  have := congrArg (inv f ≫ ·) hom_inv_id
  grind

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ inv (𝟙 X) = 𝟙 X

Tactic:
by
  apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ inv (f ≫ h) = inv h ≫ inv f

Tactic:
by
  apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv (inv f) = f

Tactic:
by
  apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
by
  apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ⟶ Y
⊢ F.map (F.preimage (F.map f)) = F.map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.hom ≫ F.preimage f.inv) = F.map (𝟙 X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty C
h : ofObj X ≤ P
i : ι
⊢ ofObj X (X i)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.inv ≫ F.preimage f.hom) = F.map (𝟙 Y)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
x✝ : X ⟶ Y
⊢ hF.preimage (F.map x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
x✝ : F.obj X ⟶ F.obj Y
⊢ F.map (hF.preimage x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
⊢ F.map (hF.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X Y Z : C
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (hF.preimage (f ≫ g)) = F.map (hF.preimage f ≫ hF.preimage g)

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.hom ≫ hF.preimage e.inv) = F.map (𝟙 X)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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 : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (α.app X)
⊢ inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.inv ≫ hF.preimage e.hom) = F.map (𝟙 Y)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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 ⟶ G
inst✝ : ∀ (X : C), IsIso (α.app X)
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (asIso (α.app Y)).hom = (asIso (α.app X)).hom ≫ G.map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : G.Full
X✝ Y✝ : C
f : (F ⋙ G).obj X✝ ⟶ (F ⋙ G).obj Y✝
⊢ (F ⋙ G).map (F.preimage (G.preimage f)) = f

Tactic:
by simp

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (p.comp nil).toList = nil.toList ++ p.toList

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : F.ReflectsIsomorphisms
X Y : C ⥤ D
f : X ⟶ Y
x✝ : IsIso (((whiskeringRight C D E).obj F).map f)
⊢ IsIso f

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : F.ReflectsIsomorphisms
X Y : C ⥤ D
f : X ⟶ Y
x✝ : IsIso (((whiskeringRight C D E).obj F).map f)
⊢ ∀ (X_1 : C), IsIso (f.app X_1)
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C✝ : Type u₁
D✝ : Type u₂
E : Type u₃
inst✝⁷ : Category.{v₁, u₁} C✝
inst✝⁶ : Category.{v₂, u₂} D✝
inst✝⁵ : Category.{v₃, u₃} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ E
J : Type u_1
C : Type u_2
D : Type u_3
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} C
inst✝² : Category.{v_3, u_3} D
G : J ⥤ D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hG : ∀ (j : J), F.essImage (G.obj j)
x✝ : J
⊢ F.map
      (F.preimage
        ((F.toEssImage.objObjPreimageIso { obj := G.obj x✝, property := ⋯ }).hom.hom ≫
          G.map (𝟙 x✝) ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj x✝, property := ⋯ }).inv.hom)) =
    F.map (𝟙 (F.toEssImage.objPreimage { obj := G.obj x✝, property := ⋯ }))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C✝ : Type u₁
D✝ : Type u₂
E : Type u₃
inst✝⁷ : Category.{v₁, u₁} C✝
inst✝⁶ : Category.{v₂, u₂} D✝
inst✝⁵ : Category.{v₃, u₃} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ E
J : Type u_1
C : Type u_2
D : Type u_3
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} C
inst✝² : Category.{v_3, u_3} D
G : J ⥤ D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hG : ∀ (j : J), F.essImage (G.obj j)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ F.map
      (F.preimage
        ((F.toEssImage.objObjPreimageIso { obj := G.obj X✝, property := ⋯ }).hom.hom ≫
          G.map (x✝¹ ≫ x✝) ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj Z✝, property := ⋯ }).inv.hom)) =
    F.map
      (F.preimage
          ((F.toEssImage.objObjPreimageIso { obj := G.obj X✝, property := ⋯ }).hom.hom ≫
            G.map x✝¹ ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj Y✝, property := ⋯ }).inv.hom) ≫
        F.preimage
          ((F.toEssImage.objObjPreimageIso { obj := G.obj Y✝, property := ⋯ }).hom.hom ≫
            G.map x✝ ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj Z✝, property := ⋯ }).inv.hom))

Tactic:
by simp

Goal state after:
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
Y : D
X : C
e : F.obj X ≅ Y
⊢ ⊤ X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
p : X = Y
⊢ eqToHom p ≫ eqToHom ⋯ = 𝟙 X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
p : X = Y
⊢ eqToHom ⋯ ≫ eqToHom p = 𝟙 Y

Tactic:
by simp

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 ⟶ G
X Y : C
h : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)

Tactic:
simp [eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ e (e.symm X✝) = X✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ Y✝ = e (e.symm Y✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
x✝ : InducedCategory D ⇑e
⊢ (𝟭 (InducedCategory D ⇑e)).obj x✝ =
    (inducedFunctor ⇑e ⋙
          { obj := ⇑e.symm, map := fun {X Y} f ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
            map_comp := ⋯ }).obj
      x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
x✝ : D
⊢ ({ obj := ⇑e.symm, map := fun {X Y} f ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
            map_comp := ⋯ } ⋙
          inducedFunctor ⇑e).obj
      x✝ =
    (𝟭 D).obj x✝

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : C ⥤ D
X : C
⊢ ∀ {X_1 Y : J} (f : X_1 ⟶ Y),
    ((F ⋙ const J).obj X).map f ≫ (Iso.refl (((F ⋙ const J).obj X).obj Y)).hom =
      (Iso.refl (((F ⋙ const J).obj X).obj X_1)).hom ≫ ((const J ⋙ (whiskeringRight J C D).obj F).obj X).map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f.op ≫ (inv f).op).unop = (𝟙 (op Y)).unop

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ ((inv f).op ≫ f.op).unop = (𝟙 (op X)).unop

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ (f ≫ (inv f.op).unop).op = (𝟙 X).op

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ ((inv f.op).unop ≫ f).op = (𝟙 Y).op

Tactic:
by simp

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
F : C ⥤ D
inst✝ : F.Full
X✝ Y✝ : Cᵒᵖ
f : F.op.obj X✝ ⟶ F.op.obj Y✝
⊢ F.op.map (F.preimage f.unop).op = f

Tactic:
by simp

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
F : Cᵒᵖ ⥤ D
inst✝ : F.Full
X✝ Y✝ : C
f : F.rightOp.obj X✝ ⟶ F.rightOp.obj Y✝
⊢ F.rightOp.map (F.preimage f.unop).unop = f

Tactic:
by simp

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
F : C ⥤ Dᵒᵖ
inst✝ : F.Full
X✝ Y✝ : Cᵒᵖ
f : F.leftOp.obj X✝ ⟶ F.leftOp.obj Y✝
⊢ F.leftOp.map (F.preimage f.op).op = f

Tactic:
by simp

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

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    (comap C h ⋙ eval (C ∘ h) j).map f ≫ (Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj Y)).hom =
      (Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj X)).hom ≫ (eval C (h j)).map f

Tactic:
by simp

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
F G : C ⥤ D
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.op.map f ≫ (α.app (unop Y)).op).unop = ((α.app (unop X)).op ≫ F.op.map f).unop

Tactic:
by simp

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
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.unop.map f ≫ (α.app (op Y)).unop).op = ((α.app (op X)).unop ≫ F.unop.map f).op

Tactic:
by simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
i : Discrete I
⊢ (𝟭 (Discrete I)).obj i = (functor (mk ∘ ⇑e) ⋙ functor (mk ∘ ⇑e.symm)).obj i

Tactic:
by simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
j : Discrete J
⊢ (functor (mk ∘ ⇑e.symm) ⋙ functor (mk ∘ ⇑e)).obj j = (𝟭 (Discrete J)).obj j

Tactic:
by simp

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

Tactic:
by simp

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

Goal state before:
pp: case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X

Tactic:
intro X
    ext i
    specialize h i
    have := congr_obj h X
    simpa

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

Tactic:
by simp

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

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

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

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
e : J ≃ I
i : I
⊢ e (e.symm i) = i

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ inv (inv f) = f

Tactic:
by simp

Goal state after: