feat(*): bump to lean 3.48.0 (#16292)

`fin n` is a structure now.

archive/imo/imo1987_q1.lean

@@ -66,7 +66,7 @@ def fixed_points_equiv' :
   inv_fun := λ p,
     ⟨⟨card (fixed_points p.1.2), (card_subtype_le _).trans_lt (nat.lt_succ_self _)⟩,
      ⟨p.1.2, rfl⟩, ⟨p.1.1, p.2⟩⟩,
-  left_inv := λ ⟨⟨k, hk⟩, ⟨σ, hσ⟩, ⟨x, hx⟩⟩, by { simp only [mem_fiber, subtype.coe_mk] at hσ,
+  left_inv := λ ⟨⟨k, hk⟩, ⟨σ, hσ⟩, ⟨x, hx⟩⟩, by { simp only [mem_fiber, fin.coe_mk] at hσ,
     subst k, refl },
   right_inv := λ ⟨⟨x, σ⟩, h⟩, rfl }
 

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.47.0"
+lean_version = "leanprover-community/lean:3.48.0"
 path = "src"
 
 [dependencies]

src/algebra/big_operators/fin.lean

@@ -222,7 +222,7 @@ begin
     rw prod_take_succ _ _ this,
     have A : ((finset.univ : finset (fin n)).filter (λ j, j.val < i + 1))
       = ((finset.univ : finset (fin n)).filter (λ j, j.val < i)) ∪ {(⟨i, h⟩ : fin n)},
-        by { ext j, simp [nat.lt_succ_iff_lt_or_eq, fin.ext_iff, - add_comm] },
+        by { ext ⟨_, _⟩, simp [nat.lt_succ_iff_lt_or_eq] },
     have B : _root_.disjoint (finset.filter (λ (j : fin n), j.val < i) finset.univ)
       (singleton (⟨i, h⟩ : fin n)), by simp,
     rw [A, finset.prod_union B, IH],

src/algebra/char_zero/quotient.lean

@@ -31,7 +31,7 @@ begin
     refine ⟨⟨(k % z).to_nat, _⟩, k / z, _⟩,
     { rw [←int.coe_nat_lt, int.to_nat_of_nonneg (int.mod_nonneg _ hz)],
       exact (int.mod_lt _ hz).trans_eq (int.abs_eq_nat_abs _) },
-    rw [subtype.coe_mk, int.to_nat_of_nonneg (int.mod_nonneg _ hz), int.div_add_mod] },
+    rw [fin.coe_mk, int.to_nat_of_nonneg (int.mod_nonneg _ hz), int.div_add_mod] },
   { rintro ⟨k, n, h⟩,
     exact ⟨_, h⟩, },
 end

src/algebraic_topology/simplex_category.lean

@@ -193,7 +193,7 @@ begin
   rcases i with ⟨i, _⟩,
   rcases j with ⟨j, _⟩,
   rcases k with ⟨k, _⟩,
-  simp only [subtype.mk_le_mk, fin.cast_succ_mk] at H,
+  simp only [fin.mk_le_mk, fin.cast_succ_mk] at H,
   dsimp,
   split_ifs,
   -- Most of the goals can now be handled by `linarith`,
@@ -241,28 +241,28 @@ begin
   rcases i with ⟨i, _⟩,
   rcases j with ⟨j, _⟩,
   rcases k with ⟨k, _⟩,
-  simp only [subtype.mk_lt_mk, fin.cast_succ_mk] at H,
+  simp only [fin.mk_lt_mk, fin.cast_succ_mk] at H,
   suffices : ite (_ < ite (k < i + 1) _ _) _ _ =
     ite _ (ite (j < k) (k - 1) k) (ite (j < k) (k - 1) k + 1),
   { simpa [apply_dite fin.cast_succ, fin.pred_above] with push_cast, },
   split_ifs,
   -- Most of the goals can now be handled by `linarith`,
   -- but we have to deal with three of them by hand.
   swap 2,
-  { simp only [subtype.mk_lt_mk] at h_1,
+  { simp only [fin.mk_lt_mk] at h_1,
     simp only [not_lt] at h_2,
     simp only [self_eq_add_right, one_ne_zero],
     exact lt_irrefl (k - 1) (lt_of_lt_of_le
       (nat.pred_lt (ne_of_lt (lt_of_le_of_lt (zero_le _) h_1)).symm)
       (le_trans (nat.le_of_lt_succ h) h_2)) },
   swap 4,
-  { simp only [subtype.mk_lt_mk] at h_1,
+  { simp only [fin.mk_lt_mk] at h_1,
     simp only [not_lt] at h,
     simp only [nat.add_succ_sub_one, add_zero],
     exfalso,
     exact lt_irrefl _ (lt_of_le_of_lt (nat.le_pred_of_lt (nat.lt_of_succ_le h)) h_3), },
   swap 4,
-  { simp only [subtype.mk_lt_mk] at h_1,
+  { simp only [fin.mk_lt_mk] at h_1,
     simp only [not_lt] at h_3,
     simp only [nat.add_succ_sub_one, add_zero],
     exact (nat.succ_pred_eq_of_pos (lt_of_le_of_lt (zero_le _) h_2)).symm, },
@@ -281,7 +281,7 @@ begin
   rcases i with ⟨i, _⟩,
   rcases j with ⟨j, _⟩,
   rcases k with ⟨k, _⟩,
-  simp only [subtype.mk_le_mk] at H,
+  simp only [fin.mk_le_mk] at H,
   -- At this point `simp with push_cast` makes good progress, but neither `simp?` nor `squeeze_simp`
   -- return usable sets of lemmas.
   -- To avoid using a non-terminal simp, we make a `suffices` statement indicating the shape

src/algebraic_topology/split_simplicial_object.lean

@@ -89,7 +89,7 @@ begin
   induction Δ₁ using opposite.rec,
   induction Δ₂ using opposite.rec,
   simp only at h₁,
-  have h₂ : Δ₁ = Δ₂ := by { ext1, simpa only [subtype.mk_eq_mk] using h₁.1, },
+  have h₂ : Δ₁ = Δ₂ := by { ext1, simpa only [fin.mk_eq_mk] using h₁.1, },
   subst h₂,
   refine ext _ _ rfl _,
   ext : 2,

src/algebraic_topology/topological_simplex.lean

@@ -40,8 +40,7 @@ lemma to_Top_obj.ext {x : simplex_category} (f g : x.to_Top_obj) :
 def to_Top_map {x y : simplex_category} (f : x ⟶ y) : x.to_Top_obj → y.to_Top_obj :=
 λ g, ⟨λ i, ∑ j in (finset.univ.filter (λ k, f k = i)), g j,
 begin
-  dsimp [to_Top_obj],
-  simp only [finset.filter_congr_decidable, finset.sum_congr],
+  simp only [finset.filter_congr_decidable, finset.sum_congr, to_Top_obj, set.mem_set_of],
   rw ← finset.sum_bUnion,
   convert g.2,
   { rw finset.eq_univ_iff_forall,

src/analysis/complex/upper_half_plane/basic.lean

@@ -154,7 +154,7 @@ begin
   change _ = (_ * (_ / _) + _) * _,
   field_simp [denom_ne_zero, -denom, -num],
   simp only [matrix.mul, dot_product, fin.sum_univ_succ, denom, num, coe_coe, subgroup.coe_mul,
-    general_linear_group.coe_mul, fintype.univ_of_subsingleton, fin.mk_eq_subtype_mk, fin.mk_zero,
+    general_linear_group.coe_mul, fintype.univ_of_subsingleton, fin.mk_zero,
     finset.sum_singleton, fin.succ_zero_eq_one, complex.of_real_add, complex.of_real_mul],
   ring
 end
@@ -167,7 +167,7 @@ begin
   rw denom_cocycle,
   field_simp [denom_ne_zero, -denom, -num],
   simp only [matrix.mul, dot_product, fin.sum_univ_succ, num, denom, coe_coe, subgroup.coe_mul,
-    general_linear_group.coe_mul, fintype.univ_of_subsingleton, fin.mk_eq_subtype_mk, fin.mk_zero,
+    general_linear_group.coe_mul, fintype.univ_of_subsingleton, fin.mk_zero,
     finset.sum_singleton, fin.succ_zero_eq_one, complex.of_real_add, complex.of_real_mul],
   ring
 end

src/analysis/convex/stone_separation.lean

@@ -74,7 +74,7 @@ begin
   congr' 3,
   rw [←mul_smul, ←mul_rotate, mul_right_comm, mul_smul, ←mul_smul _ av, mul_rotate, mul_smul _ bz,
     ←smul_add],
-  simp only [list.map, list.pmap, nat.add_def, add_zero, fin.mk_eq_subtype_mk, fin.mk_bit0,
+  simp only [list.map, list.pmap, nat.add_def, add_zero, fin.mk_bit0,
     fin.mk_one, list.foldr_cons, list.foldr_nil],
   refl,
 end

src/combinatorics/composition.lean

@@ -719,7 +719,7 @@ def composition_as_set_equiv (n : ℕ) : composition_as_set n ≃ finset (fin (n
     erw [set.mem_set_of_eq],
     simp only [this, false_or, add_right_inj, add_eq_zero_iff, one_ne_zero, false_and, fin.coe_mk],
     split,
-    { rintros ⟨j, js, hj⟩, convert js, exact (fin.ext_iff _ _).2 hj },
+    { rintros ⟨j, js, hj⟩, convert js, exact fin.ext_iff.2 hj },
     { assume h, exact ⟨i, h, rfl⟩ }
   end }
 

src/combinatorics/simple_graph/coloring.lean

@@ -213,7 +213,7 @@ begin
   split,
   { rintro hc,
     have C : G.coloring (fin n) := hc.to_coloring (by simp),
-    let f := embedding.complete_graph (fin.coe_embedding n).to_embedding,
+    let f := embedding.complete_graph fin.coe_embedding,
     use f.to_hom.comp C,
     intro v,
     cases C with color valid,
@@ -222,7 +222,7 @@ begin
     refine ⟨coloring.mk _ _⟩,
     { exact λ v, ⟨C v, Cf v⟩, },
     { rintro v w hvw,
-      simp only [subtype.mk_eq_mk, ne.def],
+      simp only [fin.mk_eq_mk, ne.def],
       exact C.valid hvw, } }
 end
 

src/computability/primrec.lean

@@ -1035,7 +1035,7 @@ def subtype {p : α → Prop} [decidable_pred p]
 instance fin {n} : primcodable (fin n) :=
 @of_equiv _ _
   (subtype $ nat_lt.comp primrec.id (const n))
-  (equiv.refl _)
+  fin.equiv_subtype
 
 instance vector {n} : primcodable (vector α n) :=
 subtype ((@primrec.eq _ _ nat.decidable_eq).comp list_length (const _))

src/data/buffer/basic.lean

@@ -189,7 +189,7 @@ lemma nth_le_to_list (b : buffer α) {i : ℕ} (h) :
 nth_le_to_list' _ _ _
 
 lemma read_eq_nth_le_to_list (b : buffer α) (i) :
-  b.read i = b.to_list.nth_le i (by simpa using i.is_lt) :=
+  b.read i = b.to_list.nth_le i (by simp) :=
 by simp [nth_le_to_list]
 
 lemma read_singleton (c : α) : [c].to_buffer.read ⟨0, by simp⟩ = c :=

src/data/countable/defs.lean

@@ -67,7 +67,8 @@ instance subsingleton.to_countable [subsingleton α] : countable α :=
 @[priority 500]
 instance [countable α] {p : α → Prop} : countable {x // p x} := subtype.val_injective.countable
 
-instance {n : ℕ} : countable (fin n) := subtype.countable
+instance {n : ℕ} : countable (fin n) :=
+function.injective.countable (@fin.eq_of_veq n)
 
 @[priority 100]
 instance finite.to_countable [finite α] : countable α :=