feat: synchronize with mathlib3#18080/18160/18174 (#1519)

- [x] leanprover-community/mathlib#18080
- [x] leanprover-community/mathlib#18160
- [ ] leanprover-community/mathlib#18174



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Algebra/Group/Basic.lean

@@ -734,12 +734,36 @@ theorem div_eq_div_iff_div_eq_div : a / b = c / d ↔ a / c = b / d := by
 
 end CommGroup
 
+section multiplicative
+
+variable [Monoid β] (p r : α → α → Prop) [IsTotal α r] (f : α → α → β)
+
+@[to_additive additive_of_symmetric_of_isTotal]
+lemma multiplicative_of_symmetric_of_isTotal
+    (hsymm : Symmetric p) (hf_swap : ∀ {a b}, p a b → f a b * f b a = 1)
+    (hmul : ∀ {a b c}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c)
+    {a b c : α} (pab : p a b) (pbc : p b c) (pac : p a c) : f a c = f a b * f b c := by
+  have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c := by
+    intros b c rbc pab pbc pac
+    obtain rab | rba := total_of r a b
+    · exact hmul rab rbc pab pbc pac
+    rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
+    obtain rac | rca := total_of r a c
+    · rw [hmul rba rac (hsymm pab) pac pbc]
+    · rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
+  obtain rbc | rcb := total_of r b c
+  · exact hmul' rbc pab pbc pac
+  · rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]
+
+#align multiplicative_of_symmetric_of_is_total multiplicative_of_symmetric_of_isTotal
+#align additive_of_symmetric_of_is_total additive_of_symmetric_of_isTotal
+
 /-- If a binary function from a type equipped with a total relation `r` to a monoid is
   anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
   (i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied. -/
 @[to_additive additive_of_isTotal "If a binary function from a type equipped with a total relation
   `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in order to show
-  it is multiplicative (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and `r b c`
+  it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and `r b c`
   are satisfied."]
 lemma multiplicative_of_isTotal [Monoid β] (f : α → α → β) (r : α → α → Prop) [t : IsTotal α r]
     (hswap : ∀ a b, f a b * f b a = 1)

Mathlib/Algebra/Module/Basic.lean

@@ -328,15 +328,13 @@ end Module
 as an instance because Lean has no way to guess `R`. -/
 protected theorem Module.subsingleton (R M : Type _) [Semiring R] [Subsingleton R] [AddCommMonoid M]
     [Module R M] : Subsingleton M :=
-  ⟨fun x y => by
-    rw [← one_smul R x, ← one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]⟩
+  MulActionWithZero.subsingleton R M
 #align module.subsingleton Module.subsingleton
 
 /-- A semiring is `Nontrivial` provided that there exists a nontrivial module over this semiring. -/
 protected theorem Module.nontrivial (R M : Type _) [Semiring R] [Nontrivial M] [AddCommMonoid M]
     [Module R M] : Nontrivial R :=
-  (subsingleton_or_nontrivial R).resolve_left fun _ =>
-    not_subsingleton M <| Module.subsingleton R M
+  MulActionWithZero.nontrivial R M
 #align module.nontrivial Module.nontrivial
 
 -- see Note [lower instance priority]

Mathlib/Algebra/SMulWithZero.lean

@@ -168,6 +168,17 @@ instance MonoidWithZero.toOppositeMulActionWithZero : MulActionWithZero Rᵐᵒ
   { MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }
 #align monoid_with_zero.to_opposite_mul_action_with_zero MonoidWithZero.toOppositeMulActionWithZero
 
+protected lemma MulActionWithZero.subsingleton
+    [MulActionWithZero R M] [Subsingleton R] : Subsingleton M :=
+  ⟨λ x y => by rw [←one_smul R x, ←one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]⟩
+#align mul_action_with_zero.subsingleton MulActionWithZero.subsingleton
+
+protected lemma MulActionWithZero.nontrivial
+    [MulActionWithZero R M] [Nontrivial M] : Nontrivial R :=
+  (subsingleton_or_nontrivial R).resolve_left fun _ =>
+    not_subsingleton M <| MulActionWithZero.subsingleton R M
+#align mul_action_with_zero.nontrivial MulActionWithZero.nontrivial
+
 variable {R M}
 variable [MulActionWithZero R M] [Zero M'] [SMul R M']
 

Mathlib/Data/Nat/WithBot.lean

@@ -85,6 +85,12 @@ theorem lt_one_iff_le_zero {x : WithBot ℕ} : x < 1 ↔ x ≤ 0 :=
   not_iff_not.mp (by simpa using one_le_iff_zero_lt)
 #align nat.with_bot.lt_one_iff_le_zero Nat.WithBot.lt_one_iff_le_zero
 
+theorem add_one_le_of_lt {n m : WithBot ℕ} (h : n < m) : n + 1 ≤ m := by
+  cases n
+  · exact bot_le
+  cases m
+  exacts [(not_lt_bot h).elim, WithBot.some_le_some.2 (WithBot.some_lt_some.1 h)]
+
 end WithBot
 
 end Nat