Trigger CI for leanprover-community/batteries#1028

.docker/gitpod-blueprint/Dockerfile

@@ -0,0 +1,47 @@
+# This is the Dockerfile for `leanprovercommunity/gitpod4-blueprint`.
+# As well as elan, we also install leanblueprint and all of its dependencies.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
+
+FROM ubuntu:jammy
+
+USER root
+
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev python3 python3-pip python3-requests -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
+RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
+
+# install leanblueprint
+RUN python3 -m pip install leanblueprint invoke
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.docker/gitpod/Dockerfile

@@ -1,12 +1,15 @@
-# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+# This is the Dockerfile for `leanprovercommunity/gitpod4`.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
 
-# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
-# so we just install everything in one go
 FROM ubuntu:jammy
 
 USER root
 
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests -y && apt-get clean
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-pip python3-requests -y && apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
     # passwordless sudo for users in the 'sudo' group

.docker/lean/Dockerfile

@@ -0,0 +1,36 @@
+# This is the Dockerfile for `leanprovercommunity/lean4`.
+# It is based on the generic `debian` image, and installs `elan` and the current stable version of `lean`.
+
+# This container does not come with a pre-installed version of mathlib;
+# you should call `lake exe cache get` which will download the most recent version.
+# The only difference between this Dockerfile and leanprovercommunity/lean4 is that this image
+# bypasses a warning that could occur when trying to connect to github for the first time.
+
+# NOTE: to run this docker image on macos or windows,
+# you will need to increase the allowed memory (in the docker GUI) beyond 2GB
+
+FROM debian
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/bash", "-l"]
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan default stable
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

Mathlib.lean

@@ -2427,6 +2427,7 @@ import Mathlib.Data.LazyList.Basic
 import Mathlib.Data.List.AList
 import Mathlib.Data.List.Basic
 import Mathlib.Data.List.Chain
+import Mathlib.Data.List.ChainOfFn
 import Mathlib.Data.List.Count
 import Mathlib.Data.List.Cycle
 import Mathlib.Data.List.Dedup

Mathlib/Algebra/Algebra/Equiv.lean

@@ -740,6 +740,10 @@ def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] :
   right_inv := fun _ ↦ rfl
   map_mul' := fun _ _ ↦ rfl
 
+/-- See also `Finite.algHom` -/
+instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂) :=
+  Finite.of_injective _ AlgEquiv.coe_algHom_injective
+
 end Semiring
 
 section CommSemiring

Mathlib/Data/Ineq.lean

@@ -9,8 +9,8 @@ import Mathlib.Lean.Expr.Basic
 # `Ineq` datatype
 
 This file contains an enum `Ineq` (whose constructors are `eq`, `le`, `lt`), and operations
-involving it. The type `Ineq` is one of the fundamental objects manipulated by the `linarith` tactic
-(and, in future, also the `linear_combination` tactic).
+involving it. The type `Ineq` is one of the fundamental objects manipulated by the `linarith` and
+`linear_combination` tactics.
 -/
 
 open Lean Elab Tactic Meta

Mathlib/Data/List/ChainOfFn.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Myers
+-/
+import Mathlib.Data.List.Chain
+import Mathlib.Data.List.OfFn
+
+/-!
+# Lemmas about `Chain'` and `OfFn`
+
+This file provides lemmas involving both `List.Chain'` and `List.OfFn`.
+-/
+
+open Nat
+
+namespace List
+
+lemma chain'_ofFn {α : Type*} {n : ℕ} {f : Fin n → α} {r : α → α → Prop} :
+    (ofFn f).Chain' r ↔ ∀ (i) (hi : i + 1 < n), r (f ⟨i, lt_of_succ_lt hi⟩) (f ⟨i + 1, hi⟩) := by
+  simp_rw [chain'_iff_get, get_ofFn, length_ofFn]
+  exact ⟨fun h i hi ↦ h i (by omega), fun h i hi ↦ h i (by omega)⟩
+
+end List

Mathlib/Data/List/OfFn.lean

@@ -83,15 +83,6 @@ theorem ofFn_succ' {n} (f : Fin (succ n) → α) :
 theorem ofFn_eq_nil_iff {n : ℕ} {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]
 
-theorem last_ofFn {n : ℕ} (f : Fin n → α) (h : ofFn f ≠ [])
-    (hn : n - 1 < n := Nat.pred_lt <| ofFn_eq_nil_iff.not.mp h) :
-    getLast (ofFn f) h = f ⟨n - 1, hn⟩ := by simp [getLast_eq_getElem]
-
-theorem last_ofFn_succ {n : ℕ} (f : Fin n.succ → α)
-    (h : ofFn f ≠ [] := mt ofFn_eq_nil_iff.mp (Nat.succ_ne_zero _)) :
-    getLast (ofFn f) h = f (Fin.last _) :=
-  last_ofFn f h
-
 /-- Note this matches the convention of `List.ofFn_succ'`, putting the `Fin m` elements first. -/
 theorem ofFn_add {m n} (f : Fin (m + n) → α) :
     List.ofFn f =
@@ -181,6 +172,73 @@ theorem pairwise_ofFn {R : α → α → Prop} {n} {f : Fin n → α} :
     (Fin.rightInverse_cast (length_ofFn f)).surjective.forall, Fin.forall_iff, Fin.cast_mk,
     Fin.mk_lt_mk, forall_comm (α := (_ : Prop)) (β := ℕ)]
 
