mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ ((ConcreteCategory.hom (𝟙 (ULift.{u, v} (G.obj (op (F.obj (unop i)))))))
        ((ConcreteCategory.hom (limit.π (F.op ⋙ G ⋙ uliftFunctor.{u, v}) i))
          ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))

Tactic:
colimitYonedaHomIsoLimitOp_π_apply

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ {
        down :=
          (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
            ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i)))))
              (𝟙 (F.obj (unop i)))) }.down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
⊢ HasColimitsOfShape (Discrete α) (Ind C)

Tactic:
refine ⟨fun F => ?_⟩
  let I : α → Type v := fun s => (F.obj ⟨s⟩).presentation.I
  let G : ∀ s, I s ⥤ C := fun s => (F.obj ⟨s⟩).presentation.F
  let iso : Discrete.functor (fun s => Pi.eval I s ⋙ G s) ⋙
      (whiskeringRight _ _ _).obj Ind.yoneda ⋙ colim ≅ F := by
    refine Discrete.natIso (fun s => ?_)
    refine (Functor.Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda)) ≪≫ ?_
    exact Ind.colimitPresentationCompYoneda _
  -- The actual proof happens during typeclass resolution in the following line, which deduces
  -- ```
  -- HasColimit Discrete.functor (fun s => Pi.eval I s ⋙ G s) ⋙
  --    (whiskeringRight _ _ _).obj Ind.yoneda ⋙ colim
  -- ```
  -- from the fact that finite limits commute with filtered colimits and from the fact that
  -- `Ind.yoneda` preserves finite colimits.
  exact hasColimit_of_iso iso.symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : PreservesFiniteLimits (F C)
⊢ PreservesFiniteLimits Ind.yoneda.rightOp

Tactic:
apply preservesFiniteLimits_rightOp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
⊢ Module.Injective (End G)ᵐᵒᵖ (G ⟶ B)

Tactic:
refine Module.Baer.injective (fun M g => ?_)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ ∃ g', ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M), g' x = g ⟨x, mem⟩
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
I : InjectiveResolution Y
J : InjectiveResolution Z
g h : I.cocomplex ⟶ J.cocomplex
g_comm : I.ι ≫ g = (CochainComplex.single₀ C).map f ≫ J.ι
h_comm : I.ι ≫ h = (CochainComplex.single₀ C).map f ≫ J.ι
⊢ I.ι ≫ (g - h) = 0

Tactic:
by simp [g_comm, h_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).f,
      zero := ⋯ }.Exact

Tactic:
apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n + 1)).f)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
this : ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f

Tactic:
simp only [Category.assoc]
    exact comm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
⊢ (Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ = R.extMk (g ≫ f) m hm ⋯

Tactic:
by
  have := HasDerivedCategory.standard C
  ext
  simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom, Category.assoc]
  rw [Cocycle.fromSingleMk_precomp g _ (zero_add _) _ (by lia) (by
      simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_precomp, ← ShiftedHom.mk₀_comp 0 rfl,
    ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) (add_zero (n : ℤ)) (by simp)]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom (p ≫ x.hom)) a'' = a

Tactic:
ModuleCat.hom_comp,

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom ∘ₗ ModuleCat.Hom.hom p) a'' = a
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom (q ≫ y.hom)) a'' = a

Tactic:
ModuleCat.hom_comp,

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom ∘ₗ ModuleCat.Hom.hom q) a'' = a
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
⊢ (MorphismProperty.ofObjectProperty P P).cokernels ≤ P

Tactic:
intro _ ⟨_, k, hk, hf⟩
    let := Cofork.IsColimit.epi hk
    exact P.prop_of_epi k.π hf.2

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
⊢ Mono (L.map f)

Tactic:
by
    rw [Preadditive.mono_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ z)
    rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]
    apply hf φ.f
    have : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f := by cat_disch
    rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ∀ (x y : G),
    ⟨fun b ↦ F.map (homOfPair b (x * y)), x * y⟩ =
      ⟨fun b ↦ F.map (homOfPair b x), x⟩ * ⟨fun b ↦ F.map (homOfPair b y), y⟩

Tactic:
intro g

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
g : G
⊢ ∀ (y : G),
    ⟨fun b ↦ F.map (homOfPair b (g * y)), g * y⟩ =
      ⟨fun b ↦ F.map (homOfPair b g), g⟩ * ⟨fun b ↦ F.map (homOfPair b y), y⟩
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N K : Action V G
p : M.Hom N
q : N.Hom K
⊢ ∀ (g : G), M.ρ g ≫ p.hom ≫ q.hom = (p.hom ≫ q.hom) ≫ K.ρ g

