chore(*): move to lean-3.11.0 (#2632)

Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>

leanpkg.toml

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

src/algebra/opposites.lean

@@ -113,7 +113,7 @@ instance [zero_ne_one_class α] : zero_ne_one_class (opposite α) :=
   .. opposite.has_zero α, .. opposite.has_one α }
 
 instance [integral_domain α] : integral_domain (opposite α) :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y (H : op _ = op (0:α)),
+{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y (H : op (_ * _) = op (0:α)),
     or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ op_inj H)
       (λ hy, or.inr $ unop_inj $ hy) (λ hx, or.inl $ unop_inj $ hx),
   .. opposite.comm_ring α, .. opposite.zero_ne_one_class α }

src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean

@@ -73,6 +73,8 @@ the original diagram `F`. -/
       simpa only [limit.lift_π, fan.mk_π_app, category.assoc, category.id_comp] using t,
     end }, }.
 
+local attribute [semireducible] op unop opposite
+
 /-- The morphism from cones over the original diagram `F` to cones over the walking pair diagram
 `diagram F`. -/
 @[simp] def cones_inv : F.cones ⟶ (diagram F).cones :=

src/category_theory/opposites.lean

@@ -181,6 +181,8 @@ variables {D : Type u₂} [category.{v₂} D]
 section
 variables {F G : C ⥤ D}
 
+local attribute [semireducible] has_hom.opposite
+
 @[simps] protected definition op (α : F ⟶ G) : G.op ⟶ F.op :=
 { app         := λ X, (α.app (unop X)).op,
   naturality' := begin tidy, erw α.naturality, refl, end }
@@ -189,7 +191,14 @@ variables {F G : C ⥤ D}
 
 @[simps] protected definition unop (α : F.op ⟶ G.op) : G ⟶ F :=
 { app         := λ X, (α.app (op X)).unop,
-  naturality' := begin tidy, erw α.naturality, refl, end }
+  naturality' :=
+  begin
+    intros X Y f,
+    have := congr_arg has_hom.hom.op (α.naturality f.op),
+    dsimp at this,
+    erw this,
+    refl,
+  end }
 
 @[simp] lemma unop_id (F : C ⥤ D) : nat_trans.unop (𝟙 F.op) = 𝟙 F := rfl
 
@@ -198,6 +207,8 @@ end
 section
 variables {F G : C ⥤ Dᵒᵖ}
 
+local attribute [semireducible] has_hom.opposite
+
 protected definition left_op (α : F ⟶ G) : G.left_op ⟶ F.left_op :=
 { app         := λ X, (α.app (unop X)).unop,
   naturality' := begin tidy, erw α.naturality, refl, end }
@@ -208,7 +219,13 @@ rfl
 
 protected definition right_op (α : F.left_op ⟶ G.left_op) : G ⟶ F :=
 { app         := λ X, (α.app (op X)).op,
-  naturality' := begin tidy, erw α.naturality, refl, end }
+  naturality' :=
+  begin
+    intros X Y f,
+    have := congr_arg has_hom.hom.op (α.naturality f.op),
+    dsimp at this,
+    erw this
+  end }
 
 @[simp] lemma right_op_app (α : F.left_op ⟶ G.left_op) (X) :
   (nat_trans.right_op α).app X = (α.app (op X)).op :=

src/category_theory/yoneda.lean

@@ -47,7 +47,7 @@ by obviously
 
 @[simp] lemma naturality {X Y : C} (α : yoneda.obj X ⟶ yoneda.obj Y)
   {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) : f ≫ α.app (op Z') h = α.app (op Z) (f ≫ h) :=
-begin erw [functor_to_types.naturality], refl end
+(functor_to_types.naturality _ _ α f.op h).symm
 
 instance yoneda_full : full (@yoneda C _) :=
 { preimage := λ X Y f, (f.app (op X)) (𝟙 X) }
@@ -144,11 +144,8 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
     naturality' :=
     begin
       intros X Y f, ext, dsimp,
-      erw [category.id_comp,
-           ←functor_to_types.naturality,
-           obj_map_id,
-           functor_to_types.naturality,
-           functor_to_types.map_id_apply]
+      erw [category.id_comp, ←functor_to_types.naturality],
+      simp only [category.comp_id, yoneda_obj_map],
     end },
   inv :=
   { app := λ F x,
@@ -167,10 +164,9 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
   begin
     ext, dsimp,
     erw [←functor_to_types.naturality,
-         obj_map_id,
-         functor_to_types.naturality,
-         functor_to_types.map_id_apply],
-    refl,
+         obj_map_id],
+    simp only [yoneda_map_app, has_hom.hom.unop_op],
+    erw [category.id_comp],
   end,
   inv_hom_id' :=
   begin

src/data/array/lemmas.lean

@@ -191,7 +191,7 @@ heq_of_heq_of_eq
   d_array.ext $ λ ⟨i, h⟩, to_list_nth_le i h _
 
 @[simp] theorem to_array_to_list (l : list α) : l.to_array.to_list = l :=
-list.ext_le (to_list_length _) $ λ n h1 h2, to_list_nth_le _ _ _
+list.ext_le (to_list_length _) $ λ n h1 h2, to_list_nth_le _ h2 _
 
 end to_array
 

src/data/complex/basic.lean

@@ -133,7 +133,7 @@ by simpa using @conj_inj z 0
 
 lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
 ⟨λ h, ⟨z.re, ext rfl $ eq_zero_of_neg_eq (congr_arg im h)⟩,
- λ ⟨h, e⟩, e.symm ▸ rfl⟩
+ λ ⟨h, e⟩, by rw [e, conj_of_real]⟩
 
 lemma eq_conj_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=
 eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩

src/data/padics/padic_norm.lean

@@ -276,7 +276,7 @@ by simp [hq, padic_norm]
 The p-adic norm is nonnegative.
 -/
 protected lemma nonneg (q : ℚ) : 0 ≤ padic_norm p q :=
-if hq : q = 0 then by simp [hq]
+if hq : q = 0 then by simp [hq, padic_norm]
 else
   begin
     unfold padic_norm; split_ifs,
@@ -356,7 +356,7 @@ eq_div_of_mul_eq _ _ (padic_norm.nonzero _ hr) (by rw [←padic_norm.mul, div_mu
 The p-adic norm of an integer is at most 1.
 -/
 protected theorem of_int (z : ℤ) : padic_norm p ↑z ≤ 1 :=
-if hz : z = 0 then by simp [hz] else
+if hz : z = 0 then by simp [hz, zero_le_one] else
 begin
   unfold padic_norm,
   rw [if_neg _],

src/data/pfun.lean

@@ -203,7 +203,7 @@ eq_some_iff.2 $ mem_map f $ mem_some _
 
 theorem mem_assert {p : Prop} {f : p → roption α}
   : ∀ {a} (h : p), a ∈ f h → a ∈ assert p f
-| _ _ ⟨h, rfl⟩ := ⟨⟨_, _⟩, rfl⟩
+| _ x ⟨h, rfl⟩ := ⟨⟨x, h⟩, rfl⟩
 
 @[simp] theorem mem_assert_iff {p : Prop} {f : p → roption α} {a} :
   a ∈ assert p f ↔ ∃ h : p, a ∈ f h :=
@@ -212,7 +212,7 @@ theorem mem_assert {p : Prop} {f : p → roption α}
 
 theorem mem_bind {f : roption α} {g : α → roption β} :
   ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g
-| _ _ ⟨h, rfl⟩ ⟨h₂, rfl⟩ := ⟨⟨_, _⟩, rfl⟩
+| _ _ ⟨h, rfl⟩ ⟨h₂, rfl⟩ := ⟨⟨h, h₂⟩, rfl⟩
 
 @[simp] theorem mem_bind_iff {f : roption α} {g : α → roption β} {b} :
   b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a :=

src/data/polynomial.lean

@@ -1835,7 +1835,7 @@ begin
   exact multiplicity.is_greatest'
     (multiplicity_finite_of_degree_pos_of_monic
     (show (0 : with_bot ℕ) < degree (X - C a),
-      by rw degree_X_sub_C; exact dec_trivial) _ hp)
+      by rw degree_X_sub_C; exact dec_trivial) (monic_X_sub_C _) hp)
     (nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
 end
 
@@ -2524,7 +2524,7 @@ begin
   { symmetry, apply finsupp.sum_mul }
 end
 
-def pow_sub_pow_factor (x y : R) : Π {i : ℕ},{z : R // x^i - y^i = z*(x - y)}
+def pow_sub_pow_factor (x y : R) : Π (i : ℕ), {z : R // x^i - y^i = z * (x - y)}
 | 0 := ⟨0, by simp⟩
 | 1 := ⟨1, by simp⟩
 | (k+2) :=
@@ -2538,18 +2538,15 @@ def pow_sub_pow_factor (x y : R) : Π {i : ℕ},{z : R // x^i - y^i = z*(x - y)}
   end
 
 def eval_sub_factor (f : polynomial R) (x y : R) :
-  {z : R // f.eval x - f.eval y = z*(x - y)} :=
+  {z : R // f.eval x - f.eval y = z * (x - y)} :=
 begin
-  existsi f.sum (λ a b, b * (pow_sub_pow_factor x y).val),
-  unfold eval eval₂,
-  rw [←finsupp.sum_sub],
-  have : finsupp.sum f (λ (a : ℕ) (b : R), b * (pow_sub_pow_factor x y).val) * (x - y) =
-    finsupp.sum f (λ (a : ℕ) (b : R), b * (pow_sub_pow_factor x y).val * (x - y)),
-  { apply finsupp.sum_mul },
-  rw this,
-  congr, ext e a,
-  rw [mul_assoc, ←(pow_sub_pow_factor x y).property],
-  simp [mul_sub]
+  refine ⟨f.sum (λ i r, r * (pow_sub_pow_factor x y i).val), _⟩,
+  delta eval eval₂,
+  rw ← finsupp.sum_sub,
+  rw finsupp.sum_mul,
+  delta finsupp.sum,
+  congr, ext i r, dsimp,
+  rw [mul_assoc, ←(pow_sub_pow_factor x y _).property, mul_sub],
 end
 
 end identities

src/data/real/hyperreal.lean

@@ -586,19 +586,19 @@ lemma zero_of_infinitesimal_real {r : ℝ} : infinitesimal r → r = 0 := eq_of_
 lemma zero_iff_infinitesimal_real {r : ℝ} : infinitesimal r ↔ r = 0 :=
 ⟨zero_of_infinitesimal_real, λ hr, by rw hr; exact infinitesimal_zero⟩
 
-lemma infinitesimal_add {x y : ℝ*} :
-  infinitesimal x → infinitesimal y → infinitesimal (x + y) :=
-zero_add 0 ▸ is_st_add
+lemma infinitesimal_add {x y : ℝ*} (hx : infinitesimal x) (hy : infinitesimal y) :
+  infinitesimal (x + y) :=
+by simpa only [add_zero] using is_st_add hx hy
 
-lemma infinitesimal_neg {x : ℝ*} : infinitesimal x → infinitesimal (-x) :=
-(neg_zero : -(0 : ℝ) = 0) ▸ is_st_neg
+lemma infinitesimal_neg {x : ℝ*} (hx : infinitesimal x) : infinitesimal (-x) :=
+by simpa only [neg_zero] using is_st_neg hx
 
 lemma infinitesimal_neg_iff {x : ℝ*} : infinitesimal x ↔ infinitesimal (-x) :=
 ⟨infinitesimal_neg, λ h, (neg_neg x) ▸ @infinitesimal_neg (-x) h⟩
 
-lemma infinitesimal_mul {x y : ℝ*} :
-  infinitesimal x → infinitesimal y → infinitesimal (x * y) :=
-zero_mul 0 ▸ is_st_mul
+lemma infinitesimal_mul {x y : ℝ*} (hx : infinitesimal x) (hy : infinitesimal y) :
+  infinitesimal (x * y) :=
+by simpa only [mul_zero] using is_st_mul hx hy
 
 theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} :
   tendsto f at_top (𝓝 0) → infinitesimal (of_seq f) :=

src/geometry/manifold/real_instances.lean

@@ -216,7 +216,7 @@ def Icc_left_chart (x y : ℝ) [fact (x < y)] :
   open_target := begin
     have : is_open {z : ℝ | z < y - x} := is_open_Iio,
     have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
-      (continuous_apply 0) _ this,
+      @continuous_apply (fin 1) (λ _, ℝ) _ 0 _ this,
     exact continuous_subtype_val _ this
   end,
   continuous_to_fun := begin
@@ -265,7 +265,7 @@ def Icc_right_chart (x y : ℝ) [fact (x < y)] :
   open_target := begin
     have : is_open {z : ℝ | z < y - x} := is_open_Iio,
     have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
-      (continuous_apply 0) _ this,
+      @continuous_apply (fin 1) (λ _, ℝ) _ 0 _ this,
     exact continuous_subtype_val _ this
   end,
   continuous_to_fun := begin

src/measure_theory/bochner_integration.lean

@@ -963,7 +963,8 @@ lemma integral_eq (f : α →₁ β) : integral f = (integral_clm).to_fun f := r
 
 @[norm_cast] lemma simple_func.integral_eq_integral (f : α →₁ₛ β) :
   integral (f : α →₁ β) = f.integral :=
-by { refine uniformly_extend_of_ind _ _ _ _, exact simple_func.integral_clm.uniform_continuous }
+uniformly_extend_of_ind simple_func.uniform_inducing simple_func.dense_range
+  simple_func.integral_clm.uniform_continuous _
 
 variables (α β)
 @[simp] lemma integral_zero : integral (0 : α →₁ β) = 0 :=

src/set_theory/cofinality.lean

@@ -66,11 +66,12 @@ namespace ordinal
   `cof 0 = 0` and `cof (succ o) = 1`, so it is only really
   interesting on limit ordinals (when it is an infinite cardinal). -/
 def cof (o : ordinal.{u}) : cardinal.{u} :=
-quot.lift_on o (λ ⟨α, r, _⟩, by exactI strict_order.cof r) $
-λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩, begin resetI,
-  show strict_order.cof r = strict_order.cof s,
-  refine cardinal.lift_inj.1 (@order_iso.cof _ _ _ _ ⟨_⟩ ⟨_⟩ _),
-  exact ⟨f, λ a b, not_congr hf⟩,
+quot.lift_on o (λ ⟨α, r, _⟩, by exactI strict_order.cof r)
+begin
+  rintros ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩,
+  rw ← cardinal.lift_inj,
+  apply order_iso.cof ⟨f, _⟩,
+  simp [hf]
 end
 
 lemma cof_type (r : α → α → Prop) [is_well_order α r] : (type r).cof = strict_order.cof r := rfl

src/topology/metric_space/emetric_space.lean

@@ -76,7 +76,8 @@ uniform_space.of_core {
   comp       :=
     le_infi $ assume ε, le_infi $ assume h,
     have (2 : ennreal) = (2 : ℕ) := by simp,
-    have A : 0 < ε / 2 := ennreal.div_pos_iff.2 ⟨ne_of_gt h, this ▸ ennreal.nat_ne_top 2⟩,
+    have A : 0 < ε / 2 := ennreal.div_pos_iff.2
+      ⟨ne_of_gt h, by { convert ennreal.nat_ne_top 2 }⟩,
     lift'_le
     (mem_infi_sets (ε / 2) $ mem_infi_sets A (subset.refl _)) $
     have ∀ (a b c : α), edist a c < ε / 2 → edist c b < ε / 2 → edist a b < ε,