making with_zero and with_one irreducible

src/algebra/continued_fractions/computation/approximations.lean

@@ -85,6 +85,7 @@ begin
   simp [(le_of_lt (nth_stream_fr_lt_one nth_stream_eq))]
 end
 
+local attribute [reducible] with_one
 /--
 Shows that the `n + 1`th integer part `bₙ₊₁` of the stream is smaller or equal than the inverse of
 the `n`th fractional part `frₙ` of the stream.
@@ -193,7 +194,7 @@ begin
     have : ¬(n + 2 ≤ 1), by linarith,
     have not_terminated_at_n : ¬g.terminated_at n, from or.resolve_left hyp this,
     obtain ⟨gp, s_ppred_nth_eq⟩ : ∃ gp, g.s.nth n = some gp, from
-      with_one.ne_one_iff_exists.elim_left not_terminated_at_n,
+      option.ne_none_iff_exists.elim_left not_terminated_at_n,
     set pconts := g.continuants_aux (n + 1) with pconts_eq,
     set ppconts := g.continuants_aux n with ppconts_eq,
     -- use the recurrence of continuants_aux
@@ -301,7 +302,7 @@ begin
       denominators_stable_of_terminated n.le_succ this,
     rw this },
   { obtain ⟨b, nth_part_denom_eq⟩ : ∃ b, g.partial_denominators.nth n = some b, from
-      with_one.ne_one_iff_exists.elim_left not_terminated,
+      option.ne_none_iff_exists.elim_left not_terminated,
     have : 1 ≤ b, from of_one_le_nth_part_denom nth_part_denom_eq,
     calc
       (gcf.of v).denominators n ≤ b * (gcf.of v).denominators n   : by simpa using

src/algebra/continued_fractions/computation/translations.lean

@@ -95,7 +95,7 @@ begin
     replace nth_fr_ne_zero : ∀ ifp, int_fract_pair.stream v n = some ifp → ifp.fr ≠ 0, by
       simpa using nth_fr_ne_zero,
     obtain ⟨ifp_n, stream_nth_eq⟩ : ∃ ifp_n, int_fract_pair.stream v n = some ifp_n, from
-      with_one.ne_one_iff_exists.elim_left stream_nth_ne_none,
+      option.ne_none_iff_exists.elim_left stream_nth_ne_none,
     existsi ifp_n,
     have ifp_n_fr_ne_zero : ifp_n.fr ≠ 0, from nth_fr_ne_zero ifp_n stream_nth_eq,
     cases ifp_n with _ ifp_n_fr,

src/algebra/continued_fractions/convergents_equiv.lean

@@ -269,7 +269,7 @@ begin
   { have : squash_gcf g n = g, from squash_gcf_eq_self_of_terminated terminated_at_n,
     simp only [this, (convergents_stable_of_terminated n.le_succ terminated_at_n)] },
   { obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.nth n = some gp_n, from
-      with_one.ne_one_iff_exists.elim_left not_terminated_at_n,
+      option.ne_none_iff_exists.elim_left not_terminated_at_n,
     have b_ne_zero : b ≠ 0, from nth_part_denom_ne_zero (part_denom_eq_s_b s_nth_eq),
     cases n with n',
     case nat.zero
@@ -358,7 +358,7 @@ begin
           { -- the difficult case at the squashed position: we first obtain the values from
             -- the sequence
             obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.nth (m + 1) = some gp_succ_m, from
-              with_one.ne_one_iff_exists.elim_left not_terminated_at_n,
+              option.ne_none_iff_exists.elim_left not_terminated_at_n,
             obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.nth m = some gp_m, from
               g.s.ge_stable m.le_succ s_succ_mth_eq,
             -- we then plug them into the recurrence

src/algebra/group/with_one.lean

@@ -55,9 +55,6 @@ option.cases_on
 instance [has_mul α] : has_mul (with_one α) :=
 { mul := option.lift_or_get (*) }
 
-@[simp, to_additive]
-lemma mul_coe [has_mul α] (a b : α) : (a : with_one α) * b = (a * b : α) := rfl
-
 @[to_additive]
 instance [semigroup α] : monoid (with_one α) :=
 { mul_assoc := (option.lift_or_get_assoc _).1,
@@ -118,6 +115,11 @@ lift (coe ∘ f) (λ x y, coe_inj.2 $ hf x y)
 
 end map
 
+attribute [irreducible] with_one
+
+@[simp, norm_cast, to_additive]
+lemma coe_mul [has_mul α] (a b : α) : ((a * b : α) : with_one α) = a * b := rfl
+
 end with_one
 
 namespace with_zero
@@ -133,8 +135,14 @@ instance [has_mul α] : mul_zero_class (with_zero α) :=
   mul_zero  := λ a, by cases a; refl,
   ..with_zero.has_zero }
 
-@[simp] lemma mul_coe [has_mul α] (a b : α) :
-  (a : with_zero α) * b = (a * b : α) := rfl
+@[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 [semigroup α] : semigroup (with_zero α) :=
 { mul_assoc := λ a b c, match a, b, c with
@@ -176,8 +184,9 @@ do a ← x, return a⁻¹
 
 instance [has_inv α] : has_inv (with_zero α) := ⟨with_zero.inv⟩
 
-@[simp] lemma inv_coe [has_inv α] (a : α) :
-  (a : with_zero α)⁻¹ = (a⁻¹ : α) := rfl
+@[simp, norm_cast] lemma coe_inv [has_inv α] (a : α) :
+  ((a⁻¹ : α) : with_zero α) = a⁻¹ := rfl
+
 @[simp] lemma inv_zero [has_inv α] :
   (0 : with_zero α)⁻¹ = 0 := rfl
 
@@ -206,17 +215,17 @@ lemma one_div (x : with_zero α) : 1 / x = x⁻¹ := one_mul _
 
 @[simp] lemma mul_right_inv : ∀  (x : with_zero α) (h : x ≠ 0), x * x⁻¹ = 1
 | 0       h := false.elim $ h rfl
-| (a : α) h := by simp [coe_one]
+| (a : α) h := by {norm_cast, simp [coe_one]}
 
 @[simp] lemma mul_left_inv : ∀  (x : with_zero α) (h : x ≠ 0), x⁻¹ * x = 1
 | 0       h := false.elim $ h rfl
-| (a : α) h := by simp [coe_one]
+| (a : α) h := by {norm_cast, simp [coe_one]}
 
 @[simp] lemma mul_inv_rev : ∀ (x y : with_zero α), (x * y)⁻¹ = y⁻¹ * x⁻¹
 | 0       0       := rfl
 | 0       (b : α) := rfl
 | (a : α) 0       := rfl
-| (a : α) (b : α) := by simp
+| (a : α) (b : α) := by {norm_cast, exact _root_.mul_inv_rev _ _}
 
 @[simp] lemma mul_div_cancel {a b : with_zero α} (hb : b ≠ 0) : a * b / b = a :=
 show _ * _ * _ = _, by simp [mul_assoc, hb]
@@ -227,6 +236,21 @@ show _ * _ * _ = _, by simp [mul_assoc, hb]
 lemma div_eq_iff_mul_eq {a b c : with_zero α} (hb : b ≠ 0) : a / b = c ↔ c * b = a :=
 by split; intro h; simp [h.symm, hb]
 
+lemma mul_inv_cancel : ∀ (a : with_zero α), a ≠ 0 → a * a⁻¹ = 1 :=
+begin
+  rintro (_ | a) h,
+    {exact absurd rfl h },
+    { refine option.some_inj.2 (_root_.mul_right_inv _) }
+end
+
+/-- if `G` is a group then `with_zero G` is a group with zero. -/
+instance : group_with_zero (with_zero α) :=
+{ inv_zero := with_zero.inv_zero,
+  mul_inv_cancel := with_zero.mul_inv_cancel,
+  ..with_zero.monoid_with_zero,
+  ..with_zero.has_inv,
+  ..with_zero.nontrivial
+}
 end group
 
 section comm_group
@@ -250,6 +274,24 @@ begin
   { rw [mul_inv_eq_iff_eq_mul, mul_right_comm, mul_comm c, ← H, mul_inv_cancel_right] }
 end
 
+theorem mul_comm {α : Type u}
+  [comm_group α] :
+  ∀ (a b : with_zero α), a * b = b * a :=
+begin
+  rintro (_ | a) (_ | b),
+  { refl },
+  { refl },
+  { refl },
+  { apply option.some_inj.2,
+    apply mul_comm
+  }
+end
+
+/-- if `G` is a `comm_group` then `with_zero G` is a `comm_group_with_zero`. -/
+instance : comm_group_with_zero (with_zero α) :=
+{ mul_comm := mul_comm,
+  ..with_zero.group_with_zero }
+
 end comm_group
 
 section semiring
@@ -272,4 +314,6 @@ instance [semiring α] : semiring (with_zero α) :=
 
 end semiring
 
+attribute [irreducible] with_zero
+
 end with_zero

src/algebra/ordered_group.lean

@@ -241,6 +241,8 @@ end units
 
 namespace with_zero
 
+local attribute [semireducible] with_zero
+
 instance [preorder α] : preorder (with_zero α) := with_bot.preorder
 instance [partial_order α] : partial_order (with_zero α) := with_bot.partial_order
 instance [partial_order α] : order_bot (with_zero α) := with_bot.order_bot
@@ -313,6 +315,8 @@ end has_one
 instance [has_add α] : has_add (with_top α) :=
 ⟨λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b))⟩
 
+local attribute [reducible] with_zero
+
 instance [add_semigroup α] : add_semigroup (with_top α) :=
 { add := (+),
   ..@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _ }
@@ -378,7 +382,7 @@ coe_lt_coe
 @[simp] lemma top_add [ordered_add_comm_monoid α] {a : with_top α} : ⊤ + a = ⊤ := rfl
 
 lemma add_eq_top [ordered_add_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
-by cases a; cases b; simp [none_eq_top, some_eq_coe, coe_add.symm]
+by {cases a; cases b; simp [none_eq_top, some_eq_coe, ←with_top.coe_add, ←with_zero.coe_add]}
 
 lemma add_lt_top [ordered_add_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
 by simp [lt_top_iff_ne_top, add_eq_top, not_or_distrib]
@@ -493,6 +497,8 @@ lemma le_add_right (h : a ≤ b) : a ≤ b + c :=
 calc a = a + 0 : by simp
   ... ≤ b + c : add_le_add h (zero_le _)
 
+local attribute [semireducible] with_zero
+
 instance with_zero.canonically_ordered_add_monoid :
   canonically_ordered_add_monoid (with_zero α) :=
 { le_iff_exists_add := λ a b, begin
@@ -793,6 +799,8 @@ lemma with_top.add_lt_add_iff_left :
     { norm_cast, exact add_lt_add_iff_left _ }
   end
 
+local attribute [reducible] with_zero
+
 lemma with_top.add_lt_add_iff_right
   {a b c : with_top α} : a < ⊤ → (c + a < b + a ↔ c < b) :=
 by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c

src/data/polynomial/ring_division.lean

@@ -87,6 +87,8 @@ begin
   rw [nat_degree_mul h2.1 h2.2], exact nat.le_add_right _ _
 end
 
+local attribute [reducible] with_zero
+
 lemma exists_finset_roots : ∀ {p : polynomial R} (hp : p ≠ 0),
   ∃ s : finset R, (s.card : with_bot ℕ) ≤ degree p ∧ ∀ x, x ∈ s ↔ is_root p x
 | p := λ hp, by haveI := classical.prop_decidable (∃ x, is_root p x); exact

src/data/seq/seq.lean

@@ -91,7 +91,7 @@ lemma ge_stable (s : seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
   ∃ (aₘ : α), s.nth m = some aₘ :=
 have s.nth n ≠ none, by simp [s_nth_eq_some],
 have s.nth m ≠ none, from mt (s.le_stable m_le_n) this,
-with_one.ne_one_iff_exists.elim_left this
+option.ne_none_iff_exists.1 this
 
 theorem not_mem_nil (a : α) : a ∉ @nil α :=
 λ ⟨n, (h : some a = none)⟩, by injection h