style: prefer some/none over .some/.none (leanprover-community#27896)

The notation `.some` and `.none` are very useful when working with other inductive types such as `LOption` which have fields names `some` and/or `none`. But for `Option`, we prefer to simply write `some`/`none`.

[#mathlib4 > style: `.some`/`.none` vs `some`/`none`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/style.3A.20.60.2Esome.60.2F.60.2Enone.60.20vs.20.60some.60.2F.60none.60)

Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>

Author: JovanGerb

Cache/IO.lean

@@ -157,7 +157,7 @@ Usually it is either `.` or something like `./.lake/packages/mathlib/`
 -/
 def getSrcDir (sp : SearchPath) (mod : Name) : IO FilePath := do
 
-  let .some srcDir ← sp.findWithExtBase "lean" mod |
+  let some srcDir ← sp.findWithExtBase "lean" mod |
     throw <| IO.userError s!"Unknown package directory for {mod}\nsearch paths: {sp}"
 
   return srcDir

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -137,8 +137,8 @@ elab "guard_decl" na:ident mod:ident : command => do
   let dcl ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo na
   let mdn := mod.getId
   let env ← getEnv
-  let .some dcli := env.getModuleIdxFor? dcl | unreachable!
-  let .some mdni := env.getModuleIdx? mdn | throwError "the module {mod} is not imported!"
+  let some dcli := env.getModuleIdxFor? dcl | unreachable!
+  let some mdni := env.getModuleIdx? mdn | throwError "the module {mod} is not imported!"
   unless dcli = mdni do throwError "instance {na} is no longer in {mod}."
 
 guard_decl Finsupp.Lex.addLeftMono Mathlib.Data.Finsupp.Lex

LongestPole/Main.lean

@@ -124,7 +124,7 @@ open System in
 def countLOC (modules : List Name) : IO (NameMap Float) := do
   let mut r := {}
   for m in modules do
-    if let .some fp ← Lean.SearchPath.findModuleWithExt [s!".{FilePath.pathSeparator}"] "lean" m
+    if let some fp ← Lean.SearchPath.findModuleWithExt [s!".{FilePath.pathSeparator}"] "lean" m
     then
       let src ← IO.FS.readFile fp
       r := r.insert m (src.toList.count '\n').toFloat

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -188,7 +188,7 @@ def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
     let rbody ← core zα pα body
     let p_pos : Option Q(0 < $e) := ← (do
       let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
-      let .some ps ← proveFinsetNonempty s | pure none
+      let some ps ← proveFinsetNonempty s | pure none
       let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
       let .some instαordsmul ← trySynthInstanceQ q(PosSMulStrictMono ℚ≥0 $α) | pure none
       assumeInstancesCommute

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -292,7 +292,7 @@ def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
     if let some p_pos := p_pos then return .positive p_pos
     -- Try to show that the product is nonnegative
     let p_nonneg : Option Q(0 ≤ $e) := ← do
-      let .some pbody := rbody.toNonneg
+      let some pbody := rbody.toNonneg
         | return none -- Fail if the body is not provably nonnegative
       let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
       -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.

Mathlib/Data/DFinsupp/Notation.lean

@@ -28,7 +28,7 @@ attribute [term_parser] Finsupp.stxSingle₀ Finsupp.stxUpdate₀
 def elabSingle₀ : Elab.Term.TermElab
   | `(term| single₀ $i $x) => fun ty? => do
     Elab.Term.tryPostponeIfNoneOrMVar ty?
-    let .some ty := ty? | Elab.throwUnsupportedSyntax
+    let some ty := ty? | Elab.throwUnsupportedSyntax
     let_expr DFinsupp _ _ _ := ← Meta.withReducible (Meta.whnf ty) | Elab.throwUnsupportedSyntax
     Elab.Term.elabTerm (← `(DFinsupp.single $i $x)) ty?
   | _ => fun _ => Elab.throwUnsupportedSyntax
@@ -38,7 +38,7 @@ def elabSingle₀ : Elab.Term.TermElab
 def elabUpdate₀ : Elab.Term.TermElab
   | `(term| update₀ $f $i $x) => fun ty? => do
     Elab.Term.tryPostponeIfNoneOrMVar ty?
-    let .some ty := ty? | Elab.throwUnsupportedSyntax
+    let some ty := ty? | Elab.throwUnsupportedSyntax
     let_expr DFinsupp _ _ _ := ← Meta.withReducible (Meta.whnf ty) | Elab.throwUnsupportedSyntax
     Elab.Term.elabTerm (← `(DFinsupp.update $f $i $x)) ty?
   | _ => fun _ => Elab.throwUnsupportedSyntax

Mathlib/Data/EReal/Operations.lean

@@ -872,11 +872,11 @@ def evalERealMul : PositivityExt where eval {u α} zα pα e := do
       | _ => pure .none
     | .nonnegative pa =>
       match (← core zα pα b).toNonneg with
-      | .some pb => pure (.nonnegative q(EReal.mul_nonneg $pa $pb))
-      | .none => pure .none
+      | some pb => pure (.nonnegative q(EReal.mul_nonneg $pa $pb))
+      | none => pure .none
     | .nonzero pa =>
       match (← core zα pα b).toNonzero with
-      | .some pb => pure (.nonzero q(mul_ne_zero $pa $pb))
+      | some pb => pure (.nonzero q(mul_ne_zero $pa $pb))
       | none => pure .none
     | _ => pure .none
   | _, _, _ => throwError "not a product of 2 `EReal`s"

Mathlib/Data/Fin/Tuple/Reflection.lean

@@ -223,9 +223,9 @@ simproc_decl prod_univ_ofNat (∏ _ : Fin _, _) := .ofQ fun u _ e => do
   match u, e with
   | .succ _, ~q(@Finset.prod (Fin $n) _ $inst (@Finset.univ _ $instF) $f) => do
     match (generalizing := false) n.nat? with
-    | .none =>
+    | none =>
       return .continue
-    | .some nVal =>
+    | some nVal =>
       let ⟨res, pf⟩ ← mkProdEqQ inst nVal f
       let ⟨_⟩ ← assertDefEqQ q($instF) q(Fin.fintype _)
       have _ : $n =Q $nVal := ⟨⟩
@@ -237,9 +237,9 @@ simproc_decl sum_univ_ofNat (∑ _ : Fin _, _) := .ofQ fun u _ e => do
   match u, e with
   | .succ _, ~q(@Finset.sum (Fin $n) _ $inst (@Finset.univ _ $instF) $f) => do
     match n.nat? with
-    | .none =>
+    | none =>
       return .continue
-    | .some nVal =>
+    | some nVal =>
       let ⟨res, pf⟩ ← mkSumEqQ inst nVal f
       let ⟨_⟩ ← assertDefEqQ q($instF) q(Fin.fintype _)
       have _ : $n =Q $nVal := ⟨⟩

Mathlib/Data/Fin/VecNotation.lean

@@ -163,7 +163,7 @@ dsimproc cons_val (Matrix.vecCons _ _ _) := fun e => do
     let etailn_whnf : Q(ℕ) ← Meta.whnfD etailn
     if let Expr.lit (.natVal length) := etailn_whnf then
       pure (length, false, q(OfNat.ofNat $etailn_whnf))
-    else if let .some ((base : Q(ℕ)), offset) ← (Meta.isOffset? etailn_whnf).run then
+    else if let some ((base : Q(ℕ)), offset) ← (Meta.isOffset? etailn_whnf).run then
       let offset_e : Q(ℕ) := mkNatLit offset
       pure (offset, true, q($base + $offset))
     else

Mathlib/Data/Finsupp/Option.lean

@@ -67,7 +67,7 @@ theorem embDomain_some_some [Zero M] (f : α →₀ M) (x) : f.embDomain .some (
 
 @[simp]
 theorem some_update_none [Zero M] (f : Option α →₀ M) (a : M) :
-    (f.update .none a).some = f.some := by
+    (f.update none a).some = f.some := by
   ext
   simp [Finsupp.update]
 
@@ -76,8 +76,8 @@ pairs of an element and a `Finsupp` on the original type. -/
 @[simps]
 noncomputable
 def optionEquiv [Zero M] : (Option α →₀ M) ≃ M × (α →₀ M) where
-  toFun P := (P .none, P.some)
-  invFun P := (P.2.embDomain .some).update .none P.1
+  toFun P := (P none, P.some)
+  invFun P := (P.2.embDomain .some).update none P.1
   left_inv P := by ext (_ | a) <;> simp [Finsupp.update]
   right_inv P := by ext <;> simp [Finsupp.update]
 
@@ -108,7 +108,7 @@ theorem sum_option_index_smul [Semiring R] [AddCommMonoid M] [Module R M] (f : O
 @[simp] lemma some_embDomain_some [Zero M] (f : α →₀ M) : (f.embDomain .some).some = f := by
   ext; rw [some_apply]; exact embDomain_apply _ _ _
 
-@[simp] lemma embDomain_some_none [Zero M] (f : α →₀ M) : f.embDomain .some .none = 0 :=
+@[simp] lemma embDomain_some_none [Zero M] (f : α →₀ M) : f.embDomain .some none = 0 :=
   embDomain_notin_range _ _ _ (by simp)
 
 end Option