mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (ConcreteCategory.hom ((cospan f g).map (𝟙 none))) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app none)) x) =
    (ConcreteCategory.hom ((cospan f g).map Hom.inl)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
simp

Goal state after:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (RingHom.id ↑C) (((Hom.hom f).comp (Hom.hom (pullback.fst f g))) x) =
    (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (ConcreteCategory.hom ((cospan f g).map (𝟙 (some WalkingPair.left))))
      ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.left))) x) =
    (ConcreteCategory.hom ((cospan f g).map (𝟙 left))) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h =
    F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ (α_ (F.map f) (F.map g) (F.map h)).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵒᵖᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ f = 𝟙 b

Tactic:
hf

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵒᵖᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = 𝟙 b
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (η ▷ g) ≫
      (G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f'✝ g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    ((G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫
      (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g

Tactic:
dsimp
    rw [← G.map₂_comp_assoc, mapComp_naturality_left, G.map₂_comp_assoc, mapComp_naturality_left,
      assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = f

Tactic:
hf

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = 𝟙 b
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (λ_ (F.map f)).hom = ((F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv) ≫ (F.map₂Iso (λ_ f)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (ρ_ (F.map f)).hom = (F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv) ≫ (F.map₂Iso (ρ_ f)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f).hom = F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId a).inv ▷ F.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
a b : B
f : a ⟶ b
⊢ (F.mapId a).hom ▷ F.map f = (F.mapComp (𝟙 a) f).inv ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b)).hom = F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
a b : B
f : a ⟶ b
⊢ F.map f ◁ (F.mapId b).hom = (F.mapComp f (𝟙 b)).inv ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommAlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommAlgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵖ C
a b✝ b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ f = 𝟙 b

Tactic:
hf

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵖ C
a b✝ b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = 𝟙 b
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommAlgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommAlgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Algebra R X
inst✝³ : CommRing Y
inst✝² : Algebra R Y
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Algebra R X
inst✝³ : CommRing Y
inst✝² : Algebra R Y
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X : C
⊢ (singleton X).op = singleton (op X)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X : Cᵒᵖ
⊢ (singleton X).unop = singleton (unop X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ inv ((F'.mapCompIso f g).hom ▷ F.map h) ≫ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j : J
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((const J).obj ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj).map f ≫
        (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ ((const J).obj (F.obj j)).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j : J
⊢ ∀ (j' : J), F j = F j'
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: β : Type v
f : β → Type v
P : Type v
s : (b : β) → P ⟶ f b
b : β
x : P
⊢ (ConcreteCategory.hom (Pi.π f b)) ((ConcreteCategory.hom (Pi.lift s)) x) = (ConcreteCategory.hom (s b)) x

Tactic:
simp

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

Goal state before:
pp: case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.fst =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.fst

Tactic:
simp

Goal state after:
case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.fst = ↾_root_.Prod.fst
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.snd =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.snd

Tactic:
simp

Goal state after:
case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.snd = ↾_root_.Prod.snd ≫ x✝
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.fst =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.fst

Tactic:
simp

Goal state after:
case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x✝¹
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.snd =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.snd

Tactic:
simp

Goal state after:
case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ ∀ (X : C), ⊤ ((𝟭 C).obj X)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
i : ι
⊢ ofObj X (X i)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
i : ι
⊢ ∃ a, (fun i ↦ ⟨X i, ⋯⟩) a = ⟨X i, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
F : C ⥤ D
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure.map F ≤ (Q.strictMap F).isoClosure

Tactic:
simp

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

Goal state before:
pp: case h.left
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ Hom.hom (homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i)) = Hom.hom (𝟙 X)

Tactic:
simp

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

Goal state before:
pp: case h.right
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ Hom.hom (homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i) = Hom.hom (𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
⊢ FinitePresentation R (MvPolynomial ι A)

Tactic:
by
  have hfp : FinitePresentation R A := inferInstance
  rw [iff_quotient_mvPolynomial'] at hfp ⊢
  -- Make universe level `v` explicit so it matches that of `ι`
  obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
  let g := (MvPolynomial.mapAlgHom f).comp (MvPolynomial.sumAlgEquiv R ι ι').toAlgHom
  cases nonempty_fintype (ι ⊕ ι')
  refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
  · rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
    exact Submodule.fg_bot
  · rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
    exact hf_ker.map MvPolynomial.C

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)

Tactic:
← isEquivalence_ιOfLE_iff h₁

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : (ιOfLE h₁).IsEquivalence
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₂
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f : A ⟶ B
⊢ f.left ≫ B.hom = A.hom

Tactic:
simp

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

Goal state before:
pp: case h₁
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f : A ⟶ B
⊢ A.hom ≫ f.right = B.hom

Tactic:
simp

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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ((CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯)).left = f.left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
p : F.Elements
⊢ (ConcreteCategory.hom (F.map (𝟙 p.fst))) p.snd = p.snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (F.map (↑f ≫ Groupoid.inv ↑f))) p.snd = p.snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ ↑(⟨Groupoid.inv ↑x✝, ⋯⟩ ≫ x✝) = ↑(𝟙 Y✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ ↑(x✝ ≫ ⟨Groupoid.inv ↑x✝, ⋯⟩) = ↑(𝟙 X✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (F.map (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst).hom))
      ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).snd =
    (unop X).snd

Tactic:
simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (𝟙 (F.obj (unop X).1))) (unop X).snd = (unop X).snd
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ↑((𝟭 F.Elementsᵒᵖ).map (op f) ≫
          (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst)
                ⋯).op.hom).unop =
    ↑((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
          (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : ⊤ ≤ P.isoClosure
y : F.Elements
x✝ : ⊤ y
⊢ ⊤ y.fst

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ (F.map (𝟙 X)).toFunctor.obj d = d

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ (Grothendieck.ι F X).obj d = (Grothendieck.ι F X).obj ((F.map (𝟙 X)).toFunctor.obj d)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ (F.map (f ≫ g)).toFunctor.obj d = (F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)

Tactic:
simp

Goal state after: