feat(algebra/order/archimedean): upgrade some ∃ to ∃! (#10343)

src/algebra/order/archimedean.lean

@@ -28,7 +28,7 @@ number `n` such that `x ≤ n • y`.
 * `ℕ`, `ℤ`, and `ℚ` are archimedean.
 -/
 
-open int
+open int set
 
 variables {α : Type*}
 
@@ -47,8 +47,8 @@ variables [linear_ordered_add_comm_group α] [archimedean α]
 
 /-- An archimedean decidable linearly ordered `add_comm_group` has a version of the floor: for
 `a > 0`, any `g` in the group lies between some two consecutive multiples of `a`. -/
-lemma exists_int_smul_near_of_pos {a : α} (ha : 0 < a) (g : α) :
-  ∃ (k : ℤ), k • a ≤ g ∧ g < (k + 1) • a :=
+lemma exists_unique_zsmul_near_of_pos {a : α} (ha : 0 < a) (g : α) :
+  ∃! k : ℤ, k • a ≤ g ∧ g < (k + 1) • a :=
 begin
   let s : set ℤ := {n : ℤ | n • a ≤ g},
   obtain ⟨k, hk : -g ≤ k • a⟩ := archimedean.arch (-g) ha,
@@ -60,35 +60,30 @@ begin
     rw ← coe_nat_zsmul at hk,
     exact le_trans hn hk },
   obtain ⟨m, hm, hm'⟩ := int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne,