Tactic:
intro g

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N K : Action V G
p : M.Hom N
q : N.Hom K
g : G
⊢ M.ρ g ≫ p.hom ≫ q.hom = (p.hom ≫ q.hom) ≫ K.ρ g
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝² : Abelian D := abelian L P
this✝¹ : PreservesFiniteColimits L
x✝² : PreservesFiniteColimits (L ⋙ G)
this✝ : G.Additive
x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
f' : Arrow C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
this : PreservesColimit (parallelPair (L.map f'.hom) 0) G
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
exact preservesColimit_of_iso_diagram G
    (show parallelPair (L.map f'.hom) 0 ≅ parallelPair f 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso iso) (Arrow.rightFunc.mapIso iso))

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ ∀ (a : U.obj X ⟶ U.obj (R.obj Y)),
    U.map (F.map a ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ a ↔
      F.map (U.map (adj₁.counit.app X)) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm a =
        adj₁.counit.app ((U ⋙ F).obj X) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm a

Tactic:
intro g

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g ↔
    F.map (U.map (adj₁.counit.app X)) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g =
      adj₁.counit.app ((U ⋙ F).obj X) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
⊢ ∀ (a : F.obj (L.obj Y) ⟶ F.obj X),
    F.map (adj₁.unit.app (L.obj Y) ≫ U.map a) = a ≫ F.map (adj₁.unit.app X) ↔
      (adj₁.homEquiv (L.obj Y) (F.obj X)) a ≫ U.map (F.map (adj₁.unit.app X)) =
        (adj₁.homEquiv (L.obj Y) (F.obj X)) a ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
intro g

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ leftZigzag t.unit ε = (λ_ t.lift).hom ≫ (ρ_ t.lift).inv

Tactic:
apply (cancel_epi (λ_ _).inv).mp

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := ⋯
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ (λ_ t.lift).inv ≫ leftZigzag t.unit ε = (λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

Tactic:
simp only [prodMap, Part.mem_mk_iff, And.exists, Prod.ext_iff]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ p.obj b = S

Tactic:
domain_eq p f ψ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ S = S
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
    ((ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      (((F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f)) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
        (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)

Tactic:
rw [tensorHom_def'_assoc, ← comp_whiskerRight_assoc,
          ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc,
          assoc, assoc, this, comp_whiskerRight_assoc, comp_whiskerRight_assoc,
          comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
          ← associator_inv_naturality_left_assoc, ← e_assoc',
          Iso.inv_hom_id_assoc, ← whisker_exchange_assoc, id_whiskerLeft_assoc,
          Iso.inv_hom_id_assoc]

Goal state after:
V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    (end_.π (diagram V F₁ F₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫
        (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
          ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝒴.p.obj (F.obj a) = 𝒳.p.obj a

Tactic:
by
  rw [← Functor.comp_obj, F.w]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
⊢ (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ (((diagram V F₁ F₂).obj (Opposite.op i)).obj i)).inv ▷ ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
        (((diagram V F₁ F₂).obj (Opposite.op i)).obj i ◁ (eHomEquiv V) (F₂.map f)) ▷
            ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (F₂.obj j) ▷
              ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j) (F₃.obj j) =
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (F₃.obj j)

Tactic:
have := end_.condition (diagram V F₁ F₂) f
      dsimp [eHomWhiskerLeft, eHomWhiskerRight] at this ⊢
      conv_lhs =>
        rw [tensorHom_def'_assoc, ← comp_whiskerRight_assoc,
          ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc,
          assoc, assoc, this, comp_whiskerRight_assoc, comp_whiskerRight_assoc,
          comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
          ← associator_inv_naturality_left_assoc, ← e_assoc',
          Iso.inv_hom_id_assoc, ← whisker_exchange_assoc, id_whiskerLeft_assoc,
          Iso.inv_hom_id_assoc]
      conv_rhs => rw [assoc, tensorHom_def'_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
x✝ : IsIso ((forgetful 𝒳 𝒴).map α)
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) ((inv ((forgetful 𝒳 𝒴).map α)).app a)

Tactic:
by simp [lift_id_inv_isIso]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)

Tactic:
rw [← IsIso.inv_hom_id (p.map φ)]

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Tactic:
refine lim.map ((colimitIsoColimitGrothendieck L F.flip).hom ≫
    (inv (colimit.pre (CostructuredArrow.grothendieckProj L ⋙ F.flip) R'))) ≫
    (colimitLimitIso (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip).inv ≫
    colim.map ?_ ≫
    colimit.pre _ R' ≫
    (colimitIsoColimitGrothendieck L (limit F)).inv

Goal state after:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F