mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ ((algebraMap S T) x * y) • z = x • y • z

Tactic:
mul_smul

Goal state after:
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ (algebraMap S T) x • y • z = x • y • z
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)
this✝ : IsScalarTower S T Q
this : IsScalarTower R S Q
⊢ (fun g' ↦ ↑R g' ∘ₗ ↑R g ∘ₗ f = i) (hg.lift (hf.lift i))

Tactic:
ext
      simp [IsBaseChange.lift_eq]

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Fobj, map := Gmap }

Tactic:
simp only [mk.injEq, heq_eq_eq, true_and]

Goal state after:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
⊢ Fmap = Gmap
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsIso f.unop ↔ IsIso f

Tactic:
rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y)

pp: case a
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)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

Tactic:
← e.unitInv_naturality

Goal state after:
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y)

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

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete J ⥤ C
⊢ ∀ {X Y : Discrete J} (f : X ⟶ Y),
    (({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
                  { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                    map_id := ⋯, map_comp := ⋯ }).obj
              F).map
          f ≫
        (Iso.refl
            ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                        map_comp := ⋯ } ⋙
                      { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ }).obj
                  F).obj
              Y)).hom =
      (Iso.refl
            ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                        map_comp := ⋯ } ⋙
                      { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ }).obj
                  F).obj
              X)).hom ≫
        ((𝟭 (Discrete J ⥤ C)).obj F).map f

Tactic:
rintro ⟨x⟩ ⟨y⟩ f

Goal state after:
J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete J ⥤ C
x y : J
f : { as := x } ⟶ { as := y }
⊢ (({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as, map_id := ⋯,
                  map_comp := ⋯ }).obj
            F).map
        f ≫
      (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := y })).hom =
    (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := x })).hom ≫
      ((𝟭 (Discrete J ⥤ C)).obj F).map f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
⊢ IsIso f

Tactic:
let ff : X →+* Y := f.hom

Goal state after:
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
⊢ IsIso f

Tactic:
let ff : X →+* Y := f.hom

Goal state after:
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
⊢ IsIso f

Tactic:
let ff : X →+* Y := f.hom

Goal state after:
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
⊢ IsIso f

Tactic:
let ff : X →+* Y := f.hom

Goal state after:
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.IsLimit

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
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ m = lift s

Tactic:
apply G.map_injective; rw [h]
      refine ht.uniq (mapCone G s) _ fun j => ?_
      convert! ← congrArg (fun f => G.map f) (w j)
      apply G.map_comp

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 : F ⊣ G
X Y : C
f : X ⟶ Y
Z : D
⊢ (Function.Bijective fun g ↦ F.map f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g

Tactic:
by
  rw [← Function.Bijective.of_comp_iff' (adj.homEquiv _ _).bijective,
    ← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective]
  congr!
  ext g
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g

Tactic:
simp [← cancel_mono ((ρ_ f).hom ▷ g)]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).obj Y
⊢ (ConcreteCategory.hom
          (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).map f ≫
            (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
            ((evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                      (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).obj
                  X).map
              f)).toFun
      g

Tactic:
← ULift.down_inj

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).map f ≫
              (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                        (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).obj
                    X).map
                f)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type (max w v₁)
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                      (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).map
                  f).app
            F)).toFun
      g

Tactic:
← ULift.down_inj

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type (max w v₁)
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                        (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).map
                    f).app
              F)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ (ConcreteCategory.hom
          (((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
            ((evaluation C (Type v₁) ⋙
                      (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                  X).map
              f)).toFun
      g

Tactic:
← ULift.down_inj

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                    X).map
                f)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation C (Type v₁) ⋙
                      (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                  f).app
            F)).toFun
      g

Tactic:
← ULift.down_inj

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                    f).app
              F)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ IsIso f

Tactic:
refine ⟨g, hg, (hf _).1 ?_⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ (fun x ↦ f ≫ x) (g ≫ f) = (fun x ↦ f ≫ x) (𝟙 Y)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ (ConcreteCategory.hom
          (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
            (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
            ((evaluation C (Type (max v₁ w)) ⋙
                      (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).obj
                  X).map
              f)).toFun
      g

Tactic:
← ULift.down_inj

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
              (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type (max v₁ w)) ⋙
                        (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).obj
                    X).map
                f)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation C (Type (max v₁ w)) ⋙
                      (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).map
                  f).app
            F)).toFun
      g

Tactic:
← ULift.down_inj

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation C (Type (max v₁ w)) ⋙
                        (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).map
                    f).app
              F)).toFun
        g).down
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: case mp
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✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f

Tactic:
exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ x ⟶ y

Tactic:
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert! h.unit.app x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
cases f
    · exact g
    cases g
    apply Hom.init _

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape J C

Tactic:
have := HasColimitsOfSize.has_colimits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
this : HasColimitsOfShape (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasColimitsOfShape J C
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B')

Tactic:
IsIso.eq_comp_inv,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ (inv (prodComparison F A B) ≫ F.map (prod.map f g)) ≫ prodComparison F A' B' = prod.map (F.map f) (F.map g)