bump to nightly-2023-04-17-10

mathlib commit leanprover-community/mathlib@17ad94b

Mathbin/Data/Int/Cast/Lemmas.lean

@@ -625,7 +625,7 @@ end Pi
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} {γ : Type.{u3}} [_inst_1 : IntCast.{u3} γ] (n : Int), Eq.{max (max (succ u1) (succ u2)) (succ u3)} ((Sum.{u1, u2} α β) -> γ) (Sum.elim.{u1, u2, succ u3} α β γ ((fun (a : Type) (b : Sort.{max (succ u1) (succ u3)}) [self : HasLiftT.{1, max (succ u1) (succ u3)} a b] => self.0) Int (α -> γ) (HasLiftT.mk.{1, max (succ u1) (succ u3)} Int (α -> γ) (CoeTCₓ.coe.{1, max (succ u1) (succ u3)} Int (α -> γ) (Int.castCoe.{max u1 u3} (α -> γ) (Pi.hasIntCast.{u1, u3} α (fun (ᾰ : α) => γ) (fun (i : α) => _inst_1))))) n) ((fun (a : Type) (b : Sort.{max (succ u2) (succ u3)}) [self : HasLiftT.{1, max (succ u2) (succ u3)} a b] => self.0) Int (β -> γ) (HasLiftT.mk.{1, max (succ u2) (succ u3)} Int (β -> γ) (CoeTCₓ.coe.{1, max (succ u2) (succ u3)} Int (β -> γ) (Int.castCoe.{max u2 u3} (β -> γ) (Pi.hasIntCast.{u2, u3} β (fun (ᾰ : β) => γ) (fun (i : β) => _inst_1))))) n)) ((fun (a : Type) (b : Sort.{max (max (succ u1) (succ u2)) (succ u3)}) [self : HasLiftT.{1, max (max (succ u1) (succ u2)) (succ u3)} a b] => self.0) Int ((Sum.{u1, u2} α β) -> γ) (HasLiftT.mk.{1, max (max (succ u1) (succ u2)) (succ u3)} Int ((Sum.{u1, u2} α β) -> γ) (CoeTCₓ.coe.{1, max (max (succ u1) (succ u2)) (succ u3)} Int ((Sum.{u1, u2} α β) -> γ) (Int.castCoe.{max (max u1 u2) u3} ((Sum.{u1, u2} α β) -> γ) (Pi.hasIntCast.{max u1 u2, u3} (Sum.{u1, u2} α β) (fun (ᾰ : Sum.{u1, u2} α β) => γ) (fun (i : Sum.{u1, u2} α β) => _inst_1))))) n)
 but is expected to have type
-  forall {α : Type.{u3}} {β : Type.{u2}} {γ : Type.{u1}} [_inst_1 : IntCast.{u1} γ] (n : Int), Eq.{max (max (succ u3) (succ u2)) (succ u1)} ((Sum.{u3, u2} α β) -> γ) (Sum.elim.{u3, u2, succ u1} α β γ (Int.cast.{max u3 u1} (α -> γ) (Pi.intCast.{u3, u1} α (fun (a._@.Mathlib.Data.Int.Cast.Lemmas._hyg.3011 : α) => γ) (fun (i : α) => _inst_1)) n) (Int.cast.{max u2 u1} (β -> γ) (Pi.intCast.{u2, u1} β (fun (a._@.Mathlib.Data.Int.Cast.Lemmas._hyg.3018 : β) => γ) (fun (i : β) => _inst_1)) n)) (Int.cast.{max (max u3 u2) u1} ((Sum.{u3, u2} α β) -> γ) (Pi.intCast.{max u3 u2, u1} (Sum.{u3, u2} α β) (fun (a._@.Mathlib.Data.Sum.Basic._hyg.1871 : Sum.{u3, u2} α β) => γ) (fun (i : Sum.{u3, u2} α β) => _inst_1)) n)
+  forall {α : Type.{u3}} {β : Type.{u2}} {γ : Type.{u1}} [_inst_1 : IntCast.{u1} γ] (n : Int), Eq.{max (max (succ u3) (succ u2)) (succ u1)} ((Sum.{u3, u2} α β) -> γ) (Sum.elim.{u3, u2, succ u1} α β γ (Int.cast.{max u3 u1} (α -> γ) (Pi.intCast.{u3, u1} α (fun (a._@.Mathlib.Data.Int.Cast.Lemmas._hyg.3012 : α) => γ) (fun (i : α) => _inst_1)) n) (Int.cast.{max u2 u1} (β -> γ) (Pi.intCast.{u2, u1} β (fun (a._@.Mathlib.Data.Int.Cast.Lemmas._hyg.3019 : β) => γ) (fun (i : β) => _inst_1)) n)) (Int.cast.{max (max u3 u2) u1} ((Sum.{u3, u2} α β) -> γ) (Pi.intCast.{max u3 u2, u1} (Sum.{u3, u2} α β) (fun (a._@.Mathlib.Data.Sum.Basic._hyg.1871 : Sum.{u3, u2} α β) => γ) (fun (i : Sum.{u3, u2} α β) => _inst_1)) n)
 Case conversion may be inaccurate. Consider using '#align sum.elim_int_cast_int_cast Sum.elim_intCast_intCastₓ'. -/
 theorem Sum.elim_intCast_intCast {α β γ : Type _} [IntCast γ] (n : ℤ) :
     Sum.elim (n : α → γ) (n : β → γ) = n :=

Mathbin/GroupTheory/OrderOfElement.lean

@@ -58,7 +58,7 @@ section IsOfFinOrder
 lean 3 declaration is
   forall {G : Type.{u1}} {n : Nat} [_inst_1 : Monoid.{u1} G] (x : G), Iff (Function.IsPeriodicPt.{u1} G (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toHasMul.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1))) x) n (OfNat.ofNat.{u1} G 1 (OfNat.mk.{u1} G 1 (One.one.{u1} G (MulOneClass.toHasOne.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1)))))) (Eq.{succ u1} G (HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G _inst_1)) x n) (OfNat.ofNat.{u1} G 1 (OfNat.mk.{u1} G 1 (One.one.{u1} G (MulOneClass.toHasOne.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1))))))
 but is expected to have type
-  forall {G : Type.{u1}} {n : Nat} [_inst_1 : Monoid.{u1} G] (x : G), Iff (Function.IsPeriodicPt.{u1} G ((fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.83 : G) (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.85 : G) => HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toMul.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1))) x._@.Mathlib.GroupTheory.OrderOfElement._hyg.83 x._@.Mathlib.GroupTheory.OrderOfElement._hyg.85) x) n (OfNat.ofNat.{u1} G 1 (One.toOfNat1.{u1} G (Monoid.toOne.{u1} G _inst_1)))) (Eq.{succ u1} G (HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G _inst_1)) x n) (OfNat.ofNat.{u1} G 1 (One.toOfNat1.{u1} G (Monoid.toOne.{u1} G _inst_1))))
+  forall {G : Type.{u1}} {n : Nat} [_inst_1 : Monoid.{u1} G] (x : G), Iff (Function.IsPeriodicPt.{u1} G ((fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.82 : G) (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.84 : G) => HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toMul.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1))) x._@.Mathlib.GroupTheory.OrderOfElement._hyg.82 x._@.Mathlib.GroupTheory.OrderOfElement._hyg.84) x) n (OfNat.ofNat.{u1} G 1 (One.toOfNat1.{u1} G (Monoid.toOne.{u1} G _inst_1)))) (Eq.{succ u1} G (HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G _inst_1)) x n) (OfNat.ofNat.{u1} G 1 (One.toOfNat1.{u1} G (Monoid.toOne.{u1} G _inst_1))))
 Case conversion may be inaccurate. Consider using '#align is_periodic_pt_mul_iff_pow_eq_one isPeriodicPt_mul_iff_pow_eq_oneₓ'. -/
 @[to_additive]
 theorem isPeriodicPt_mul_iff_pow_eq_one (x : G) : IsPeriodicPt ((· * ·) x) n 1 ↔ x ^ n = 1 := by
@@ -718,7 +718,7 @@ theorem pow_injective_of_lt_orderOf (hn : n < orderOf x) (hm : m < orderOf x) (e
 lean 3 declaration is
   forall {G : Type.{u1}} (x : G) (y : G) [_inst_1 : LeftCancelMonoid.{u1} G] [_inst_2 : DecidableEq.{succ u1} G], (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero))) (orderOf.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x)) -> (Iff (Membership.Mem.{u1, u1} G (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) (SetLike.hasMem.{u1, u1} (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) G (Submonoid.setLike.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1)))) y (Submonoid.powers.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x)) (Membership.Mem.{u1, u1} G (Finset.{u1} G) (Finset.hasMem.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_2 a b) (HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) x) (Finset.range (orderOf.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x)))))
 but is expected to have type
-  forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : Monoid.{u1} G] [_inst_2 : DecidableEq.{succ u1} G], (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (orderOf.{u1} G _inst_1 x)) -> (Iff (Membership.mem.{u1, u1} G (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1)) (SetLike.instMembership.{u1, u1} (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1)) G (Submonoid.instSetLikeSubmonoid.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1))) y (Submonoid.powers.{u1} G _inst_1 x)) (Membership.mem.{u1, u1} G (Finset.{u1} G) (Finset.instMembershipFinset.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_2 a b) (fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.2063 : Nat) => HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G _inst_1)) x x._@.Mathlib.GroupTheory.OrderOfElement._hyg.2063) (Finset.range (orderOf.{u1} G _inst_1 x)))))
+  forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : Monoid.{u1} G] [_inst_2 : DecidableEq.{succ u1} G], (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (orderOf.{u1} G _inst_1 x)) -> (Iff (Membership.mem.{u1, u1} G (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1)) (SetLike.instMembership.{u1, u1} (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1)) G (Submonoid.instSetLikeSubmonoid.{u1} G (Monoid.toMulOneClass.{u1} G _inst_1))) y (Submonoid.powers.{u1} G _inst_1 x)) (Membership.mem.{u1, u1} G (Finset.{u1} G) (Finset.instMembershipFinset.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_2 a b) (fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.2062 : Nat) => HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G _inst_1)) x x._@.Mathlib.GroupTheory.OrderOfElement._hyg.2062) (Finset.range (orderOf.{u1} G _inst_1 x)))))
 Case conversion may be inaccurate. Consider using '#align mem_powers_iff_mem_range_order_of' mem_powers_iff_mem_range_order_of'ₓ'. -/
 @[to_additive mem_multiples_iff_mem_range_addOrderOf']
 theorem mem_powers_iff_mem_range_order_of' [DecidableEq G] (hx : 0 < orderOf x) :
@@ -1111,7 +1111,7 @@ theorem orderOf_pow [Finite G] (x : G) : orderOf (x ^ n) = orderOf x / gcd (orde
 lean 3 declaration is
   forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : LeftCancelMonoid.{u1} G] [_inst_3 : Finite.{succ u1} G] [_inst_4 : DecidableEq.{succ u1} G], Iff (Membership.Mem.{u1, u1} G (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) (SetLike.hasMem.{u1, u1} (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) G (Submonoid.setLike.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1)))) y (Submonoid.powers.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x)) (Membership.Mem.{u1, u1} G (Finset.{u1} G) (Finset.hasMem.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_4 a b) (HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) x) (Finset.range (orderOf.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x))))
 but is expected to have type
