bump to nightly-2023-04-07-14

mathlib commit leanprover-community/mathlib@5ec62c8

Mathbin/Logic/Equiv/Set.lean

@@ -1068,12 +1068,6 @@ noncomputable def Set.BijOn.equiv {α : Type _} {β : Type _} {s : Set α} {t :
 #align set.bij_on.equiv Set.BijOn.equiv
 -/
 
-/- warning: dite_comp_equiv_update -> dite_comp_equiv_update is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} {β : Sort.{u2}} {γ : Sort.{u3}} {s : Set.{u1} α} (e : Equiv.{u2, succ u1} β (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s)) (v : β -> γ) (w : α -> γ) (j : β) (x : γ) [_inst_1 : DecidableEq.{u2} β] [_inst_2 : DecidableEq.{succ u1} α] [_inst_3 : forall (j : α), Decidable (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) j s)], Eq.{imax (succ u1) u3} (α -> γ) (fun (i : α) => dite.{u3} γ (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) i s) (_inst_3 i) (fun (h : Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) i s) => Function.update.{u2, u3} β (fun (ᾰ : β) => γ) (fun (a : β) (b : β) => _inst_1 a b) v j x (coeFn.{max 1 (imax (succ u1) u2) u2 (succ u1), imax (succ u1) u2} (Equiv.{succ u1, u2} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) β) (fun (_x : Equiv.{succ u1, u2} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) β) => (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) -> β) (Equiv.hasCoeToFun.{succ u1, u2} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) β) (Equiv.symm.{u2, succ u1} β (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) e) (Subtype.mk.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x s) i h))) (fun (h : Not (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) i s)) => w i)) (Function.update.{succ u1, u3} α (fun (i : α) => γ) (fun (a : α) (b : α) => _inst_2 a b) (fun (i : α) => dite.{u3} γ (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) i s) (_inst_3 i) (fun (h : Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) i s) => v (coeFn.{max 1 (imax (succ u1) u2) u2 (succ u1), imax (succ u1) u2} (Equiv.{succ u1, u2} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) β) (fun (_x : Equiv.{succ u1, u2} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) β) => (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) -> β) (Equiv.hasCoeToFun.{succ u1, u2} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) β) (Equiv.symm.{u2, succ u1} β (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) e) (Subtype.mk.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x s) i h))) (fun (h : Not (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) i s)) => w i)) ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) α (HasLiftT.mk.{succ u1, succ u1} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) α (CoeTCₓ.coe.{succ u1, succ u1} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) α (coeBase.{succ u1, succ u1} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) α (coeSubtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x s))))) (coeFn.{max 1 (max u2 (succ u1)) (imax (succ u1) u2), max u2 (succ u1)} (Equiv.{u2, succ u1} β (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s)) (fun (_x : Equiv.{u2, succ u1} β (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s)) => β -> (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s)) (Equiv.hasCoeToFun.{u2, succ u1} β (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s)) e j)) x)
-but is expected to have type
-  forall {α : Type.{u3}} {β : Sort.{u2}} {γ : Sort.{u1}} {s : Set.{u3} α} (e : Equiv.{u2, succ u3} β (Set.Elem.{u3} α s)) (v : β -> γ) (w : α -> γ) (j : β) (x : γ) [_inst_1 : DecidableEq.{u2} β] [_inst_2 : DecidableEq.{succ u3} α] [_inst_3 : forall (j : α), Decidable (Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) j s)], Eq.{imax (succ u3) u1} (α -> γ) (fun (i : α) => dite.{u1} γ (Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) i s) (_inst_3 i) (fun (h : Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) i s) => Function.update.{u2, u1} β (fun (ᾰ : β) => γ) (fun (a : β) (b : β) => _inst_1 a b) v j x (FunLike.coe.{max (succ u3) u2, succ u3, u2} (Equiv.{succ u3, u2} (Set.Elem.{u3} α s) β) (Set.Elem.{u3} α s) (fun (_x : Set.Elem.{u3} α s) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : Set.Elem.{u3} α s) => β) _x) (Equiv.instFunLikeEquiv.{succ u3, u2} (Set.Elem.{u3} α s) β) (Equiv.symm.{u2, succ u3} β (Set.Elem.{u3} α s) e) (Subtype.mk.{succ u3} α (fun (x : α) => Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) x s) i h))) (fun (h : Not (Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) i s)) => w i)) (Function.update.{succ u3, u1} α (fun (i : α) => γ) (fun (a : α) (b : α) => _inst_2 a b) (fun (i : α) => dite.{u1} γ (Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) i s) (_inst_3 i) (fun (h : Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) i s) => v (FunLike.coe.{max (succ u3) u2, succ u3, u2} (Equiv.{succ u3, u2} (Set.Elem.{u3} α s) β) (Set.Elem.{u3} α s) (fun (_x : Set.Elem.{u3} α s) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : Set.Elem.{u3} α s) => β) _x) (Equiv.instFunLikeEquiv.{succ u3, u2} (Set.Elem.{u3} α s) β) (Equiv.symm.{u2, succ u3} β (Set.Elem.{u3} α s) e) (Subtype.mk.{succ u3} α (fun (x : α) => Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) x s) i h))) (fun (h : Not (Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) i s)) => w i)) (Subtype.val.{succ u3} α (fun (x : α) => Membership.mem.{u3, u3} α (Set.{u3} α) (Set.instMembershipSet.{u3} α) x s) (FunLike.coe.{max (succ u3) u2, u2, succ u3} (Equiv.{u2, succ u3} β (Set.Elem.{u3} α s)) β (fun (_x : β) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : β) => Set.Elem.{u3} α s) _x) (Equiv.instFunLikeEquiv.{u2, succ u3} β (Set.Elem.{u3} α s)) e j)) x)
-Case conversion may be inaccurate. Consider using '#align dite_comp_equiv_update dite_comp_equiv_updateₓ'. -/
 /-- The composition of an updated function with an equiv on a subset can be expressed as an
 updated function. -/
 theorem dite_comp_equiv_update {α : Type _} {β : Sort _} {γ : Sort _} {s : Set α} (e : β ≃ s)
@@ -1093,5 +1087,5 @@ theorem dite_comp_equiv_update {α : Type _} {β : Sort _} {γ : Sort _} {s : Se
       have : (e j : α) ∈ s := (e j).2
       rwa [← h] at this
     simp [h, this]
-#align dite_comp_equiv_update dite_comp_equiv_update
+#align dite_comp_equiv_update dite_comp_equiv_updateₓ