fix errors from rebase, mk_all

Author: robertmaxton42

Mathlib.lean

@@ -2181,6 +2181,11 @@ import Mathlib.CategoryTheory.Category.PartialFun
 import Mathlib.CategoryTheory.Category.Pointed
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.Quiv
+import Mathlib.CategoryTheory.Category.Quiv.AsFunctor.Defs
+import Mathlib.CategoryTheory.Category.Quiv.Colimits
+import Mathlib.CategoryTheory.Category.Quiv.Limits
+import Mathlib.CategoryTheory.Category.Quiv.Shapes
+import Mathlib.CategoryTheory.Category.Quiv.WalkingQuiver
 import Mathlib.CategoryTheory.Category.ReflQuiv
 import Mathlib.CategoryTheory.Category.RelCat
 import Mathlib.CategoryTheory.Category.TwoP
@@ -2288,6 +2293,7 @@ import Mathlib.CategoryTheory.Filtered.CostructuredArrow
 import Mathlib.CategoryTheory.Filtered.Final
 import Mathlib.CategoryTheory.Filtered.Flat
 import Mathlib.CategoryTheory.Filtered.Grothendieck
+import Mathlib.CategoryTheory.Filtered.Level
 import Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
 import Mathlib.CategoryTheory.Filtered.Small
 import Mathlib.CategoryTheory.FinCategory.AsType
@@ -2899,6 +2905,7 @@ import Mathlib.CategoryTheory.Sums.Basic
 import Mathlib.CategoryTheory.Sums.Products
 import Mathlib.CategoryTheory.Thin
 import Mathlib.CategoryTheory.Topos.Classifier
+import Mathlib.CategoryTheory.Topos.Presheaf
 import Mathlib.CategoryTheory.Triangulated.Adjunction
 import Mathlib.CategoryTheory.Triangulated.Basic
 import Mathlib.CategoryTheory.Triangulated.Functor

Mathlib/CategoryTheory/Equivalence.lean

@@ -716,8 +716,9 @@ alias Equivalence.ofFullSubcategory := ObjectProperty.fullSubcategoryCongr
 the right functor restricted to the essential image of the left functor. -/
 @[simps!]
 def essImageInclusionComp (F : C ⥤ D) (G : D ⥤ E) :
-    (F.essImageInclusion ⋙ G).EssImageSubcategory ≌ (F ⋙ G).EssImageSubcategory :=
-  ObjectProperty.fullSubcategoryCongr fun e ↦ by
+    (F.essImage.ι ⋙ G).EssImageSubcategory ≌ (F ⋙ G).EssImageSubcategory :=
+  ObjectProperty.fullSubcategoryCongr <| by
+    ext e
     constructor <;> intro h
     · use (Functor.essImage.witness h).2.choose
       exact ⟨G.mapIso (Functor.essImage.witness h).2.choose_spec.some |>.trans <|
@@ -733,18 +734,16 @@ noncomputable def Functor.EssImage.compEquivOfFullyFaithful
     (F : C ⥤ D) (G : D ⥤ E) [G.Full] [G.Faithful] :
     (F ⋙ G).EssImageSubcategory ≌ F.EssImageSubcategory :=
   letI inverse : F.EssImageSubcategory ⥤ (F ⋙ G).EssImageSubcategory :=
-    FullSubcategory.lift _ (F.essImageInclusion ⋙ G)
+    ObjectProperty.lift _ (F.essImage.ι ⋙ G)
       (⟨_, ⟨G.mapIso ·.property.choose_spec.some⟩⟩)
-  have : inverse.Full := inferInstanceAs (FullSubcategory.lift _ _ _).Full
-  have : inverse.Faithful := inferInstanceAs (FullSubcategory.lift _ _ _).Faithful
   have : inverse.EssSurj := by
     constructor
     rintro ⟨Y, ⟨X, ⟨ι⟩⟩⟩
     exact ⟨⟨F.obj X, ⟨X, ⟨Iso.refl _⟩⟩⟩, ⟨InducedCategory.isoMk ι⟩⟩
-  have : inverse.IsEquivalence := ⟨‹_›, ‹_›, ‹_›⟩
+  have : inverse.IsEquivalence := ⟨inferInstance, inferInstance, ‹_›⟩
   inverse.asEquivalence.symm
 
-end Equivalence
+-- end Equivalence
 
 namespace Iso
 

Mathlib/Logic/Equiv/Basic.lean

@@ -433,17 +433,6 @@ def sigmaAssocProd {α β : Type*} {γ : α → β → Type*} :
     (ab : α × β) × γ ab.1 ab.2 ≃ (a : α) × (b : β) × γ a b :=
   sigmaCongrLeft' (sigmaEquivProd _ _).symm |>.trans <| sigmaAssoc γ
 