-  refine ⟨m, hm, _⟩,
-  by_contra H,
-  linarith [hm' _ $ not_lt.mp H]
+  have hm'' : g < (m + 1) • a,
+  { contrapose! hm', exact ⟨m + 1, hm', lt_add_one _⟩, },
+  refine ⟨m, ⟨hm, hm''⟩, λ n hn, (hm' n hn.1).antisymm $ int.le_of_lt_add_one _⟩,
+  rw ← zsmul_lt_zsmul_iff ha,
+  exact lt_of_le_of_lt hm hn.2
 end
 
-lemma exists_int_smul_near_of_pos' {a : α} (ha : 0 < a) (g : α) :
-  ∃ (k : ℤ), 0 ≤ g - k • a ∧ g - k • a < a :=
-begin
-  obtain ⟨k, h1, h2⟩ := exists_int_smul_near_of_pos ha g,
-  refine ⟨k, sub_nonneg.mpr h1, _⟩,
-  simpa only [sub_lt_iff_lt_add', add_zsmul, one_zsmul] using h2
-end
-
-lemma exists_add_int_smul_mem_Ico {a : α} (ha : 0 < a) (b c : α) :
-  ∃ m : ℤ, b + m • a ∈ set.Ico c (c + a) :=
-begin
-  rcases exists_int_smul_near_of_pos' ha (b - c) with ⟨m, hle, hlt⟩,
-  refine ⟨-m, _, _⟩,
-  { rwa [neg_zsmul, ← sub_eq_add_neg, le_sub, ← sub_nonneg] },
-  { rwa [sub_right_comm, sub_lt_iff_lt_add', sub_eq_add_neg, ← neg_zsmul] at hlt }
-end
-
-lemma exists_add_int_smul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
-  ∃ m : ℤ, b + m • a ∈ set.Ioc c (c + a) :=
-begin
-  rcases exists_int_smul_near_of_pos ha (c - b) with ⟨m, hle, hlt⟩,
-  refine ⟨m + 1, sub_lt_iff_lt_add'.1 hlt, _⟩,
-  rwa [add_zsmul, one_zsmul, ← add_assoc, add_le_add_iff_right, ← le_sub_iff_add_le']
-end
+lemma exists_unique_zsmul_near_of_pos' {a : α} (ha : 0 < a) (g : α) :
+  ∃! k : ℤ, 0 ≤ g - k • a ∧ g - k • a < a :=
+by simpa only [sub_nonneg, add_zsmul, one_zsmul, sub_lt_iff_lt_add']
+  using exists_unique_zsmul_near_of_pos ha g
+
+lemma exists_unique_add_zsmul_mem_Ico {a : α} (ha : 0 < a) (b c : α) :
+  ∃! m : ℤ, b + m • a ∈ set.Ico c (c + a) :=
+(equiv.neg ℤ).bijective.exists_unique_iff.2 $
+  by simpa only [equiv.neg_apply, mem_Ico, neg_zsmul, ← sub_eq_add_neg, le_sub_iff_add_le, zero_add,
+    add_comm c, sub_lt_iff_lt_add', add_assoc] using exists_unique_zsmul_near_of_pos' ha (b - c)
+
+lemma exists_unique_add_zsmul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
+  ∃! m : ℤ, b + m • a ∈ set.Ioc c (c + a) :=
+(equiv.add_right (1 : ℤ)).bijective.exists_unique_iff.2 $
+  by simpa only [add_zsmul, sub_lt_iff_lt_add', le_sub_iff_add_le', ← add_assoc, and.comm, mem_Ioc,
+    equiv.coe_add_right, one_zsmul, add_le_add_iff_right]
+    using exists_unique_zsmul_near_of_pos ha (c - b)
 
 end linear_ordered_add_comm_group
 

src/algebra/periodic.lean

@@ -252,23 +252,23 @@ lemma periodic.int_mul_eq [ring α]
 lemma periodic.exists_mem_Ico₀ [linear_ordered_add_comm_group α] [archimedean α]
   (h : periodic f c) (hc : 0 < c) (x) :
   ∃ y ∈ set.Ico 0 c, f x = f y :=
-let ⟨n, H⟩ := exists_int_smul_near_of_pos' hc x in
+let ⟨n, H, _⟩ := exists_unique_zsmul_near_of_pos' hc x in
 ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩
 
 /-- If a function `f` is `periodic` with positive period `c`, then for all `x` there exists some
   `y ∈ Ico a (a + c)` such that `f x = f y`. -/
 lemma periodic.exists_mem_Ico [linear_ordered_add_comm_group α] [archimedean α]
   (h : periodic f c) (hc : 0 < c) (x a) :
   ∃ y ∈ set.Ico a (a + c), f x = f y :=
-let ⟨n, H⟩ := exists_add_int_smul_mem_Ico hc x a in
+let ⟨n, H, _⟩ := exists_unique_add_zsmul_mem_Ico hc x a in
 ⟨x + n • c, H, (h.zsmul n x).symm⟩
 
 /-- If a function `f` is `periodic` with positive period `c`, then for all `x` there exists some
   `y ∈ Ioc a (a + c)` such that `f x = f y`. -/
 lemma periodic.exists_mem_Ioc [linear_ordered_add_comm_group α] [archimedean α]
   (h : periodic f c) (hc : 0 < c) (x a) :
   ∃ y ∈ set.Ioc a (a + c), f x = f y :=
-let ⟨n, H⟩ := exists_add_int_smul_mem_Ioc hc x a in
+let ⟨n, H, _⟩ := exists_unique_add_zsmul_mem_Ioc hc x a in
 ⟨x + n • c, H, (h.zsmul n x).symm⟩
 
 lemma periodic_with_period_zero [add_zero_class α]

src/group_theory/archimedean.lean

@@ -40,8 +40,8 @@ begin
   obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha,
   refine le_antisymm _ (H.closure_le.mpr $ by simp [a_in]),
   intros g g_in,
-  obtain ⟨k, nonneg, lt⟩ : ∃ k, 0 ≤ g - k • a ∧ g - k • a < a :=
-    exists_int_smul_near_of_pos' a_pos g,
+  obtain ⟨k, ⟨nonneg, lt⟩, _⟩ : ∃! k, 0 ≤ g - k • a ∧ g - k • a < a :=
+    exists_unique_zsmul_near_of_pos' a_pos g,
   have h_zero : g - k • a = 0,
   { by_contra h,
     have h : a ≤ g - k • a,

src/logic/function/basic.lean

@@ -125,27 +125,27 @@ instance decidable_eq_pfun (p : Prop) [decidable p] (α : p → Type*)
   [Π hp, decidable_eq (α hp)] : decidable_eq (Π hp, α hp)
 | f g := decidable_of_iff (∀ hp, f hp = g hp) funext_iff.symm
 
-theorem surjective.forall {f : α → β} (hf : surjective f) {p : β → Prop} :
+protected theorem surjective.forall {f : α → β} (hf : surjective f) {p : β → Prop} :
   (∀ y, p y) ↔ ∀ x, p (f x) :=
 ⟨λ h x, h (f x), λ h y, let ⟨x, hx⟩ := hf y in hx ▸ h x⟩
 
-theorem surjective.forall₂ {f : α → β} (hf : surjective f) {p : β → β → Prop} :
+protected theorem surjective.forall₂ {f : α → β} (hf : surjective f) {p : β → β → Prop} :
   (∀ y₁ y₂, p y₁ y₂) ↔ ∀ x₁ x₂, p (f x₁) (f x₂) :=
 hf.forall.trans $ forall_congr $ λ x, hf.forall
 
-theorem surjective.forall₃ {f : α → β} (hf : surjective f) {p : β → β → β → Prop} :
+protected theorem surjective.forall₃ {f : α → β} (hf : surjective f) {p : β → β → β → Prop} :
   (∀ y₁ y₂ y₃, p y₁ y₂ y₃) ↔ ∀ x₁ x₂ x₃, p (f x₁) (f x₂) (f x₃) :=
 hf.forall.trans $ forall_congr $ λ x, hf.forall₂
 
-theorem surjective.exists {f : α → β} (hf : surjective f) {p : β → Prop} :
+protected theorem surjective.exists {f : α → β} (hf : surjective f) {p : β → Prop} :
   (∃ y, p y) ↔ ∃ x, p (f x) :=
 ⟨λ ⟨y, hy⟩, let ⟨x, hx⟩ := hf y in ⟨x, hx.symm ▸ hy⟩, λ ⟨x, hx⟩, ⟨f x, hx⟩⟩
 
-theorem surjective.exists₂ {f : α → β} (hf : surjective f) {p : β → β → Prop} :
+protected theorem surjective.exists₂ {f : α → β} (hf : surjective f) {p : β → β → Prop} :
   (∃ y₁ y₂, p y₁ y₂) ↔ ∃ x₁ x₂, p (f x₁) (f x₂) :=
 hf.exists.trans $ exists_congr $ λ x, hf.exists
 
-theorem surjective.exists₃ {f : α → β} (hf : surjective f) {p : β → β → β → Prop} :
+protected theorem surjective.exists₃ {f : α → β} (hf : surjective f) {p : β → β → β → Prop} :
   (∃ y₁ y₂ y₃, p y₁ y₂ y₃) ↔ ∃ x₁ x₂ x₃, p (f x₁) (f x₂) (f x₃) :=
 hf.exists.trans $ exists_congr $ λ x, hf.exists₂
 
@@ -157,9 +157,17 @@ lemma bijective_iff_exists_unique (f : α → β) : bijective f ↔
     λ b, exists_of_exists_unique (he b) ⟩⟩
 
 /-- Shorthand for using projection notation with `function.bijective_iff_exists_unique`. -/
-lemma bijective.exists_unique {f : α → β} (hf : bijective f) (b : β) : ∃! (a : α), f a = b :=
+protected lemma bijective.exists_unique {f : α → β} (hf : bijective f) (b : β) :
+  ∃! (a : α), f a = b :=
 (bijective_iff_exists_unique f).mp hf b
 
+lemma bijective.exists_unique_iff {f : α → β} (hf : bijective f) {p : β → Prop} :
+  (∃! y, p y) ↔ ∃! x, p (f x) :=
+⟨λ ⟨y, hpy, hy⟩, let ⟨x, hx⟩ := hf.surjective y in ⟨x, by rwa hx,
+  λ z (hz : p (f z)), hf.injective $ hx.symm ▸ hy _ hz⟩,
+  λ ⟨x, hpx, hx⟩, ⟨f x, hpx, λ y hy,
+    let ⟨z, hz⟩ := hf.surjective y in hz ▸ congr_arg f $ hx _ $ by rwa hz⟩⟩
+
 lemma bijective.of_comp_iff (f : α → β) {g : γ → α} (hg : bijective g) :
   bijective (f ∘ g) ↔ bijective f :=
 and_congr (injective.of_comp_iff' _ hg) (surjective.of_comp_iff _ hg.surjective)