mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.vcomp.h₁
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ (fun p ↦ normalizeAux p f✝) = ?mk.vcomp.b

Tactic:
assumption

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

Goal state before:
pp: case mk.vcomp.h₂
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝

Tactic:
assumption

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:
by intro _ _ _ _ _ η h; dsimp; induction η using Quot.rec <;> cat_disch

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg₁ : f.base = g.base
hfg₂ : eqToHom ⋯ ≫ f.fiber = g.fiber
⊢ f = g

Tactic:
by
  cases f; cases g
  dsimp at hfg₁ hfg₂
  cat_disch

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x : ∫ F
⊢ (map (𝟙 F)).obj x = (𝟭 (∫ F)).obj x

Tactic:
simp [map]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ F
⊢ (map (α ≫ β)).obj x✝ = (map α ⋙ map β).obj x✝

Tactic:
simp [map]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x : ∫ᶜ F
⊢ (map (𝟙 F)).obj x = (𝟭 (∫ᶜ F)).obj x

Tactic:
simp [map]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ᶜ F
⊢ (map (α ≫ β)).obj x✝ = (map α ⋙ map β).obj x✝

Tactic:
simp [map]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j : ConnectedComponents J
⊢ ∀ (j₁ j₂ : j.Component), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
rintro ⟨j₁, hj₁⟩ ⟨j₂, rfl⟩

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
⊢ φ₁ = φ₂

Tactic:
by
  let adj := mapPullbackAdj g
  let U : Over Z := Over.mk (φ₁ ≫ snd f g)
  let φ₁' : U ⟶ (pullback g).obj (Over.mk f) := Over.homMk φ₁
  let φ₂' : U ⟶ (pullback g).obj (Over.mk f) := Over.homMk φ₂ (by simpa using! h₂.symm)
  have : φ₁' = φ₂' := by
    apply (adj.homEquiv U _).symm.injective
    apply (Over.forget X).map_injective
    simpa using! h₁
  exact congr_arg CommaMorphism.left this

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C
f g : x ⟶ y
⊢ IsDiscrete C

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C'
f g : x ⟶ y
⊢ IsDiscrete C'

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C
f : x ⟶ y
⊢ IsDiscrete C

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C'
f : x ⟶ y
⊢ IsDiscrete C'

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)

Tactic:
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : C ≌ D
x✝ : X✝ ⟶ Y✝
c : C
⊢ (asNatTrans ((𝟭 (C ≌ D)).map x✝ ≫ (Iso.refl ((𝟭 (C ≌ D)).obj Y✝)).hom)).app c =
    (asNatTrans ((Iso.refl ((𝟭 (C ≌ D)).obj X✝)).hom ≫ (symmEquivFunctor C D ⋙ symmEquivInverse C D).map x✝)).app c

Tactic:
simp [symm, symmEquivInverse]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : (D ≌ C)ᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (symmEquivInverse C D ⋙ symmEquivFunctor C D).map x✝ ≫ (Iso.refl (Opposite.unop Y✝)).op.hom =
    (Iso.refl (Opposite.unop X✝)).op.hom ≫ (𝟭 (D ≌ C)ᵒᵖ).map x✝

Tactic:
simp [symm, symmEquivInverse]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : C ≌ D
⊢ (symmEquivFunctor C D).map ((ofComponents (fun e ↦ Iso.refl ((𝟭 (C ≌ D)).obj e)) ⋯).hom.app X) ≫
      (ofComponents (fun e ↦ (Iso.refl (Opposite.unop e)).op) ⋯).hom.app ((symmEquivFunctor C D).obj X) =
    𝟙 ((symmEquivFunctor C D).obj X)

Tactic:
simp [symm, symmEquivInverse]

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✝ : HasFunctorEnrichedHom V F₁ F₂
X : J
⊢ precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂))

Tactic:
by
    ext j
    -- this was produced by `simp?`
    simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, id_comp]
    congr 1
    simp [Under.map, Comma.mapLeft]
    rfl

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)
S : ShortComplex C
⊢ S.ShortExact ↔ ∀ (i : I), (S.map (F i)).ShortExact

Tactic:
refine ⟨fun hS i ↦ ?_, fun hS ↦ ?_⟩

Goal state after:
case refine_1
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)
S : ShortComplex C
hS : S.ShortExact
i : I
⊢ (S.map (F i)).ShortExact

case refine_2
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)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ S.ShortExact
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
a : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (𝟙 X))) a = a

Tactic:
simp only [map_id, FintypeCat.id_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
⊢ IsTerminal (colimit (SingleObj.functor (Aut.toEnd X))) ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)

Tactic:
let J : SingleObj (Aut X) ⥤ C := SingleObj.functor (Aut.toEnd X)

Goal state after:
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 := SingleObj.functor (Aut.toEnd X)
⊢ IsTerminal (colimit (SingleObj.functor (Aut.toEnd X))) ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
⊢ ∃ A f a, IsGalois A ∧ (ConcreteCategory.hom (F.map f)) a = x

