From 84b27843bf537a040555d75127a5df27b4a767d8 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 24 Sep 2024 23:51:37 +0000 Subject: [PATCH] chore: adaptations for nightly-2024-09-24 (#17094) Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: Kim Morrison --- Mathlib/Algebra/AddTorsor.lean | 1 - Mathlib/Logic/Nonempty.lean | 7 ------- .../Topology/UniformSpace/UniformConvergenceTopology.lean | 4 ++-- lake-manifest.json | 2 +- lean-toolchain | 2 +- 5 files changed, 4 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/AddTorsor.lean b/Mathlib/Algebra/AddTorsor.lean index f9baa6191726f..32963195471d0 100644 --- a/Mathlib/Algebra/AddTorsor.lean +++ b/Mathlib/Algebra/AddTorsor.lean @@ -248,7 +248,6 @@ instance instAddTorsor : AddTorsor (G × G') (P × P') where zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _) add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _) vsub p₁ p₂ := (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2) - nonempty := Prod.instNonempty vsub_vadd' _ _ := Prod.ext (vsub_vadd _ _) (vsub_vadd _ _) vadd_vsub' _ _ := Prod.ext (vadd_vsub _ _) (vadd_vsub _ _) diff --git a/Mathlib/Logic/Nonempty.lean b/Mathlib/Logic/Nonempty.lean index 1a52ca02ab2d4..1c8198b9475d3 100644 --- a/Mathlib/Logic/Nonempty.lean +++ b/Mathlib/Logic/Nonempty.lean @@ -99,13 +99,6 @@ theorem Nonempty.elim_to_inhabited {α : Sort*} [h : Nonempty α] {p : Prop} (f p := h.elim <| f ∘ Inhabited.mk -protected instance Prod.instNonempty {α β} [h : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) := - h.elim fun g ↦ h2.elim fun g2 ↦ ⟨⟨g, g2⟩⟩ - -protected instance Pi.instNonempty {ι : Sort*} {α : ι → Sort*} [∀ i, Nonempty (α i)] : - Nonempty (∀ i, α i) := - ⟨fun _ ↦ Classical.arbitrary _⟩ - theorem Classical.nonempty_pi {ι} {α : ι → Sort*} : Nonempty (∀ i, α i) ↔ ∀ i, Nonempty (α i) := ⟨fun ⟨f⟩ a ↦ ⟨f a⟩, @Pi.instNonempty _ _⟩ diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index 4eae4a2c7b4eb..f828a823ee8cd 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean @@ -157,9 +157,9 @@ open UniformConvergence variable {α β : Type*} {𝔖 : Set (Set α)} -instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty +instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty _ -instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty +instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty _ instance [Subsingleton β] : Subsingleton (α →ᵤ β) := inferInstanceAs <| Subsingleton <| α → β diff --git a/lake-manifest.json b/lake-manifest.json index ac14cbf86e7d7..ed832574476f2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6823ca35a23905867f0c6d9678932e6f261157e4", + "rev": "c37494a698d68c5e3711575fcb90ebf2974900ff", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lean-toolchain b/lean-toolchain index a5551df349f89..98d327efee081 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-09-23 +leanprover/lean4:nightly-2024-09-24