+lemma head_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) :
+    (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
+  rw [← getElem_zero (length_ofFn _ ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),
+    List.getElem_ofFn]
+
+lemma getLast_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) :
+    (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩ := by
+  simp [getLast_eq_getElem]
+
+lemma getLast_ofFn_succ {n : ℕ} (f : Fin n.succ → α) :
+    (ofFn f).getLast (mt ofFn_eq_nil_iff.1 (Nat.succ_ne_zero _)) = f (Fin.last _) :=
+  getLast_ofFn f _
+
+@[deprecated getLast_ofFn (since := "2024-11-06")]
+theorem last_ofFn {n : ℕ} (f : Fin n → α) (h : ofFn f ≠ [])
+    (hn : n - 1 < n := Nat.pred_lt <| ofFn_eq_nil_iff.not.mp h) :
+    getLast (ofFn f) h = f ⟨n - 1, hn⟩ := by simp [getLast_eq_getElem]
+
+@[deprecated getLast_ofFn_succ (since := "2024-11-06")]
+theorem last_ofFn_succ {n : ℕ} (f : Fin n.succ → α)
+    (h : ofFn f ≠ [] := mt ofFn_eq_nil_iff.mp (Nat.succ_ne_zero _)) :
+    getLast (ofFn f) h = f (Fin.last _) :=
+  getLast_ofFn_succ _
+
+lemma ofFn_cons {n} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f) = a :: ofFn f := by
+  rw [ofFn_succ]
+  rfl
+
+-- Temporary local copy of result from Lean commit 1e98fd7f2d965ab035dbf1099fb4a4ffde16b151.
+theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
+    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
+  rw [find?_eq_some]
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ⟨bs, rfl⟩, h⟩
+    refine ⟨as.length, ⟨?_, ?_, ?_⟩⟩
+    · simp only [length_append, length_cons]
+      refine Nat.lt_add_of_pos_right (zero_lt_succ bs.length)
+    · rw [getElem_append_right (Nat.le_refl as.length)]
+      simp
+    · intro j h'
+      rw [getElem_append_left h']
+      exact h _ (getElem_mem h')
+  · rintro ⟨i, h, rfl, h'⟩
+    refine ⟨xs.take i, ⟨xs.drop (i+1), ?_⟩, ?_⟩
+    · rw [getElem_cons_drop, take_append_drop]
+    · intro a m
+      rw [mem_take_iff_getElem] at m
+      obtain ⟨j, h, rfl⟩ := m
+      apply h'
+      omega
+
+lemma find?_ofFn_eq_some {n} {f : Fin n → α} {p : α → Bool} {b : α} :
+    (ofFn f).find? p = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬(p (f j) = true) := by
+  rw [find?_eq_some_iff_getElem]
+  exact ⟨fun ⟨hpb, i, hi, hfb, h⟩ ↦
+      ⟨hpb, ⟨⟨i, (length_ofFn f) ▸ hi⟩, by simpa using hfb, fun j hj ↦ by simpa using h j hj⟩⟩,
+    fun ⟨hpb, i, hfb, h⟩ ↦
+      ⟨hpb, ⟨i, (length_ofFn f).symm ▸ i.isLt, by simpa using hfb,
+        fun j hj ↦ by simpa using h ⟨j, by omega⟩ (by simpa using hj)⟩⟩⟩
+
+lemma find?_ofFn_eq_some_of_injective {n} {f : Fin n → α} {p : α → Bool} {i : Fin n}
+    (h : Function.Injective f) :
+    (ofFn f).find? p = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬(p (f j) = true) := by
+  simp only [find?_ofFn_eq_some, h.eq_iff, Bool.not_eq_true, exists_eq_left]
+
 /-- Lists are equivalent to the sigma type of tuples of a given length. -/
 @[simps]
 def equivSigmaTuple : List α ≃ Σn, Fin n → α where

Mathlib/Order/Basic.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Mario Carneiro
 import Mathlib.Data.Subtype
 import Mathlib.Order.Defs
 import Mathlib.Order.Notation
+import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.Spread
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Inhabit
@@ -1066,10 +1067,14 @@ theorem mk_lt_mk [LT α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
 theorem coe_le_coe [LE α] {p : α → Prop} {x y : Subtype p} : (x : α) ≤ y ↔ x ≤ y :=
   Iff.rfl
 
+@[gcongr] alias ⟨_, GCongr.coe_le_coe⟩ := coe_le_coe
+
 @[simp, norm_cast]
 theorem coe_lt_coe [LT α] {p : α → Prop} {x y : Subtype p} : (x : α) < y ↔ x < y :=
   Iff.rfl
 
+@[gcongr] alias ⟨_, GCongr.coe_lt_coe⟩ := coe_lt_coe
+
 instance preorder [Preorder α] (p : α → Prop) : Preorder (Subtype p) :=
   Preorder.lift (fun (a : Subtype p) ↦ (a : α))