bump to nightly-2023-04-20-08

mathlib commit leanprover-community/mathlib@730c6d4

Mathbin/Algebra/Algebra/Operations.lean

@@ -270,7 +270,7 @@ theorem mul_toAddSubmonoid (M N : Submodule R A) :
     (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid :=
   by
   dsimp [Mul.mul]
-  simp_rw [← LinearMap.mulLeft_toAddMonoid_hom R, LinearMap.mulLeft, ← map_to_add_submonoid _ N,
+  simp_rw [← LinearMap.mulLeft_toAddMonoidHom R, LinearMap.mulLeft, ← map_to_add_submonoid _ N,
     map₂]
   rw [supr_to_add_submonoid]
   rfl

Mathbin/Algebra/Module/Submodule/Basic.lean

@@ -580,15 +580,15 @@ variable {α β : Type _}
 instance [VAdd M α] : VAdd p α :=
   p.toAddSubmonoid.VAdd
 
-/- warning: submodule.vadd_comm_class -> Submodule.vAddCommClass is a dubious translation:
+/- warning: submodule.vadd_comm_class -> Submodule.vaddCommClass is a dubious translation:
 lean 3 declaration is
   forall {R : Type.{u1}} {M : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : AddCommMonoid.{u2} M] {module_M : Module.{u1, u2} R M _inst_1 _inst_2} (p : Submodule.{u1, u2} R M _inst_1 _inst_2 module_M) {α : Type.{u3}} {β : Type.{u4}} [_inst_3 : VAdd.{u2, u4} M β] [_inst_4 : VAdd.{u3, u4} α β] [_inst_5 : VAddCommClass.{u2, u3, u4} M α β _inst_3 _inst_4], VAddCommClass.{u2, u3, u4} (coeSort.{succ u2, succ (succ u2)} (Submodule.{u1, u2} R M _inst_1 _inst_2 module_M) Type.{u2} (SetLike.hasCoeToSort.{u2, u2} (Submodule.{u1, u2} R M _inst_1 _inst_2 module_M) M (Submodule.setLike.{u1, u2} R M _inst_1 _inst_2 module_M)) p) α β (Submodule.hasVadd.{u1, u2, u4} R M _inst_1 _inst_2 module_M p β _inst_3) _inst_4
 but is expected to have type
   forall {R : Type.{u1}} {M : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : AddCommMonoid.{u2} M] {module_M : Module.{u1, u2} R M _inst_1 _inst_2} (p : Submodule.{u1, u2} R M _inst_1 _inst_2 module_M) {α : Type.{u3}} {β : Type.{u4}} [_inst_3 : VAdd.{u2, u4} M β] [_inst_4 : VAdd.{u3, u4} α β] [_inst_5 : VAddCommClass.{u2, u3, u4} M α β _inst_3 _inst_4], VAddCommClass.{u2, u3, u4} (Subtype.{succ u2} M (fun (x : M) => Membership.mem.{u2, u2} M (Submodule.{u1, u2} R M _inst_1 _inst_2 module_M) (SetLike.instMembership.{u2, u2} (Submodule.{u1, u2} R M _inst_1 _inst_2 module_M) M (Submodule.setLike.{u1, u2} R M _inst_1 _inst_2 module_M)) x p)) α β (Submodule.instVAddSubtypeMemSubmoduleInstMembershipSetLike.{u1, u2, u4} R M _inst_1 _inst_2 module_M p β _inst_3) _inst_4
-Case conversion may be inaccurate. Consider using '#align submodule.vadd_comm_class Submodule.vAddCommClassₓ'. -/
-instance vAddCommClass [VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCommClass p α β :=
+Case conversion may be inaccurate. Consider using '#align submodule.vadd_comm_class Submodule.vaddCommClassₓ'. -/
+instance vaddCommClass [VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCommClass p α β :=
   ⟨fun a => (vadd_comm (a : M) : _)⟩
-#align submodule.vadd_comm_class Submodule.vAddCommClass
+#align submodule.vadd_comm_class Submodule.vaddCommClass
 
 instance [VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd p α :=
   ⟨fun x y h => Subtype.ext <| eq_of_vadd_eq_vadd h⟩

Mathbin/Analysis/BoxIntegral/Box/SubboxInduction.lean

@@ -207,8 +207,8 @@ theorem subbox_induction_on' {p : Box ι → Prop} (I : Box ι)
     mem_Inter.1
       (csupᵢ_mem_Inter_Icc_of_antitone_Icc ((@box.Icc ι).Monotone.comp_antitone hJmono) fun m =>
         (J m).lower_le_upper)
-  have hJl_mem : ∀ m, (J m).lower ∈ I.Icc := fun m => le_iff_Icc.1 (hJle m) (J m).lower_mem_icc
-  have hJu_mem : ∀ m, (J m).upper ∈ I.Icc := fun m => le_iff_Icc.1 (hJle m) (J m).upper_mem_icc
+  have hJl_mem : ∀ m, (J m).lower ∈ I.Icc := fun m => le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
+  have hJu_mem : ∀ m, (J m).upper ∈ I.Icc := fun m => le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
   have hJlz : tendsto (fun m => (J m).lower) at_top (𝓝 z) :=
     tendsto_atTop_csupᵢ (antitone_lower.comp hJmono) ⟨I.upper, fun x ⟨m, hm⟩ => hm ▸ (hJl_mem m).2⟩
   have hJuz : tendsto (fun m => (J m).upper) at_top (𝓝 z) :=

Mathbin/Analysis/BoxIntegral/Partition/Measure.lean

@@ -50,7 +50,7 @@ theorem measure_Icc_lt_top (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure 
 #align box_integral.box.measure_Icc_lt_top BoxIntegral.Box.measure_Icc_lt_top
 
 theorem measure_coe_lt_top (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] : μ I < ∞ :=
-  (measure_mono <| coe_subset_icc).trans_lt (I.measure_Icc_lt_top μ)
+  (measure_mono <| coe_subset_Icc).trans_lt (I.measure_Icc_lt_top μ)
 #align box_integral.box.measure_coe_lt_top BoxIntegral.Box.measure_coe_lt_top
 
 section Countable

Mathbin/Analysis/BoxIntegral/Partition/Tagged.lean

@@ -134,7 +134,7 @@ def bUnionTagged (π : Prepartition I) (πi : ∀ J, TaggedPrepartition J) : Tag
     where
   toPrepartition := π.bunionᵢ fun J => (πi J).toPrepartition
   Tag J := (πi (π.bUnionIndex (fun J => (πi J).toPrepartition) J)).Tag J
-  tag_mem_Icc J := Box.le_iff_icc.1 (π.bUnionIndex_le _ _) ((πi _).tag_mem_Icc _)
+  tag_mem_Icc J := Box.le_iff_Icc.1 (π.bUnionIndex_le _ _) ((πi _).tag_mem_Icc _)
 #align box_integral.prepartition.bUnion_tagged BoxIntegral.Prepartition.bUnionTagged
 
 @[simp]
@@ -270,7 +270,7 @@ theorem isSubordinate_bUnionTagged [Fintype ι] {π : Prepartition I}
 
 theorem IsSubordinate.bUnionPrepartition [Fintype ι] (h : IsSubordinate π r)
     (πi : ∀ J, Prepartition J) : IsSubordinate (π.bUnionPrepartition πi) r := fun J hJ =>
-  Subset.trans (Box.le_iff_icc.1 <| π.toPrepartition.le_bUnionIndex hJ) <|
+  Subset.trans (Box.le_iff_Icc.1 <| π.toPrepartition.le_bUnionIndex hJ) <|
     h _ <| π.toPrepartition.bUnionIndex_mem hJ
 #align box_integral.tagged_prepartition.is_subordinate.bUnion_prepartition BoxIntegral.TaggedPrepartition.IsSubordinate.bUnionPrepartition
 
@@ -309,7 +309,7 @@ theorem mem_single {J'} (hJ : J ≤ I) (h : x ∈ I.Icc) : J' ∈ single I J hJ
 #align box_integral.tagged_prepartition.mem_single BoxIntegral.TaggedPrepartition.mem_single
 
 instance (I : Box ι) : Inhabited (TaggedPrepartition I) :=
-  ⟨single I I le_rfl I.upper I.upper_mem_icc⟩
+  ⟨single I I le_rfl I.upper I.upper_mem_Icc⟩
 
 theorem isPartition_single_iff (hJ : J ≤ I) (h : x ∈ I.Icc) :
     (single I J hJ x h).IsPartition ↔ J = I :=
@@ -412,7 +412,7 @@ def embedBox (I J : Box ι) (h : I ≤ J) : TaggedPrepartition I ↪ TaggedPrepa
   toFun π :=
     { π with
       le_of_mem' := fun J' hJ' => (π.le_of_mem' J' hJ').trans h
-      tag_mem_Icc := fun J => Box.le_iff_icc.1 h (π.tag_mem_Icc J) }
+      tag_mem_Icc := fun J => Box.le_iff_Icc.1 h (π.tag_mem_Icc J) }
   inj' := by
     rintro ⟨⟨b₁, h₁le, h₁d⟩, t₁, ht₁⟩ ⟨⟨b₂, h₂le, h₂d⟩, t₂, ht₂⟩ H
     simpa using H

Mathbin/Data/Bitvec/Basic.lean

@@ -18,28 +18,39 @@ namespace Bitvec
 instance (n : ℕ) : Preorder (Bitvec n) :=
   Preorder.lift Bitvec.toNat
 
+#print Bitvec.ofFin /-
 /-- convert `fin` to `bitvec` -/
 def ofFin {n : ℕ} (i : Fin <| 2 ^ n) : Bitvec n :=
   Bitvec.ofNat _ i.val
 #align bitvec.of_fin Bitvec.ofFin
+-/
 
+#print Bitvec.ofFin_val /-
 theorem ofFin_val {n : ℕ} (i : Fin <| 2 ^ n) : (ofFin i).toNat = i.val := by
   rw [of_fin, to_nat_of_nat, Nat.mod_eq_of_lt] <;> apply i.is_lt
 #align bitvec.of_fin_val Bitvec.ofFin_val
+-/
 
+#print Bitvec.toFin /-
 /-- convert `bitvec` to `fin` -/
 def toFin {n : ℕ} (i : Bitvec n) : Fin <| 2 ^ n :=
   i.toNat
 #align bitvec.to_fin Bitvec.toFin
+-/
 
+#print Bitvec.addLsb_eq_twice_add_one /-
 theorem addLsb_eq_twice_add_one {x b} : addLsb x b = 2 * x + cond b 1 0 := by
   simp [add_lsb, two_mul]
 #align bitvec.add_lsb_eq_twice_add_one Bitvec.addLsb_eq_twice_add_one
+-/
 
+#print Bitvec.toNat_eq_foldr_reverse /-
 theorem toNat_eq_foldr_reverse {n : ℕ} (v : Bitvec n) :
     v.toNat = v.toList.reverse.foldr (flip addLsb) 0 := by rw [List.foldr_reverse, flip] <;> rfl
 #align bitvec.to_nat_eq_foldr_reverse Bitvec.toNat_eq_foldr_reverse
+-/
 
+#print Bitvec.toNat_lt /-
 theorem toNat_lt {n : ℕ} (v : Bitvec n) : v.toNat < 2 ^ n :=
   by
   suffices v.to_nat + 1 ≤ 2 ^ n by simpa
@@ -63,21 +74,31 @@ theorem toNat_lt {n : ℕ} (v : Bitvec n) : v.toNat < 2 ^ n :=
       exact ys_ih rfl
       norm_num
 #align bitvec.to_nat_lt Bitvec.toNat_lt
+-/
 
+#print Bitvec.addLsb_div_two /-
 theorem addLsb_div_two {x b} : addLsb x b / 2 = x := by
   cases b <;>
       simp only [Nat.add_mul_div_left, add_lsb, ← two_mul, add_comm, Nat.succ_pos',
         Nat.mul_div_right, gt_iff_lt, zero_add, cond] <;>
     norm_num
 #align bitvec.add_lsb_div_two Bitvec.addLsb_div_two
+-/
 
+/- warning: bitvec.to_bool_add_lsb_mod_two -> Bitvec.decide_addLsb_mod_two is a dubious translation:
+lean 3 declaration is
+  forall {x : Nat} {b : Bool}, Eq.{1} Bool (Decidable.decide (Eq.{1} Nat (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) (Bitvec.addLsb x b) (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))) (Nat.decidableEq (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) (Bitvec.addLsb x b) (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) b
+but is expected to have type
+  forall {x : Nat} {b : Bool}, Eq.{1} Bool (Decidable.decide (Eq.{1} Nat (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) (Bitvec.addLsb x b) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (instDecidableEqNat (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) (Bitvec.addLsb x b) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) b
+Case conversion may be inaccurate. Consider using '#align bitvec.to_bool_add_lsb_mod_two Bitvec.decide_addLsb_mod_twoₓ'. -/
 theorem decide_addLsb_mod_two {x b} : decide (addLsb x b % 2 = 1) = b := by
   cases b <;>
       simp only [Bool.decide_iff, Nat.add_mul_mod_self_left, add_lsb, ← two_mul, add_comm,
         Bool.decide_False, Nat.mul_mod_right, zero_add, cond, zero_ne_one] <;>
     norm_num
 #align bitvec.to_bool_add_lsb_mod_two Bitvec.decide_addLsb_mod_two
 
+#print Bitvec.ofNat_toNat /-
 theorem ofNat_toNat {n : ℕ} (v : Bitvec n) : Bitvec.ofNat _ v.toNat = v :=
   by
   cases' v with xs h
@@ -99,29 +120,40 @@ theorem ofNat_toNat {n : ℕ} (v : Bitvec n) : Bitvec.ofNat _ v.toNat = v :=
     apply ys_ih
     rfl
 #align bitvec.of_nat_to_nat Bitvec.ofNat_toNat
+-/
 
+#print Bitvec.toFin_val /-
 theorem toFin_val {n : ℕ} (v : Bitvec n) : (toFin v : ℕ) = v.toNat := by
   rw [to_fin, Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt] <;> apply to_nat_lt
 #align bitvec.to_fin_val Bitvec.toFin_val
+-/
 
+#print Bitvec.toFin_le_toFin_of_le /-
 theorem toFin_le_toFin_of_le {n} {v₀ v₁ : Bitvec n} (h : v₀ ≤ v₁) : v₀.toFin ≤ v₁.toFin :=
   show (v₀.toFin : ℕ) ≤ v₁.toFin by rw [to_fin_val, to_fin_val] <;> exact h
 #align bitvec.to_fin_le_to_fin_of_le Bitvec.toFin_le_toFin_of_le
+-/
 
+#print Bitvec.ofFin_le_ofFin_of_le /-
 theorem ofFin_le_ofFin_of_le {n : ℕ} {i j : Fin (2 ^ n)} (h : i ≤ j) : ofFin i ≤ ofFin j :=
   show (Bitvec.ofNat n i).toNat ≤ (Bitvec.ofNat n j).toNat
     by
     simp only [to_nat_of_nat, Nat.mod_eq_of_lt, Fin.is_lt]
     exact h
 #align bitvec.of_fin_le_of_fin_of_le Bitvec.ofFin_le_ofFin_of_le
+-/
 
+#print Bitvec.toFin_ofFin /-
 theorem toFin_ofFin {n} (i : Fin <| 2 ^ n) : (ofFin i).toFin = i :=
   Fin.eq_of_veq (by simp [to_fin_val, of_fin, to_nat_of_nat, Nat.mod_eq_of_lt, i.is_lt])
 #align bitvec.to_fin_of_fin Bitvec.toFin_ofFin
+-/
 
+#print Bitvec.ofFin_toFin /-
 theorem ofFin_toFin {n} (v : Bitvec n) : ofFin (toFin v) = v := by
   dsimp [of_fin] <;> rw [to_fin_val, of_nat_to_nat]
 #align bitvec.of_fin_to_fin Bitvec.ofFin_toFin
+-/
 
 end Bitvec