-  forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : LeftCancelMonoid.{u1} G] [_inst_3 : Finite.{succ u1} G] [_inst_4 : DecidableEq.{succ u1} G], Iff (Membership.mem.{u1, u1} G (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) (SetLike.instMembership.{u1, u1} (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) G (Submonoid.instSetLikeSubmonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1)))) y (Submonoid.powers.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x)) (Membership.mem.{u1, u1} G (Finset.{u1} G) (Finset.instMembershipFinset.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_4 a b) ((fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6916 : G) (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6918 : Nat) => HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6916 x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6918) x) (Finset.range (orderOf.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x))))
+  forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : LeftCancelMonoid.{u1} G] [_inst_3 : Finite.{succ u1} G] [_inst_4 : DecidableEq.{succ u1} G], Iff (Membership.mem.{u1, u1} G (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) (SetLike.instMembership.{u1, u1} (Submonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) G (Submonoid.instSetLikeSubmonoid.{u1} G (Monoid.toMulOneClass.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1)))) y (Submonoid.powers.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x)) (Membership.mem.{u1, u1} G (Finset.{u1} G) (Finset.instMembershipFinset.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_4 a b) ((fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6915 : G) (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6917 : Nat) => HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1))) x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6915 x._@.Mathlib.GroupTheory.OrderOfElement._hyg.6917) x) (Finset.range (orderOf.{u1} G (LeftCancelMonoid.toMonoid.{u1} G _inst_1) x))))
 Case conversion may be inaccurate. Consider using '#align mem_powers_iff_mem_range_order_of mem_powers_iff_mem_range_orderOfₓ'. -/
 @[to_additive mem_multiples_iff_mem_range_addOrderOf]
 theorem mem_powers_iff_mem_range_orderOf [Finite G] [DecidableEq G] :
@@ -1273,7 +1273,7 @@ theorem powers_eq_zpowers [Finite G] (x : G) : (Submonoid.powers x : Set G) = zp
 lean 3 declaration is
   forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : Group.{u1} G] [_inst_3 : Finite.{succ u1} G] [_inst_4 : DecidableEq.{succ u1} G], Iff (Membership.Mem.{u1, u1} G (Subgroup.{u1} G _inst_1) (SetLike.hasMem.{u1, u1} (Subgroup.{u1} G _inst_1) G (Subgroup.setLike.{u1} G _inst_1)) y (Subgroup.zpowers.{u1} G _inst_1 x)) (Membership.Mem.{u1, u1} G (Finset.{u1} G) (Finset.hasMem.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_4 a b) (HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)))) x) (Finset.range (orderOf.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)) x))))
 but is expected to have type
-  forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : Group.{u1} G] [_inst_3 : Finite.{succ u1} G] [_inst_4 : DecidableEq.{succ u1} G], Iff (Membership.mem.{u1, u1} G (Subgroup.{u1} G _inst_1) (SetLike.instMembership.{u1, u1} (Subgroup.{u1} G _inst_1) G (Subgroup.instSetLikeSubgroup.{u1} G _inst_1)) y (Subgroup.zpowers.{u1} G _inst_1 x)) (Membership.mem.{u1, u1} G (Finset.{u1} G) (Finset.instMembershipFinset.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_4 a b) ((fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7973 : G) (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7975 : Nat) => HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)))) x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7973 x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7975) x) (Finset.range (orderOf.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)) x))))
+  forall {G : Type.{u1}} {x : G} {y : G} [_inst_1 : Group.{u1} G] [_inst_3 : Finite.{succ u1} G] [_inst_4 : DecidableEq.{succ u1} G], Iff (Membership.mem.{u1, u1} G (Subgroup.{u1} G _inst_1) (SetLike.instMembership.{u1, u1} (Subgroup.{u1} G _inst_1) G (Subgroup.instSetLikeSubgroup.{u1} G _inst_1)) y (Subgroup.zpowers.{u1} G _inst_1 x)) (Membership.mem.{u1, u1} G (Finset.{u1} G) (Finset.instMembershipFinset.{u1} G) y (Finset.image.{0, u1} Nat G (fun (a : G) (b : G) => _inst_4 a b) ((fun (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7972 : G) (x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7974 : Nat) => HPow.hPow.{u1, 0, u1} G Nat G (instHPow.{u1, 0} G Nat (Monoid.Pow.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)))) x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7972 x._@.Mathlib.GroupTheory.OrderOfElement._hyg.7974) x) (Finset.range (orderOf.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)) x))))
 Case conversion may be inaccurate. Consider using '#align mem_zpowers_iff_mem_range_order_of mem_zpowers_iff_mem_range_orderOfₓ'. -/
 @[to_additive mem_zmultiples_iff_mem_range_addOrderOf]
 theorem mem_zpowers_iff_mem_range_orderOf [Finite G] [DecidableEq G] :

Mathbin/Order/Category/BddDistLat.lean

@@ -27,7 +27,7 @@ open CategoryTheory
 
 /-- The category of bounded distributive lattices with bounded lattice morphisms. -/
 structure BddDistLat where
-  toDistLat : DistLat
+  toDistLat : DistLatCat
   [isBoundedOrder : BoundedOrder to_DistLat]
 #align BddDistLat BddDistLat
 
@@ -70,7 +70,7 @@ instance : LargeCategory.{u} BddDistLat :=
 instance : ConcreteCategory BddDistLat :=
   InducedCategory.concreteCategory toBddLat
 
-instance hasForgetToDistLat : HasForget₂ BddDistLat DistLat
+instance hasForgetToDistLat : HasForget₂ BddDistLat DistLatCat
     where forget₂ :=
     { obj := fun X => ⟨X⟩
       map := fun X Y => BoundedLatticeHom.toLatticeHom }
@@ -80,11 +80,11 @@ instance hasForgetToBddLat : HasForget₂ BddDistLat BddLat :=
   InducedCategory.hasForget₂ toBddLat
 #align BddDistLat.has_forget_to_BddLat BddDistLat.hasForgetToBddLat
 
-theorem forget_bddLat_latCat_eq_forget_distLat_latCat :
+theorem forget_bddLat_latCat_eq_forget_distLatCat_latCat :
     forget₂ BddDistLat BddLat ⋙ forget₂ BddLat LatCat =
-      forget₂ BddDistLat DistLat ⋙ forget₂ DistLat LatCat :=
+      forget₂ BddDistLat DistLatCat ⋙ forget₂ DistLatCat LatCat :=
   rfl
-#align BddDistLat.forget_BddLat_Lat_eq_forget_DistLat_Lat BddDistLat.forget_bddLat_latCat_eq_forget_distLat_latCat
+#align BddDistLat.forget_BddLat_Lat_eq_forget_DistLat_Lat BddDistLat.forget_bddLat_latCat_eq_forget_distLatCat_latCat
 
 /-- Constructs an equivalence between bounded distributive lattices from an order isomorphism
 between them. -/
@@ -118,8 +118,9 @@ def dualEquiv : BddDistLat ≌ BddDistLat :=
 
 end BddDistLat
 
-theorem bddDistLat_dual_comp_forget_to_distLat :
-    BddDistLat.dual ⋙ forget₂ BddDistLat DistLat = forget₂ BddDistLat DistLat ⋙ DistLat.dual :=
+theorem bddDistLat_dual_comp_forget_to_distLatCat :
+    BddDistLat.dual ⋙ forget₂ BddDistLat DistLatCat =
+      forget₂ BddDistLat DistLatCat ⋙ DistLatCat.dual :=
   rfl
-#align BddDistLat_dual_comp_forget_to_DistLat bddDistLat_dual_comp_forget_to_distLat
+#align BddDistLat_dual_comp_forget_to_DistLat bddDistLat_dual_comp_forget_to_distLatCat