chore: bump Std for #251 (#7126)

Some minor renaming: * `Sum.not_isLeft` becomes `Sum.bnot_isLeft` * `Sum.Not_isLeft` becomes `Sum.not_isLeft` A few explicit arguments also became implicit. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Sep 12, 2023 · fc20085 · fc20085
1 parent 127feab
commit fc20085
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 415 deletions.
diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean
@@ -357,7 +357,7 @@ end Pi
 
 theorem Sum.elim_intCast_intCast {α β γ : Type*} [IntCast γ] (n : ℤ) :
     Sum.elim (n : α → γ) (n : β → γ) = n :=
-  @Sum.elim_lam_const_lam_const α β γ n
+  Sum.elim_lam_const_lam_const (γ := γ) n
 #align sum.elim_int_cast_int_cast Sum.elim_intCast_intCast
 
 /-! ### Order dual -/

diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean
@@ -203,7 +203,7 @@ end Pi
 
 theorem Sum.elim_natCast_natCast {α β γ : Type*} [NatCast γ] (n : ℕ) :
     Sum.elim (n : α → γ) (n : β → γ) = n :=
-  @Sum.elim_lam_const_lam_const α β γ n
+  Sum.elim_lam_const_lam_const (γ := γ) n
 #align sum.elim_nat_cast_nat_cast Sum.elim_natCast_natCast
 
 -- Guard against import creep regression.