Tactic:
obtain ⟨A, a, h1, h2⟩ := exists_galois_representative F X
  obtain ⟨f, hf⟩ := h2.surjective x
  exact ⟨A, f, a, h1, hf⟩

Goal state after:
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 : C
inst✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
⊢ ∃ g, g • x = y

Tactic:
let e (Y : C) : F'.obj Y ≃ F.obj Y := (F.obj Y).uSwitchEquiv

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Tactic:
convert! this <;> simp only [Groupoid.inv_eq_inv]

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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map p✝ ∈ S.arrows (φ.obj c✝) (φ.obj d✝)

Tactic:
assumption

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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map q✝ ∈ S.arrows (φ.obj d✝) (φ.obj e✝)

Tactic:
assumption

Goal state after:
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
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}

Tactic:
rw [inv_eq_inv, ← Functor.map_inv, ← inv_eq_inv]

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✝
⊢ φ.map (Groupoid.inv 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
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✝
⊢ f✝ ∈ S.arrows c✝ d✝

Tactic:
assumption

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

Goal state before:
pp: 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✝

Tactic:
assumption

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

Goal state before:
pp: case left
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
left✝ : c✝ ∈ D
right✝ : d✝ ∈ D
⊢ d✝ ∈ D

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
left✝ : c✝ ∈ D
right✝ : d✝ ∈ D
⊢ c✝ ∈ D

Tactic:
assumption

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

Goal state before:
pp: case left
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
left✝¹ : c✝ ∈ D
right✝¹ : d✝ ∈ D
q✝ : d✝ ⟶ e✝
left✝ : d✝ ∈ D
right✝ : e✝ ∈ D
⊢ c✝ ∈ D

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
left✝¹ : c✝ ∈ D
right✝¹ : d✝ ∈ D
q✝ : d✝ ⟶ e✝
left✝ : d✝ ∈ D
right✝ : e✝ ∈ D
⊢ e✝ ∈ D

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: case right
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 g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).R
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g

Tactic:
exact h _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
have : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x
      (mk (Y := zero) (h₁ Z).some) := by
        rintro ⟨(_ | _), ⟨⟩, φ⟩
        · apply h₂
        · refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)
          exact Zigzag.of_inv (homMk left)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this✝ : Nonempty (CostructuredArrow (parallelPair f g) Z)
this : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
⊢ IsLimit (pullbackCone f g pb)

Tactic:
by
  refine PullbackCone.IsLimit.mk
    (fst := (pullbackCone f g pb).fst) (snd := (pullbackCone f g pb).snd) _
    (fun s ↦ (homPullbackEquiv f g pb hpb s.pt).2 ⟨(s.fst, s.snd), s.condition⟩)
    (fun s ↦ congrArg (·.1.fst)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s ↦ congrArg (·.1.snd)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s m h₁ h₂ ↦ ?_)
  convert! ((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm using 3
  rw [← h₁, ← h₂]; rfl

Goal state after:
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 : ℕ) → functorObj M N (n + 1) ⟶ functorObj M N n

Tactic:
intro n
  refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
  all_goals split_ifs; try rfl; try lia

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ (X ⟶ yp) → md

pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ Function.Injective ?m.137

Tactic:
· intro f
        exact ⟨_, _, f⟩

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ Function.Injective fun f ↦ ⟨X, ⟨yp, f⟩⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: case left
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.left = θ'.left

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: case right
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.right = θ'.right

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: case base
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.base = θ'.base

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁷ : Category.{v_1, u_5} K
inst✝⁶ : Category.{v_2, u_6} K'
inst✝⁵ : Category.{v_3, u_1} J
inst✝⁴ : Category.{v_4, u_2} J'
inst✝³ : Category.{v_5, u_3} C
inst✝² : Category.{v_6, u_4} D
inst✝¹ : HasColimitsOfShape K' C
inst✝ : PreservesLimitsOfShape K colim
G : J ⥤ C
h : (preservesLimitsOfShape K).ColimitOfShape K' G
this✝ : ∀ (j : K'), preservesLimitsOfShape K (h.diag.obj j)
this : PreservesLimitsOfShape K h.diag.flip
e : h.diag.flip ⋙ colim ≅ G :=
  NatIso.ofComponents
    (fun j ↦
      (colimit.isColimit (h.diag.flip.obj j)).coconePointUniqueUpToIso
        (isColimitOfPreserves ((evaluation J C).obj j) h.isColimit))
    ⋯
⊢ preservesLimitsOfShape K G

Tactic:
exact preservesLimitsOfShape_of_natIso e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case fst
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.fst = g.fst

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case snd
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.snd = g.snd

Tactic:
assumption

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

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro W X Y Z ⟨f⟩ ⟨g⟩ ⟨h⟩
    exact Quotient.sound (assoc f g h)

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ adj.unit.app (adj.toMonad.obj A.A) ≫
      G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
apply adj.right_triangle_components_assoc

Goal state after: