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

`fin n` is a structure now.

Author: gebner

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 }