refactor(*): use option.map₂ (#18081)

Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: 3 people

src/algebra/continued_fractions/convergents_equiv.lean

@@ -111,7 +111,7 @@ squashed into position `n`. -/
 lemma squash_seq_nth_of_not_terminated {gp_n gp_succ_n : pair K}
   (s_nth_eq : s.nth n = some gp_n) (s_succ_nth_eq : s.nth (n + 1) = some gp_succ_n) :
   (squash_seq s n).nth n = some ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ :=
-by simp [*, squash_seq, (seq.zip_with_nth_some (seq.nats_nth n) s_nth_eq _)]
+by simp [*, squash_seq]
 
 /-- The values before the squashed position stay the same. -/
 lemma squash_seq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squash_seq s n).nth m = s.nth m :=
@@ -123,8 +123,7 @@ begin
       s.ge_stable n.le_succ s_succ_nth_eq,
     obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.nth m = some gp_m, from
       s.ge_stable (le_of_lt m_lt_n) s_nth_eq,
-    simp [*, squash_seq, (seq.zip_with_nth_some (seq.nats_nth m) s_mth_eq _),
-      (ne_of_lt m_lt_n)] }
+    simp [*, squash_seq, m_lt_n.ne] }
 end
 
 /-- Squashing at position `n + 1` and taking the tail is the same as squashing the tail of the