-/-- A subtype of a sigma which pins down the base of the sigma is equivalent to
-the respective fiber. -/
-@[simps]
-def sigmaSubtype {α : Type*} {β : α → Type*} (a : α) :
-    {s : Sigma β // s.1 = a} ≃ β a where
-  toFun := fun ⟨⟨_, b⟩, h⟩ => h ▸ b
-  invFun b := ⟨⟨a, b⟩, rfl⟩
-  left_inv := fun ⟨a, h⟩ ↦ by cases h; simp
-  right_inv b := by simp
-
-
 section
 attribute [local simp] Trans.trans sigmaAssoc subtypeSigmaEquiv uniqueSigma eqRec_eq_cast
 
@@ -489,40 +478,6 @@ lemma sigmaSigmaSubtypeEq_symm_apply {α β : Type*} {γ : α → β → Type*}
   simp [sigmaSigmaSubtypeEq]
 
 end
-
-/-- A sigma of a sigma whose second base does not depend on the first is equivalent
-to a sigma whose base is a product. -/
-@[simps!]
-def sigmaAssocProd {α β : Type*} {γ : α → β → Type*} :
-    (ab : α × β) × γ ab.1 ab.2 ≃ (a : α) × (b : β) × γ a b :=
-  sigmaCongrLeft' (sigmaEquivProd _ _).symm |>.trans <| sigmaAssoc γ
-
-
-/-- A subtype of a dependent triple which pins down both bases is equivalent to the
-respective fiber. -/
-@[simps! (config := {simpRhs := true})]
-def sigmaSigmaSubtype {α : Type*} {β : α → Type*} {γ : (a : α) → β a → Type*}
-    (p : (a : α) × β a → Prop) [uniq : Unique {ab // p ab}] (a : α) (b : β a) (h : p ⟨a, b⟩) :
-    {s : (a : α) × (b : β a) × γ a b // p ⟨s.1, s.2.1⟩} ≃ γ a b := by
-  calc {s : (a : α) × (b : β a) × γ a b // p ⟨s.1, s.2.1⟩}
-  _ ≃ _ := subtypeEquiv (p := fun ⟨a, b, c⟩ ↦ p ⟨a, b⟩) (q := (p ·.1))
-    (sigmaAssoc γ).symm fun s ↦ by simp [sigmaAssoc]
-  _ ≃ _ := subtypeSigmaEquiv _ _
-  _ ≃ _ := uniqueSigma (fun ab ↦ γ (Sigma.fst <| Subtype.val ab) (Sigma.snd <| Subtype.val ab))
-  _ ≃ γ a b := by rw [ ← show ⟨⟨a, b⟩, h⟩ = uniq.default from uniq.uniq _]
-
-/-- A specialization of `sigmaSigmaSubtype` to the case where the second base
-does not depend on the first, and the property being checked for is simple
-equality. Useful for e.g. hom-types. -/
-@[simps!]
-def sigmaSigmaSubtypeEq {α β : Type*} {γ : α → β → Type*} (a : α) (b : β) :
-    {s : (a : α) × (b : β) × γ a b // s.1 = a ∧ s.2.1 = b} ≃ γ a b :=
-  have : Unique (@Subtype ((_ : α) × β) (fun ⟨a', b'⟩ ↦ a' = a ∧ b' = b)) := {
-    default := ⟨⟨a, b⟩, ⟨rfl, rfl⟩⟩
-    uniq := by rintro ⟨⟨a', b'⟩, ⟨rfl, rfl⟩⟩; rfl
-  }
-  sigmaSigmaSubtype (fun ⟨a', b'⟩ ↦ a' = a ∧ b' = b) a b ⟨rfl, rfl⟩
-
 end
 
 section subtypeEquivCodomain
@@ -988,12 +943,6 @@ lemma eq_conj {α α' β β' : Sort*} (ε₁ : α ≃ α') (ε₂ : β' ≃ β)
     (f : α → β) (f' : α' → β') : ε₂.symm ∘ f ∘ ε₁.symm = f' ↔ f = ε₂ ∘ f' ∘ ε₁ := by
   rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]
 
-lemma eq_conj {α α' β β' : Type*} (ε₁ : α ≃ α') (ε₂ : β' ≃ β)
-    (f : α → β) (f' : α' → β') : f = ε₂ ∘ f' ∘ ε₁ ↔ ε₂.symm ∘ f ∘ ε₁.symm = f' := by
-  constructor <;> (intro h; ext)
-  · simp [h]
-  · simp [← h]
-
 section BinaryOp
 
 variable {α₁ β₁ : Type*} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁)