fixes

Author: kim-em

Mathlib/Algebra/Homology/HomotopyFiber.lean

@@ -44,6 +44,7 @@ instance [HasBinaryBiproducts C] : HasHomotopyFiber φ where
 
 variable [HasHomotopyFiber φ] [DecidableRel c.Rel]
 
+set_option backward.defeqAttrib.useBackward true in
 instance : HasHomotopyCofiber ((opFunctor C c).map φ.op) where
   hasBinaryBiproduct i j hij := by
     have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij
@@ -58,6 +59,7 @@ end
 
 variable (K) [∀ i, HasBinaryBiproduct (K.X i) (K.X i)]
 
+set_option backward.defeqAttrib.useBackward true in
 instance (i : α) : HasBinaryBiproduct (K.op.X i) (K.op.X i) := by
   dsimp; infer_instance
 
@@ -84,6 +86,7 @@ noncomputable def pathObject := (unopFunctor C c.symm).obj (op K.op.cylinder)
 
 namespace pathObject
 
+set_option backward.defeqAttrib.useBackward true in
 lemma isZero_X (i : α) (h₁ : IsZero (K.X i)) (h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)) :
     IsZero (K.pathObject.X i) := by
   apply IsZero.unop

Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean

@@ -83,6 +83,7 @@ def postcomp {f g : X ⟶ Y} (h : P.LeftHomotopy f g) {Z : C} (p : Y ⟶ Z) :
     P.LeftHomotopy (f ≫ p) (g ≫ p) where
   h := h.h ≫ p
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Left homotopies in a full subcategory identify to left homotopies in the
 ambient category. -/
 noncomputable def fullSubcategoryEquiv {P : ObjectProperty C} {X Y : P.FullSubcategory}

Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy.lean

@@ -86,6 +86,7 @@ def precomp {f g : X ⟶ Y} (h : P.RightHomotopy f g) {Z : C} (i : Z ⟶ X) :
     P.RightHomotopy (i ≫ f) (i ≫ g) where
   h := i ≫ h.h
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Right homotopies in a full subcategory identify to right homotopies in the
 ambient category. -/
 noncomputable def fullSubcategoryEquiv {P : ObjectProperty C} {X Y : P.FullSubcategory}

Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean

@@ -62,7 +62,6 @@ lemma exists_lift_of_kanComplex [KanComplex X]
 /-- If `X` is a Kan complex and `f : ∀ (j : Fin (n + 2)) (_ : j ≠ i), Δ[n] ⟶ X`
 is a compatible family of morphisms (which defines a morphism `Λ[n + 1, i] ⟶ X`),
 then this is a lifting `Δ[n + 1] ⟶ X`. -/
-@[no_expose]
 noncomputable def liftOfKanComplex [KanComplex X] (hf : horn.IsCompatible f) :
     Δ[n + 1] ⟶ X :=
   hf.exists_lift_of_kanComplex.choose

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -560,7 +560,7 @@ theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} := by
 
 @[simp]
 theorem _root_.Order.cof_ordinal : Order.cof Ordinal.{u} = Cardinal.univ.{u, u + 1} := by
-  have := (OrderIso.ofRelIsoLT liftPrincipalSeg.subrelIso.{u, u + 1}).lift_cof_congr
+  have := (OrderIso.ofRelIsoLT liftPrincipalSeg.{u, u + 1}.subrelIso).lift_cof_congr
   rw [Cardinal.lift_id'.{_, u + 2}] at this
   change Order.cof (Iio univ) = _ at this
   rwa [cof_Iio, ← lift_cof, Cardinal.lift_inj, cof_univ, eq_comm] at this