@@ -141,19 +140,15 @@ begin
   { obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.nth (n + 1) = some gp_succ_n, from
       s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq,
     -- apply extensionality with `m` and continue by cases `m = n`.
-    ext m,
+    ext1 m,
     cases decidable.em (m = n) with m_eq_n m_ne_n,
     { have : s.tail.nth n = some gp_succ_n, from (s.nth_tail n).trans s_succ_nth_eq,
-      simp [*, squash_seq, seq.nth_tail, (seq.zip_with_nth_some (seq.nats_nth n) this),
-        (seq.zip_with_nth_some (seq.nats_nth (n + 1)) s_succ_nth_eq)] },
+      simp [*, squash_seq] },
     { have : s.tail.nth m = s.nth (m + 1), from s.nth_tail m,
       cases s_succ_mth_eq : s.nth (m + 1),
       all_goals { have s_tail_mth_eq, from this.trans s_succ_mth_eq },
-      { simp only [*, squash_seq, seq.nth_tail, (seq.zip_with_nth_none' s_succ_mth_eq),
-          (seq.zip_with_nth_none' s_tail_mth_eq)] },
-      { simp [*, squash_seq, seq.nth_tail,
-          (seq.zip_with_nth_some (seq.nats_nth (m + 1)) s_succ_mth_eq),
-          (seq.zip_with_nth_some (seq.nats_nth m) s_tail_mth_eq)] } } }
+      { simp only [*, squash_seq, seq.nth_tail, seq.nth_zip_with, option.map₂_none_right] },
+      { simp [*, squash_seq] } } }
 end
 
 /-- The auxiliary function `convergents'_aux` returns the same value for a sequence and the

src/algebra/group/with_one/defs.lean

@@ -19,6 +19,12 @@ this provides an example of an adjunction is proved in `algebra.category.Mon.adj
 Another result says that adjoining to a group an element `zero` gives a `group_with_zero`. For more
 information about these structures (which are not that standard in informal mathematics, see
 `algebra.group_with_zero.basic`)
+
+## Implementation notes
+
+At various points in this file, `id $` is used in at the start of a proof field in a structure. This
+ensures that the generated `_proof_1` lemmas are stated in terms of the algebraic operations and
+not `option.map`, as the latter does not typecheck once `with_zero`/`with_one` is irreducible.
 -/
 
 universes u v w
@@ -49,7 +55,7 @@ instance [has_mul α] : has_mul (with_one α) := ⟨option.lift_or_get (*)⟩
 @[to_additive] instance [has_inv α] : has_inv (with_one α) := ⟨λ a, option.map has_inv.inv a⟩
 
 @[to_additive] instance [has_involutive_inv α] : has_involutive_inv (with_one α) :=
-{ inv_inv := λ a, (option.map_map _ _ _).trans $ by simp_rw [inv_comp_inv, option.map_id, id],
+{ inv_inv := id $ λ a, (option.map_map _ _ _).trans $ by simp_rw [inv_comp_inv, option.map_id, id],
   ..with_one.has_inv }
 
 @[to_additive] instance [has_inv α] : inv_one_class (with_one α) :=
@@ -112,15 +118,12 @@ protected lemma cases_on {P : with_one α → Prop} :
   ∀ (x : with_one α), P 1 → (∀ a : α, P a) → P x :=
 option.cases_on
 
--- the `show` statements in the proofs are important, because otherwise the generated lemmas
--- `with_one.mul_one_class._proof_{1,2}` have an ill-typed statement after `with_one` is made
--- irreducible.
 @[to_additive]
 instance [has_mul α] : mul_one_class (with_one α) :=
 { mul := (*),
   one := (1),
-  one_mul   := show ∀ x : with_one α, 1 * x = x, from (option.lift_or_get_is_left_id _).1,
-  mul_one   := show ∀ x : with_one α, x * 1 = x, from (option.lift_or_get_is_right_id _).1 }
+  one_mul := id $ (option.lift_or_get_is_left_id _).1,
+  mul_one := id $ (option.lift_or_get_is_right_id _).1 }
 
 @[to_additive]
 instance [semigroup α] : monoid (with_one α) :=
@@ -153,49 +156,28 @@ instance [one : has_one α] : has_one (with_zero α) :=
 @[simp, norm_cast] lemma coe_one [has_one α] : ((1 : α) : with_zero α) = 1 := rfl
 
 instance [has_mul α] : mul_zero_class (with_zero α) :=
-{ mul       := λ o₁ o₂, o₁.bind (λ a, option.map (λ b, a * b) o₂),
-  zero_mul  := λ a, rfl,
-  mul_zero  := λ a, by cases a; refl,
+{ mul       := option.map₂ (*),
+  zero_mul  := id $ option.map₂_none_left (*),
+  mul_zero  := id $ option.map₂_none_right (*),
   ..with_zero.has_zero }
 
 @[simp, norm_cast] lemma coe_mul {α : Type u} [has_mul α]
   {a b : α} : ((a * b : α) : with_zero α) = a * b := rfl
 
-@[simp] lemma zero_mul {α : Type u} [has_mul α]
-  (a : with_zero α) : 0 * a = 0 := rfl
-
-@[simp] lemma mul_zero {α : Type u} [has_mul α]
-  (a : with_zero α) : a * 0 = 0 := by cases a; refl
-
 instance [has_mul α] : no_zero_divisors (with_zero α) :=
-⟨by { rintro (a|a) (b|b) h, exacts [or.inl rfl, or.inl rfl, or.inr rfl, option.no_confusion h] }⟩
+⟨λ a b, id $ option.map₂_eq_none_iff.1⟩
 
 instance [semigroup α] : semigroup_with_zero (with_zero α) :=
-{ mul_assoc := λ a b c, match a, b, c with
-    | none,   _,      _      := rfl
-    | some a, none,   _      := rfl
-    | some a, some b, none   := rfl
-    | some a, some b, some c := congr_arg some (mul_assoc _ _ _)
-    end,
+{ mul_assoc := id $ λ _ _ _, option.map₂_assoc mul_assoc,
   ..with_zero.mul_zero_class }
 
 instance [comm_semigroup α] : comm_semigroup (with_zero α) :=
-{ mul_comm := λ a b, match a, b with
-    | none,   _      := (mul_zero _).symm
-    | some a, none   := rfl
-    | some a, some b := congr_arg some (mul_comm _ _)
-    end,
+{ mul_comm := id $ λ _ _, option.map₂_comm mul_comm,
   ..with_zero.semigroup_with_zero }
 
 instance [mul_one_class α] : mul_zero_one_class (with_zero α) :=
-{ one_mul := λ a, match a with
-    | none   := rfl
-    | some a := congr_arg some $ one_mul _
-    end,
-  mul_one := λ a, match a with
-    | none   := rfl
-    | some a := congr_arg some $ mul_one _
-    end,
+{ one_mul := id $ option.map₂_left_identity one_mul,
+  mul_one := id $ option.map₂_right_identity mul_one,
   ..with_zero.mul_zero_class,
   ..with_zero.has_one }
 
@@ -234,16 +216,15 @@ instance [has_inv α] : has_inv (with_zero α) := ⟨λ a, option.map has_inv.in
 @[simp] lemma inv_zero [has_inv α] : (0 : with_zero α)⁻¹ = 0 := rfl
 
 instance [has_involutive_inv α] : has_involutive_inv (with_zero α) :=
-{ inv_inv := λ a, (option.map_map _ _ _).trans $ by simp_rw [inv_comp_inv, option.map_id, id],
+{ inv_inv := id $ λ a, (option.map_map _ _ _).trans $ by simp_rw [inv_comp_inv, option.map_id, id],
   ..with_zero.has_inv }
 
 instance [inv_one_class α] : inv_one_class (with_zero α) :=
 { inv_one := show ((1⁻¹ : α) : with_zero α) = 1, by simp,
   ..with_zero.has_one,
   ..with_zero.has_inv }
 
-instance [has_div α] : has_div (with_zero α) :=
-⟨λ o₁ o₂, o₁.bind (λ a, option.map (λ b, a / b) o₂)⟩
+instance [has_div α] : has_div (with_zero α) := ⟨option.map₂ (/)⟩
 
 @[norm_cast] lemma coe_div [has_div α] (a b : α) : ↑(a / b : α) = (a / b : with_zero α) := rfl
 

src/algebra/monoid_algebra/grading.lean

@@ -180,7 +180,7 @@ graded_algebra.of_alg_hom _
     dsimp,
     rw [decompose_aux_single, direct_sum.coe_alg_hom_of, subtype.coe_mk],
   end)
-  (λ i x, by convert (decompose_aux_coe f x : _))
+  (λ i x, by rw [decompose_aux_coe f x])
 
 -- Lean can't find this later without us repeating it
 instance grade_by.decomposition : direct_sum.decomposition (grade_by R f) :=

src/algebra/order/monoid/with_top.lean

@@ -54,7 +54,7 @@ end has_one
 section has_add
 variables [has_add α] {a b c d : with_top α} {x y : α}
 
-instance : has_add (with_top α) := ⟨λ o₁ o₂, o₁.bind $ λ a, o₂.map $ (+) a⟩
+instance : has_add (with_top α) := ⟨option.map₂ (+)⟩
 
 @[norm_cast] lemma coe_add : ((x + y : α) : with_top α) = x + y := rfl
 @[norm_cast] lemma coe_bit0 : ((bit0 x : α) : with_top α) = bit0 x := rfl
@@ -201,35 +201,16 @@ end
 end has_add
 
 instance [add_semigroup α] : add_semigroup (with_top α) :=
-{ add_assoc := begin
-    repeat { refine with_top.rec_top_coe _ _; try { intro }};
-    simp [←with_top.coe_add, add_assoc]
-  end,
+{ add_assoc := λ _ _ _, option.map₂_assoc add_assoc,
   ..with_top.has_add }
 
 instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
-{ add_comm :=
-  begin
-    repeat { refine with_top.rec_top_coe _ _; try { intro }};
-    simp [←with_top.coe_add, add_comm]
-  end,
+{ add_comm := λ _ _, option.map₂_comm add_comm,
   ..with_top.add_semigroup }
 
 instance [add_zero_class α] : add_zero_class (with_top α) :=
-{ zero_add :=
-  begin
-    refine with_top.rec_top_coe _ _,
-    { simp },
-    { intro,
-      rw [←with_top.coe_zero, ←with_top.coe_add, zero_add] }
-  end,
-  add_zero :=
-  begin
-    refine with_top.rec_top_coe _ _,
-    { simp },
-    { intro,
-      rw [←with_top.coe_zero, ←with_top.coe_add, add_zero] }
-  end,
+{ zero_add := option.map₂_left_identity zero_add,
+  add_zero := option.map₂_right_identity add_zero,
   ..with_top.has_zero,
   ..with_top.has_add }
 

src/algebra/order/ring/with_top.lean

@@ -30,12 +30,11 @@ variables [has_zero α] [has_mul α]
 
 instance : mul_zero_class (with_top α) :=
 { zero := 0,
-  mul := λ m n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
+  mul := λ m n, if m = 0 ∨ n = 0 then 0 else option.map₂ (*) m n,
   zero_mul := assume a, if_pos $ or.inl rfl,
   mul_zero := assume a, if_pos $ or.inr rfl }
 
-lemma mul_def {a b : with_top α} :
-  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
+lemma mul_def {a b : with_top α} : a * b = if a = 0 ∨ b = 0 then 0 else option.map₂ (*) a b := rfl
 
 @[simp] lemma mul_top {a : with_top α} (h : a ≠ 0) : a * ⊤ = ⊤ :=
 by cases a; simp [mul_def, h]; refl
@@ -46,6 +45,14 @@ by cases a; simp [mul_def, h]; refl
 @[simp] lemma top_mul_top : (⊤ * ⊤ : with_top α) = ⊤ :=
 top_mul top_ne_zero
 
+instance [no_zero_divisors α] : no_zero_divisors (with_top α) :=
+begin
+  refine ⟨λ a b h₁, decidable.by_contradiction $ λ h₂, _⟩,
+  rw [mul_def, if_neg h₂] at h₁,
+  rcases option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩,
+  exact h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))
+end
+
 end has_mul
 
 section mul_zero_class
@@ -55,7 +62,7 @@ variables [mul_zero_class α]
 @[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
 decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
 decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
-by { simp [*, mul_def], refl }
+by { simp [*, mul_def] }
 
 lemma mul_coe {b : α} (hb : b ≠ 0) : ∀{a : with_top α}, a * b = a.bind (λa:α, ↑(a * b))
 | none     := show (if (⊤:with_top α) = 0 ∨ (b:with_top α) = 0 then 0 else ⊤ : with_top α) = ⊤,
@@ -114,8 +121,8 @@ instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top
     begin
       have : ∀ z, map f z = 0 ↔ z = 0,
         from λ z, (option.map_injective hf).eq_iff' f.to_zero_hom.with_top_map.map_zero,
-      rcases eq_or_ne x 0 with rfl|hx, { simp },
-      rcases eq_or_ne y 0 with rfl|hy, { simp },
+      rcases decidable.eq_or_ne x 0 with rfl|hx, { simp },
+      rcases decidable.eq_or_ne y 0 with rfl|hy, { simp },
       induction x using with_top.rec_top_coe, { simp [hy, this] },
       induction y using with_top.rec_top_coe,
       { have : (f x : with_top S) ≠ 0, by simpa [hf.eq_iff' (map_zero f)] using hx,
@@ -124,10 +131,6 @@ instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top
     end,
   .. f.to_zero_hom.with_top_map, .. f.to_monoid_hom.to_one_hom.with_top_map }
 
-instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_top α) :=
-⟨λ a b, by cases a; cases b; dsimp [mul_def]; split_ifs;
-  simp [*, none_eq_top, some_eq_coe, mul_eq_zero] at *⟩
-
 instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_top α) :=
 { mul := (*),
   zero := 0,
@@ -150,7 +153,7 @@ instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
 { mul := (*),
   zero := 0,
   mul_comm := λ a b,
-    by simp only [or_comm, mul_def, option.bind_comm a b, mul_comm],
+    by simp only [or_comm, mul_def, mul_comm, @option.map₂_comm _ _ _ _ a b _ mul_comm],
   .. with_top.monoid_with_zero }
 
 variables [canonically_ordered_comm_semiring α]
@@ -202,7 +205,7 @@ instance : mul_zero_class (with_bot α) :=
 with_top.mul_zero_class
 
 lemma mul_def {a b : with_bot α} :
-  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
+  a * b = if a = 0 ∨ b = 0 then 0 else option.map₂ (*) a b := rfl
 
 @[simp] lemma mul_bot {a : with_bot α} (h : a ≠ 0) : a * ⊥ = ⊥ :=
 with_top.mul_top h
@@ -220,9 +223,7 @@ section mul_zero_class
 variables [mul_zero_class α]
 
 @[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_bot α) = a * b :=
-decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
-decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
-by { simp [*, mul_def], refl }
+with_top.coe_mul
 
 lemma mul_coe {b : α} (hb : b ≠ 0) {a : with_bot α} : a * b = a.bind (λa:α, ↑(a * b)) :=
 with_top.mul_coe hb

src/data/finset/n_ary.lean

@@ -321,4 +321,16 @@ lemma image_image₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f'
   image₂ f s (t.image g) = (image₂ f' t s).image g' :=
 (image_image₂_antidistrib_right $ λ a b, (h_right_anticomm b a).symm).symm
 
+/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
+`finset.image₂ f`. -/
+lemma image₂_left_identity {f : α → γ → γ} {a : α} (h : ∀ b, f a b = b) (t : finset γ) :
+  image₂ f {a} t = t :=
+coe_injective $ by rw [coe_image₂, coe_singleton, set.image2_left_identity h]
+
+/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
+`finset.image₂ f`. -/
+lemma image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b = a) (s : finset γ) :
+  image₂ f s {b} = s :=
+by rw [image₂_singleton_right, funext h, image_id']
+
 end finset

src/data/option/n_ary.lean

@@ -42,8 +42,10 @@ because of the lack of universe polymorphism. -/
 lemma map₂_def {α β γ : Type*} (f : α → β → γ) (a : option α) (b : option β) :
   map₂ f a b = f <$> a <*> b := by cases a; refl
 
-@[simp] lemma map₂_some_some (f : α → β → γ) (a : α) (b : β) : map₂ f (some a) (some b) = f a b :=
+@[simp] lemma map₂_some_some (f : α → β → γ) (a : α) (b : β) :
+  map₂ f (some a) (some b) = some (f a b) :=
 rfl
+
 lemma map₂_coe_coe (f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b := rfl
 @[simp] lemma map₂_none_left (f : α → β → γ) (b : option β) : map₂ f none b = none := rfl
 @[simp] lemma map₂_none_right (f : α → β → γ) (a : option α) : map₂ f a none = none :=
@@ -170,4 +172,16 @@ lemma map_map₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : 
   map₂ f a (b.map g) = (map₂ f' b a).map g' :=
 by cases a; cases b; simp [h_right_anticomm]
 
+/-- If `a` is a left identity for a binary operation `f`, then `some a` is a left identity for
+`option.map₂ f`. -/
+lemma map₂_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (o : option β) :
+  map₂ f (some a) o = o :=
+by { cases o, exacts [rfl, congr_arg some (h _)] }
+
+/-- If `b` is a right identity for a binary operation `f`, then `some b` is a right identity for
+`option.map₂ f`. -/
+lemma map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (o : option α) :
+  map₂ f o (some b) = o :=
+by simp [h, map₂]
+
 end option