mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
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 : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Epi f

Tactic:
rintro ⟨X', Y', f', _, ⟨e⟩⟩
    exact ((MorphismProperty.epimorphisms D).arrow_mk_iso_iff e).1
      (by simpa using inferInstanceAs (Epi (L.map f')))

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
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
G : D ⥤ₑ E
⊢ exactFunctor C E (L ⋙ G.obj)

Tactic:
simpa only [exactFunctor_comp_iff L P] using G.property

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
intro _ _ _ _ _ η h

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
    (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
⊢ ∀ (X Y : ↑((objects ⋙ typeToCat).obj x✝²)) (f : X ⟶ Y),
    ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
      (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f

Tactic:
by intro ⟨_⟩ ⟨_⟩ f
            obtain rfl := Discrete.eq_of_hom f
            cat_disch

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
⊢ ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩ ↔
    ∃ a_1 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_1

Tactic:
suffices c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a) from
      ⟨by aesop, by simp; grind⟩

Goal state after:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
⊢ c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ (f a).Dom

Tactic:
rw [WellFounded.fixF_eq] at h₂

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf ↦
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p ↦
            WellFounded.fixF
              (fun a IH ↦
                Part.assert (f a).Dom fun hf ↦
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ (f a).Dom
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
rw [WellFounded.fixF_eq] at h₂

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf ↦
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p ↦
            WellFounded.fixF
              (fun a IH ↦
                Part.assert (f a).Dom fun hf ↦
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this✝ : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  (β_ (𝟙_ V) (𝟙_ V)).hom ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ (λ_ (𝟙_ V)).inv ≫
      (β_ (𝟙_ V) (𝟙_ V)).hom ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop

Tactic:
rw [this, ← Category.assoc]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this✝ : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  (β_ (𝟙_ V) (𝟙_ V)).hom ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ ((λ_ (𝟙_ V)).inv ≫ (homTo V f.unop ⊗ₘ homTo V g.unop)) ≫ eComp V x y z = f.unop ≫ g.unop
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
ψ ψ' : a' ⟶ a
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (g := g) rfl (ψ ≫ φ) ψ rfl, map_uniq p f φ (g := g) rfl (ψ ≫ φ) ψ' h.symm]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : HasFibers p
S : 𝒮
a b : Fib p S
φ : (ι S).obj a ⟶ (ι S).obj b
inst✝ : p.IsHomLift (𝟙 S) φ
⊢ (ι S).map (homMk φ) = φ

Tactic:
by
  simp [Fib.homMk, congr_hom (inducedFunctor_comp p S)]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex C c
f : K ⟶ L
⊢ QuasiIso f ↔ ∀ (i : I), QuasiIso (((F i).mapHomologicalComplex c).map f)

Tactic:
simp only [_root_.quasiIso_iff, hP.quasiIsoAt_iff]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex C c
f : K ⟶ L
⊢ (∀ (i : α) (i_1 : I), QuasiIsoAt (((F i_1).mapHomologicalComplex c).map f) i) ↔
    ∀ (i : I) (i_1 : α), QuasiIsoAt (((F i).mapHomologicalComplex c).map f) i_1
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: case e₁
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ IsTerminal (colimit (SingleObj.functor (Aut.toEnd X))) ≃ ?β

pp: case e₂
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ ?β ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)

pp: case β
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ Sort ?u.105

Tactic:
· apply (IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
      (isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)

Goal state after:
case e₂
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ IsLimit (asEmptyCone (Quot ⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))))) ≃
    Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝³ x✝² : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝¹ x✝ : { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ { obj := B, pt := b, isGalois := isGalois✝ }
f : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hf :
  (ConcreteCategory.hom (F.map f)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
g : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hg :
  (ConcreteCategory.hom (F.map g)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
Z : C
h : Z ⟶ A
z : (F.obj Z).obj
hgal : IsGalois Z
hhz : (ConcreteCategory.hom (F.map h)) z = a
⊢ ({ val := h, comp := hhz } ≫ { val := f, comp := hf }).val =
    ({ val := h, comp := hhz } ≫ { val := g, comp := hg }).val

Tactic:
apply evaluation_injective_of_isConnected F Z B z

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝³ x✝² : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝¹ x✝ : { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ { obj := B, pt := b, isGalois := isGalois✝ }
f : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hf :
  (ConcreteCategory.hom (F.map f)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
g : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hg :
  (ConcreteCategory.hom (F.map g)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
Z : C
h : Z ⟶ A
z : (F.obj Z).obj
hgal : IsGalois Z
hhz : (ConcreteCategory.hom (F.map h)) z = a
⊢ (fun f ↦ (ConcreteCategory.hom (F.map f)) z) ({ val := h, comp := hhz } ≫ { val := f, comp := hf }).val =
    (fun f ↦ (ConcreteCategory.hom (F.map f)) z) ({ val := h, comp := hhz } ≫ { val := g, comp := hg }).val
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
⊢ ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi

Tactic:
obtain ⟨Y, i, y, h1, _, _⟩ := fiber_in_connected_component F X x

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 : (ConcreteCategory.hom (F.map i)) y = x
left✝ : IsConnected Y
right✝ : Mono i
⊢ ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G✝ : Type u₁
inst✝ : Groupoid G✝
F G : FreeGroupoid C ⥤ G✝
h : of C ⋙ F = of C ⋙ G
⊢ F = G

Tactic:
by rw [lift_unique (of C ⋙ G) F h, ← lift_unique (of C ⋙ G) G rfl]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ ⋂ S ∈ s, S.arrows c✝ d✝
⊢ Groupoid.inv p✝ ∈ ⋂ S ∈ s, S.arrows d✝ c✝

Tactic:
rw [mem_iInter₂] at hp ⊢; exact fun S hS => S.inv (hp S hS)

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {p | Discrete.Arrows c d p} → Groupoid.inv p ∈ {p | Discrete.Arrows d c p}

Tactic:
rintro _ _ _ ⟨⟩

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d : C
⊢ Groupoid.inv (𝟙 c✝) ∈ {p | Discrete.Arrows c✝ c✝ p}
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ X c d ⊆ ⋂ S ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, S.arrows c d

Tactic:
simp only [subset_iInter₂_iff]

Goal state after:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ ∀ i ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, X c d ⊆ i.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
⊢ ∀ {c d : D} {p : c ⟶ d}, p ∈ {x | Map.Arrows φ hφ S c d x} → Groupoid.inv p ∈ {x | Map.Arrows φ hφ S d c x}

Tactic:
rintro _ _ _ ⟨⟩

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f✝ : c✝ ⟶ d✝
hf✝ : f✝ ∈ S.arrows c✝ d✝
⊢ Groupoid.inv (φ.map f✝) ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c✝) x}
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d

Tactic:
rintro _ _ _ ⟨⟩

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ : C
a✝ : c✝ ⟶ d✝
left✝ : c✝ = d✝
right✝ : a✝ ∈ S.arrows c✝ d✝
⊢ a✝ ∈ S.arrows c✝ d✝
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {_f | c ∈ D ∧ d ∈ D} → Groupoid.inv p ∈ {_f | d ∈ D ∧ c ∈ D}

Tactic:
rintro _ _ _ ⟨⟩

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
left✝ : c✝ ∈ D
right✝ : d✝ ∈ D
⊢ Groupoid.inv p✝ ∈ {_f | d✝ ∈ D ∧ c✝ ∈ D}
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f✝ : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f✝ i = (F.obj (op j)).map g ≫ f✝ j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ (F.map φ.op).app j ≫ (f.app (op j)).app j ≫ ι G j = (F.obj (op j')).map φ ≫ (f.app (op j')).app j' ≫ ι G j'

Tactic:
by
    simp [chosenCoend.condition]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p

Tactic:
p₂₃_p₃_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₃ ≫ f₃ = h.p
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n : ℕ
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) n ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < n + 1 then M i else N i) n ≫ eqToHom ⋯ ≫ f n

Tactic:
simp [functorMap]

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

Goal state before:
pp: case zero
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
h : ¬0 < 0
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op 0) then M m else N m) 0 ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < 0 + 1 then M i else N i) 0 ≫ eqToHom ⋯ ≫ f 0

Tactic:
simp [functorMap]

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

Goal state before:
pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if m < n then M m else N m) m

Tactic:
slice_lhs 2 4 => simp only [← dite_eq_ite, ← functorMap_commSq f h]

Goal state after:
case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ s.π.app (Opposite.op (m + 1)) ≫
      ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
          Pi.π (fun m ↦ if x : m < n then M m else N m) m ≫ eqToHom ⋯) ≫
        eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
⊢ (F.map f.op).app j ≫ ι F j = (F.obj (op j')).map f ≫ ι F j'

Tactic:
by
  ext
  apply Quot.sound
  apply coendRel.mk

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ shrinkYoneda.{w, v, u}.map (F.map f.unop).unop ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm ((ConcreteCategory.hom (P.map (F.map f.unop))) (↑s (unop j₂))) ≫ 𝟙 P

Tactic:
rw [shrinkYonedaEquiv_symm_map, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.id
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
X : F C
⊢ motive ⟦Hom.id X⟧

Tactic:
exact id X

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
        μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
      F.map (Y₁ ◁ e₂.hom)

Tactic:
← cancel_mono (F.map (e₁.hom ▷ L.obj X₂)),

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂)) ≫
      F.map (e₁.hom ▷ L.obj X₂) =
    (((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
        F.map (Y₁ ◁ e₂.hom)) ≫
      F.map (e₁.hom ▷ L.obj X₂)