What's Changed

• feat: upstream List.attach and Array.attach from Batteries by @llllvvuu in https://github.com/leanprover/lean4/pull/4586
• fix: typo hearbeats -> heartbeats by @kmill in https://github.com/leanprover/lean4/pull/4590
• feat: total ByteArray.toList/findIdx? by @Vtec234 in https://github.com/leanprover/lean4/pull/4582
• chore: release triggers update of release.lean-lang.org by @nomeata in https://github.com/leanprover/lean4/pull/4531
• chore: begin development cycle for v4.11.0 by @semorrison in https://github.com/leanprover/lean4/pull/4594
• chore: pr-release: adjust to new lakefile.lean syntax by @nomeata in https://github.com/leanprover/lean4/pull/4598
• fix: adapt kernel interruption to new cancellation system by @Kha in https://github.com/leanprover/lean4/pull/4584
• feat: omega error message: normalize constraint order by @nomeata in https://github.com/leanprover/lean4/pull/4612
• fix: diagnostics: show kernel diags even if it is the only section by @nomeata in https://github.com/leanprover/lean4/pull/4611
• feat: termination_by structural by @nomeata in https://github.com/leanprover/lean4/pull/4542
• feat: mul recurrence theorems for LeanSAT by @bollu in https://github.com/leanprover/lean4/pull/4568
• fix: unresolve name avoiding locals by @digama0 in https://github.com/leanprover/lean4/pull/4593
• feat: Nat.and_le_(left|right) by @TwoFX in https://github.com/leanprover/lean4/pull/4597
• feat: additional lemmas for Option by @TwoFX in https://github.com/leanprover/lean4/pull/4599
• feat: additional lemmas for lists by @TwoFX in https://github.com/leanprover/lean4/pull/4602
• feat: getElem_congr by @TwoFX in https://github.com/leanprover/lean4/pull/4603
• feat: additional lemmas for cond by @TwoFX in https://github.com/leanprover/lean4/pull/4604
• feat: additional lemmas for bounded integers by @TwoFX in https://github.com/leanprover/lean4/pull/4605
• chore: defs that should be theorems by @semorrison in https://github.com/leanprover/lean4/pull/4619
• chore: delete deprecations from 2022 by @semorrison in https://github.com/leanprover/lean4/pull/4618
• chore: satisfy duplicate namespace linter by @semorrison in https://github.com/leanprover/lean4/pull/4616
• chore: follow simpNF linter's advice by @semorrison in https://github.com/leanprover/lean4/pull/4620
• chore: add 'since' dates to deprecated by @semorrison in https://github.com/leanprover/lean4/pull/4617
• chore: make constructor-as-variable test more robust by @TwoFX in https://github.com/leanprover/lean4/pull/4625
• fix: enforce isDefEqStuckEx at unstuckMVar procedure by @leodemoura in https://github.com/leanprover/lean4/pull/4596
• fix: Windows build by @Kha in https://github.com/leanprover/lean4/pull/4628
• chore: pr-release: use right tag name by @nomeata in https://github.com/leanprover/lean4/pull/4632
• fix: set default value of pp.instantiateMVars to true and make the option be effective by @kmill in https://github.com/leanprover/lean4/pull/4558
• feat: USize.and_toNat by @TwoFX in https://github.com/leanprover/lean4/pull/4629
• feat: Option.or by @TwoFX in https://github.com/leanprover/lean4/pull/4600
• chore: typo by @alok in https://github.com/leanprover/lean4/pull/4635
• feat: safe exponentiation by @leodemoura in https://github.com/leanprover/lean4/pull/4637
• fix: make sure syntax nodes always run their formatters by @kmill in https://github.com/leanprover/lean4/pull/4631
• chore: manual nightly trigger by @Kha in https://github.com/leanprover/lean4/pull/4638
• chore: CI: restart-on-label: view run more often by @nomeata in https://github.com/leanprover/lean4/pull/4640
• refactor: include declNames in Structural.EqnInfo by @nomeata in https://github.com/leanprover/lean4/pull/4639
• fix: snapshot subtree was not restored on reuse by @Kha in https://github.com/leanprover/lean4/pull/4643
• refactor: lambdaBoundedTelescope by @nomeata in https://github.com/leanprover/lean4/pull/4642
• fix: improve synthAppInstances by @leodemoura in https://github.com/leanprover/lean4/pull/4646
• feat: EquivBEq and LawfulHashable classes by @TwoFX in https://github.com/leanprover/lean4/pull/4607
• feat: additional lemmas for arrays by @TwoFX in https://github.com/leanprover/lean4/pull/4627
• fix: universe level in .below and .brecOn construction by @nomeata in https://github.com/leanprover/lean4/pull/4651
• refactor: Split Constructions module by @nomeata in https://github.com/leanprover/lean4/pull/4656
• feat: Std.HashMap by @TwoFX in https://github.com/leanprover/lean4/pull/4583
• chore: restart-on-label: wait for 30s by @nomeata in https://github.com/leanprover/lean4/pull/4663
• fix: don't set pp.tagAppFns when pretty printing signatures by @kmill in https://github.com/leanprover/lean4/pull/4665
• fix: move Std from libleanshared to much smaller libInit_shared by @Kha in https://github.com/leanprover/lean4/pull/4661
• fix: explicitly initialize Std in lean_initialize by @Kha in https://github.com/leanprover/lean4/pull/4668
• chore: make Antisymm a Prop by @semorrison in https://github.com/leanprover/lean4/pull/4666
• fix: hasBadParamDep? to look at term, not type by @nomeata in https://github.com/leanprover/lean4/pull/4672
• chore: bump actions/checkout and actions/upload-artifacts by @nomeata in https://github.com/leanprover/lean4/pull/4664
• chore: cleanup unused arguments (from linter) by @semorrison in https://github.com/leanprover/lean4/pull/4621
• fix: unorphan modules in Init by @TwoFX in https://github.com/leanprover/lean4/pull/4680
• fix: unorphan modules in Std.Data by @TwoFX in https://github.com/leanprover/lean4/pull/4679
• chore: update codeowners by @TwoFX in https://github.com/leanprover/lean4/pull/4681
• chore: Inhabited instances for Std.HashMap by @TwoFX in https://github.com/leanprover/lean4/pull/4682
• chore: fix "max dynamic symbols" metric by @Kha in https://github.com/leanprover/lean4/pull/4669
• fix: calculate error suppression per snapshot by @Kha in https://github.com/leanprover/lean4/pull/4657
• chore: update comments in kernel/declaration.h by @nomeata in https://github.com/leanprover/lean4/pull/4683
• feat: structural mutual recursion by @nomeata in https://github.com/leanprover/lean4/pull/4575
• feat: Process.tryWait by @hargoniX in https://github.com/leanprover/lean4/pull/4660
• chore: adjust List.replicate simp lemmas by @semorrison in https://github.com/leanprover/lean4/pull/4687
• chore: upstream ToExpr FilePath and compile_time_search_path% by @semorrison in https://github.com/leanprover/lean4/pull/4453
• chore: forward and backward directions of not_exists by @semorrison in https://github.com/leanprover/lean4/pull/4688
• chore: upstream SMap.foldM by @semorrison in https://github.com/leanprover/lean4/pull/4690
• chore: improve compatibility of tests/list_simp with Mathlib by @semorrison in https://github.com/leanprover/lean4/pull/4691
• chore: add step to release checklist by @semorrison in https://github.com/leanprover/lean4/pull/4693
• refactor: InductiveVal.numNested instead of .isNested by @nomeata in https://github.com/leanprover/lean4/pull/4684
• feat: make @[ext] derive ext_iff theorems from user ext theorems by @kmill in https://github.com/leanprover/lean4/pull/4543
• chore: upstream eq_iff_true_of_subsingleton by @semorrison in https://github.com/leanprover/lean4/pull/4689
• chore: make use of ext_iff realization now that stage0 is updated by @kmill in https://github.com/leanprover/lean4/pull/4694
• feat: lake: require @ git by @tydeu in https://github.com/leanprover/lean4/pull/4692
• feat: omega doesn't push coercion over multiplication unnecessarily by @semorrison in https://github.com/leanprover/lean4/pull/4695
• feat: chore upstream List.Sublist and API from Batteries by @semorrison in https://github.com/leanprover/lean4/pull/4697
• fix: prefer original module in const2ModIdx by @digama0 in https://github.com/leanprover/lean4/pull/4652
• feat: characterisations of List.Sublist by @semorrison in https://github.com/leanprover/lean4/pull/4704
• feat: basic material on List.Pairwise and Nodup by @semorrison in https://github.com/leanprover/lean4/pull/4706
• doc: update release checklist for new release notes workflow by @kmill in https://github.com/leanprover/lean4/pull/4458
• feat: lemmas for List.head and List.getLast by @semorrison in https://github.com/leanprover/lean4/pull/4678
• feat: simp normal form tests for Pairwise and Nodup by @semorrison in https://github.com/leanprover/lean4/pull/4707
• chore: reorganise lemmas on list getters by @semorrison in https://github.com/leanprover/lean4/pull/4708
• fix: Repr instances for Int and Float by @leodemoura in https://github.com/leanprover/lean4/pull/4709
• fix: decide tactic transparency by @leodemoura in https://github.com/leanprover/lean4/pull/4711
• fix: make iff theorem generated by @[ext] preserve inst implicits by @kmill in https://github.com/leanprover/lean4/pull/4710
• fix: deprecated warnings for overloaded symbols by @leodemoura in https://github.com/leanprover/lean4/pull/4713
• fix: mutual structural recursion: check that datatype parameters agree by @nomeata in https://github.com/leanprover/lean4/pull/4715
• feat: upstream more erase API by @semorrison in https://github.com/leanprover/lean4/pull/4720
• chore: fix typo in doc-string by @grunweg in https://github.com/leanprover/lean4/pull/4719
• feat: further theorems for List.erase by @semorrison in https://github.com/leanprover/lean4/pull/4723
• fix: make matcher pretty printer sensitive to pp.explicit by @kmill in https://github.com/leanprover/lean4/pull/4724
• fix: nested structural recursion over reflexive data type by @nomeata in https://github.com/leanprover/lean4/pull/4728
• feat: detailed feedback on decide tactic failure by @kmill in https://github.com/leanprover/lean4/pull/4674
• feat: Meta.withErasedFVars by @nomeata in https://github.com/leanprover/lean4/pull/4731
• feat: add #discr_tree_key command and discr_tree_key tactic by @mattrobball in https://github.com/leanprover/lean4/pull/4447
• feat: .below and .brecOn for nested inductive by @nomeata in https://github.com/leanprover/lean4/pull/4658
• refactor: use indVal.numNested or indVal.numTypeFormers where applicable by @nomeata in https://github.com/leanprover/lean4/pull/4734
• feat: lake: cleaner release handling & related touchups by @tydeu in https://github.com/leanprover/lean4/pull/4735
• doc: fix misplaced docstring for getThe by @sullyj3 in https://github.com/leanprover/lean4/pull/4737
• refactor: IndGroupInfo and IndGroupInst by @nomeata in https://github.com/leanprover/lean4/pull/4738
• test: extend test for #4671 with nice example reported on zulip by @nomeata in https://github.com/leanprover/lean4/pull/4740
• feat: infer mutual structural recursion by @nomeata in https://github.com/leanprover/lean4/pull/4718
• feat: structural recursion over nested datatypes by @nomeata in https://github.com/leanprover/lean4/pull/4733
• feat: PProd and MProd syntax (part 1) by @nomeata in https://github.com/leanprover/lean4/pull/4747
• feat: PProd and MProd syntax (part 2) by @nomeata in https://github.com/leanprover/lean4/pull/4730
• chore: exclude more symbols to get below Windows symbol limit by @Kha in https://github.com/leanprover/lean4/pull/4746
• chore: rename HashMap.remove to HashMap.erase by @TwoFX in https://github.com/leanprover/lean4/pull/4725
• chore: missing profileitM by @leodemoura in https://github.com/leanprover/lean4/pull/4753
• feat: add Lean.Expr.numObjs by @leodemoura in https://github.com/leanprover/lean4/pull/4754
• chore: rename TC to Relation.TransGen by @semorrison in https://github.com/leanprover/lean4/pull/4760
• chore: add comment for why anonymous constructor notation isn't flattened during pretty printing by @kmill in https://github.com/leanprover/lean4/pull/4764
• feat: PProd syntax (part 3) by @nomeata in https://github.com/leanprover/lean4/pull/4756
• refactor: move Synax.hasIdent, shake dependencies by @nomeata in https://github.com/leanprover/lean4/pull/4766
• perf: add ShareCommon.shareCommon' by @leodemoura in https://github.com/leanprover/lean4/pull/4767
• chore: add missing withTraceNode by @leodemoura in https://github.com/leanprover/lean4/pull/4769
• feat: simprocs for #[1,2,3,4,5][2] by @semorrison in https://github.com/leanprover/lean4/pull/4765
• chore: fix BEq argument order in hash map lemmas by @TwoFX in https://github.com/leanprover/lean4/pull/4732
• fix: resolve instances for HashMap via unification by @TwoFX in https://github.com/leanprover/lean4/pull/4759
• doc: mention linearity in hash map docstring by @TwoFX in https://github.com/leanprover/lean4/pull/4771
• chore: simplify shareCommon' by @leodemoura in https://github.com/leanprover/lean4/pull/4775
• perf: Replacement.apply by @leodemoura in https://github.com/leanprover/lean4/pull/4776
• fix: missing assignment validation at closeMainGoal by @leodemoura in https://github.com/leanprover/lean4/pull/4777
• feat: improve @[ext] error message when ext_iff generation fails by @kmill in https://github.com/leanprover/lean4/pull/4762
• feat: add some low level helper APIs by @leodemoura in https://github.com/leanprover/lean4/pull/4778
• fix: have elabAsElim check inferred motive for type correctness by @kmill in https://github.com/leanprover/lean4/pull/4722
• perf: ensure Expr.replaceExpr preserve DAG structure in Exprs by @leodemoura in https://github.com/leanprover/lean4/pull/4779
• chore: document replaceUnsafeM issue by @leodemoura in https://github.com/leanprover/lean4/pull/4783
• fix: .eq_def theorem generation with messy universes by @leodemoura in https://github.com/leanprover/lean4/pull/4712
• chore: Simp.Config.implicitDefEqProofs := true by default by @leodemoura in https://github.com/leanprover/lean4/pull/4784
• refactor: IndGroupInst.brecOn by @nomeata in https://github.com/leanprover/lean4/pull/4787
• refactor: add numFixed to Structural.EqnInfo by @nomeata in https://github.com/leanprover/lean4/pull/4788
• fix: add term elaborator for Lean.Parser.Term.namedPattern by @leodemoura in https://github.com/leanprover/lean4/pull/4792
• feat: theory from LeanSAT by @hargoniX in https://github.com/leanprover/lean4/pull/4742
• perf: for_each with precise cache by @leodemoura in https://github.com/leanprover/lean4/pull/4794
• perf: find? and findExt? by @leodemoura in https://github.com/leanprover/lean4/pull/4795
• perf: kernel replace with precise cache by @leodemoura in https://github.com/leanprover/lean4/pull/4796
• fix: for_each_fn.cpp by @leodemoura in https://github.com/leanprover/lean4/pull/4797
• fix: replace_fn.cpp by @leodemoura in https://github.com/leanprover/lean4/pull/4798
• perf: Expr.replace by @leodemoura in https://github.com/leanprover/lean4/pull/4799
• doc: remove reference to HashMap.find? from Option docstring by @TwoFX in https://github.com/leanprover/lean4/pull/4782
• fix: remove typeclass assumptions for Nodup.eraseP by @TwoFX in https://github.com/leanprover/lean4/pull/4790
• feat: usize for array types by @fgdorais in https://github.com/leanprover/lean4/pull/4801
• feat: use usize for array types by @fgdorais in https://github.com/leanprover/lean4/pull/4802
• refactor: FunInd overhaul by @nomeata in https://github.com/leanprover/lean4/pull/4789
• refactor: Introduce PProdN module by @nomeata in https://github.com/leanprover/lean4/pull/4807
• chore: remove bif from hash map lemmas by @TwoFX in https://github.com/leanprover/lean4/pull/4791
• feat: functional induction for mutual structural recursion by @nomeata in https://github.com/leanprover/lean4/pull/4772
• feat: unnecessary termination_by clauses cause warnings, not errors by @nomeata in https://github.com/leanprover/lean4/pull/4809
• doc: document Command.Scope by @grunweg in https://github.com/leanprover/lean4/pull/4748
• fix: make elab_as_elim eagerly elaborate arguments for parameters appearing in the types of targets by @kmill in https://github.com/leanprover/lean4/pull/4800
• feat: more hash map lemmas by @TwoFX in https://github.com/leanprover/lean4/pull/4803
• doc: update quickstart guide by @mhuisi in https://github.com/leanprover/lean4/pull/4806
• chore: release notes for mutual structural induction by @nomeata in https://github.com/leanprover/lean4/pull/4808
• feat: safer #eval, and #eval! by @nomeata in https://github.com/leanprover/lean4/pull/4810
• test: update test output following stage0 update by @nomeata in https://github.com/leanprover/lean4/pull/4815
• test: test case for #4751 by @nomeata in https://github.com/leanprover/lean4/pull/4819
• chore: List.filterMapM runs and returns left-to-right by @semorrison in https://github.com/leanprover/lean4/pull/4820
• feat: trailing whitespace changes should not invalidate imports by @Kha in https://github.com/leanprover/lean4/pull/4580
• feat: respond to info view requests as soon as relevant tactic has finished execution by @Kha in https://github.com/leanprover/lean4/pull/4727
• fix: make sure anonymous dot notation works with pi-type-valued type synonyms by @kmill in https://github.com/leanprover/lean4/pull/4818
• feat: create ci workflow on lake new/init by @austinletson in https://github.com/leanprover/lean4/pull/4608
• fix: filter duplicate subexpressions by @mhuisi in https://github.com/leanprover/lean4/pull/4786
• test: make #1697 test case Linux-Debug safe by @nomeata in https://github.com/leanprover/lean4/pull/4829
• chore: report github actions failure on zulip by @nomeata in https://github.com/leanprover/lean4/pull/4830
• fix: structural recursion: do not check for brecOn too early by @nomeata in https://github.com/leanprover/lean4/pull/4831
• chore: upstream IsPrefix/IsSuffix/IsInfix by @semorrison in https://github.com/leanprover/lean4/pull/4836
• feat: gaps/cleanup in List lemmas by @semorrison in https://github.com/leanprover/lean4/pull/4835
• feat: List.IsPrefix/IsSuffix is decidable by @semorrison in https://github.com/leanprover/lean4/pull/4837
• chore: upon nightly release, trigger nightly_bump_toolchain on mathlib4 by @nomeata in https://github.com/leanprover/lean4/pull/4838
• chore: fix List deprecations by @semorrison in https://github.com/leanprover/lean4/pull/4842
• chore: correct List.Subset lemma names by @semorrison in https://github.com/leanprover/lean4/pull/4843
• fix: calling programs with spaces on Windows by @Kha in https://github.com/leanprover/lean4/pull/4515
• doc: lake: require @ git in README by @tydeu in https://github.com/leanprover/lean4/pull/4849
• feat: lake: CLI options to control output & failure log levels by @tydeu in https://github.com/leanprover/lean4/pull/4847
• feat: bitVec shiftLeft recurrences for bitblasting by @bollu in https://github.com/leanprover/lean4/pull/4571
• chore: cleanups for Mathlib.Init by @semorrison in https://github.com/leanprover/lean4/pull/4852
• fix: handle unimported builtin names for location links by @kmill in https://github.com/leanprover/lean4/pull/4780
• chore: update Topological.lean by @eltociear in https://github.com/leanprover/lean4/pull/4853
• feat: upstream more List operations by @semorrison in https://github.com/leanprover/lean4/pull/4855
• fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance, no chaining by @nomeata in https://github.com/leanprover/lean4/pull/4839
• refactor: IndPredBelow: use apply_assumption by @nomeata in https://github.com/leanprover/lean4/pull/4841
• fix: handle dependent fields when deriving BEq by @arthur-adjedj in https://github.com/leanprover/lean4/pull/3792
• feat: upstream more List lemmas by @semorrison in https://github.com/leanprover/lean4/pull/4856
• chore: CI: fix msys2 by @Kha in https://github.com/leanprover/lean4/pull/4859
• chore: fix universe in PSigma.exists by @semorrison in https://github.com/leanprover/lean4/pull/4862
• feat: more than one optional argument can be omitted while pretty printing by @kmill in https://github.com/leanprover/lean4/pull/4854
• fix: make elabAsElim aware of explicit motive arguments by @kmill in https://github.com/leanprover/lean4/pull/4817
• refactor: deriving DecidableEq to use termination_by structural by @nomeata in https://github.com/leanprover/lean4/pull/4826
• chore: split Init.Data.List.Lemmas by @semorrison in https://github.com/leanprover/lean4/pull/4863
• chore: upstream List.pairwise_iff_getElem by @semorrison in https://github.com/leanprover/lean4/pull/4866
• chore: upstream List.eraseIdx lemmas by @semorrison in https://github.com/leanprover/lean4/pull/4865
• chore: fix naming of List.Subset lemmas by @semorrison in https://github.com/leanprover/lean4/pull/4868
• perf: precise cache for foldConsts by @leodemoura in https://github.com/leanprover/lean4/pull/4871
• chore: fix binder explicitness in List.map_subset by @semorrison in https://github.com/leanprover/lean4/pull/4877
• chore: rename PSigma.exists by @semorrison in https://github.com/leanprover/lean4/pull/4878
• fix: mistake in statement of List.take_takeWhile by @kmill in https://github.com/leanprover/lean4/pull/4875
• chore: copy release notes from releases/v4.10.0 by @kmill in https://github.com/leanprover/lean4/pull/4864
• fix: make "use `set_option diagnostics true" message conditional on current setting by @kmill in https://github.com/leanprover/lean4/pull/4781
• chore: updates to release_checklist.md by @semorrison in https://github.com/leanprover/lean4/pull/4876
• chore: correct doc-string for Array.swap! by @semorrison in https://github.com/leanprover/lean4/pull/4869
• refactor: split out Lean.Language.Lean.Types by @Kha in https://github.com/leanprover/lean4/pull/4881
• feat: include command by @Kha in https://github.com/leanprover/lean4/pull/4883
• fix: make import resolution case-sensitive on all platforms by @Kha in https://github.com/leanprover/lean4/pull/4538
• feat: Nat simprocs for simplifying bit expressions by @bollu in https://github.com/leanprover/lean4/pull/4874
• chore: shorten suggestion about diagnostics by @semorrison in https://github.com/leanprover/lean4/pull/4882
• refactor: sharecommon by @leodemoura in https://github.com/leanprover/lean4/pull/4887
• feat: ushiftRight bitblasting by @bollu in https://github.com/leanprover/lean4/pull/4872
• perf: precise cache for expr_eq_fn by @leodemoura in https://github.com/leanprover/lean4/pull/4890
• fix: export symbols needed by Verso by @david-christiansen in https://github.com/leanprover/lean4/pull/4884
• fix: LEAN_EXPORT in sharecommon by @Kha in https://github.com/leanprover/lean4/pull/4893
• chore: revert "fix: make import resolution case-sensitive on all platforms" by @Kha in https://github.com/leanprover/lean4/pull/4896
• doc: add docstring to IO.FS.realpath by @alok in https://github.com/leanprover/lean4/pull/4648
• feat: getLsb_replicate by @bollu in https://github.com/leanprover/lean4/pull/4873
• chore: deprecate Nix-based build, remove interactive components by @Kha in https://github.com/leanprover/lean4/pull/4895
• feat: accept user-defined options on the cmdline by @Kha in https://github.com/leanprover/lean4/pull/4741
• perf: fix implementation of move constructors and move assignment ope… by @legrosbuffle in https://github.com/leanprover/lean4/pull/4700
• perf: avoid expr copies in replace_rec_fn::apply by @legrosbuffle in https://github.com/leanprover/lean4/pull/4702
• perf: use NatPow Int instead of HPow Int Nat Int by @leodemoura in https://github.com/leanprover/lean4/pull/4903

New Contributors

• @grunweg made their first contribution in https://github.com/leanprover/lean4/pull/4719
• @eltociear made their first contribution in https://github.com/leanprover/lean4/pull/4853
• @legrosbuffle made their first contribution in https://github.com/leanprover/lean4/pull/4700

Full Changelog: https://github.com/leanprover/lean4/compare/v4.10.0...v4.11.0-rc1