From e20ee29b39847bb782e6ef1c990597da8d86354b Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 17 Nov 2023 10:48:15 -0500 Subject: [PATCH] experiment with examples --- DuperOnMathlib/DuperOnMathlib/CSB.lean | 91 +++++++++++++++++++ .../DuperOnMathlib/PrimesModFour.lean | 78 +++++++--------- 2 files changed, 124 insertions(+), 45 deletions(-) diff --git a/DuperOnMathlib/DuperOnMathlib/CSB.lean b/DuperOnMathlib/DuperOnMathlib/CSB.lean index b65e62f..f5b180f 100644 --- a/DuperOnMathlib/DuperOnMathlib/CSB.lean +++ b/DuperOnMathlib/DuperOnMathlib/CSB.lean @@ -3,6 +3,9 @@ import Mathlib.Data.Set.Lattice import Mathlib.Data.Set.Function import Mathlib.Tactic.Set import Mathlib.Tactic.WLOG +import DuperOnMathlib.DuperInterface + +set_option reduceInstances false open Set open Function @@ -13,6 +16,92 @@ From *Mathematics in Lean*. noncomputable section open Classical + +section +variable {α β : Type*} [Nonempty β] +variable (f : α → β) (g : β → α) + +def sbAux : ℕ → Set α + | 0 => univ \ g '' univ + | n + 1 => g '' (f '' sbAux n) + +def sbSet := + ⋃ n, sbAux f g n + +def sbFun (x : α) : β := + if x ∈ sbSet f g then f x else invFun g x + +theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by + have : x ∈ g '' univ := by + duper [sbAux, hx, sbSet, mem_iUnion, mem_diff, mem_univ, hx] + have : ∃ y, g y = x := by + duper [image_univ, mem_range, this] + duper [invFun_eq, this] + +-- Nice try: +-- theorem sb_right_inv' {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by +-- have : x ∈ g '' univ := by +-- duper [sbAux, hx, sbSet, mem_iUnion, mem_diff, mem_univ, hx] +-- duper [invFun_eq, image_univ, mem_range, this] + +theorem sb_injective (hf : Injective f) : Injective (sbFun f g) := by + set A := sbSet f g with A_def + set h := sbFun f g with h_def + intro x₁ x₂ + intro (hxeq : h x₁ = h x₂) + show x₁ = x₂ + simp only [h_def, sbFun, ← A_def] at hxeq + by_cases xA : x₁ ∈ A ∨ x₂ ∈ A + · wlog x₁A : x₁ ∈ A generalizing x₁ x₂ hxeq xA + · symm + apply this hxeq.symm xA.symm (xA.resolve_left x₁A) + have x₂A : x₂ ∈ A := by + apply not_imp_self.mp + intro (x₂nA : x₂ ∉ A) + rw [if_pos x₁A, if_neg x₂nA] at hxeq + rw [A_def, sbSet, mem_iUnion] at x₁A + have x₂eq : x₂ = g (f x₁) := by + rw [hxeq, sb_right_inv f g x₂nA] + rcases x₁A with ⟨n, hn⟩ + rw [A_def, sbSet, mem_iUnion] + use n + 1 + simp [sbAux] + exact ⟨x₁, hn, x₂eq.symm⟩ + rw [if_pos x₁A, if_pos x₂A] at hxeq + exact hf hxeq + push_neg at xA + rw [if_neg xA.1, if_neg xA.2] at hxeq + rw [← sb_right_inv f g xA.1, hxeq, sb_right_inv f g xA.2] + +theorem sb_surjective (hg : Injective g) : Surjective (sbFun f g) := by + set A := sbSet f g with A_def + set h := sbFun f g with h_def + intro y + by_cases gyA : g y ∈ A + · rw [A_def, sbSet, mem_iUnion] at gyA + rcases gyA with ⟨n, hn⟩ + rcases n with _ | n + · simp [sbAux] at hn + simp [sbAux] at hn + rcases hn with ⟨x, xmem, hx⟩ + use x + have : x ∈ A := by + rw [A_def, sbSet, mem_iUnion] + exact ⟨n, xmem⟩ + simp only [h_def, sbFun, if_pos this] + exact hg hx + use g y + simp only [h_def, sbFun, if_neg gyA] + apply leftInverse_invFun hg + +theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) : + ∃ h : α → β, Bijective h := + ⟨sbFun f g, sb_injective f g hf, sb_surjective f g hg⟩ + +end + +namespace original + variable {α β : Type*} [Nonempty β] variable (f : α → β) (g : β → α) @@ -91,3 +180,5 @@ theorem sb_surjective (hg : Injective g) : Surjective (sbFun f g) := by theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) : ∃ h : α → β, Bijective h := ⟨sbFun f g, sb_injective f g hf, sb_surjective f g hg⟩ + +end original diff --git a/DuperOnMathlib/DuperOnMathlib/PrimesModFour.lean b/DuperOnMathlib/DuperOnMathlib/PrimesModFour.lean index e5c0b1a..88e5694 100644 --- a/DuperOnMathlib/DuperOnMathlib/PrimesModFour.lean +++ b/DuperOnMathlib/DuperOnMathlib/PrimesModFour.lean @@ -6,22 +6,17 @@ import Mathlib.Tactic import Mathlib.Tactic.IntervalCases import DuperOnMathlib.DuperInterface +set_option reduceInstances false lemma composite_of_not_prime {n : ℕ} (h : 2 ≤ n) (hnp : ¬ n.Prime) : ∃ m k, n = m * k ∧ 1 < m ∧ 1 < k ∧ m < n ∧ k < n := by rw [Nat.prime_def_lt] at hnp have : ∃ m, m ∣ n ∧ m < n ∧ m ≠ 1 := by - simpa [h] using hnp + duper [h, hnp] rcases this with ⟨m, mdvd, mlt, mne⟩ have neq : n = m * (n / m) := by symm; rwa [Nat.mul_div_eq_iff_dvd] use m, n / m, neq - have mge1 : 1 < m := by - have : 1 ≤ m ↔ 0 < m := Iff.refl _ - - -- nice try... - -- duper [lt_of_le_of_ne, Ne.symm, Nat.pos_of_ne_zero, mdvd, -- zero_dvd_iff, ne_of_lt, ne_eq, this, mlt, mne] - - -- a fully manual proof + have mgt1 : 1 < m := by -- apply lt_of_le_of_ne _ (Ne.symm mne) -- rw [ne_eq] at mne -- apply Nat.pos_of_ne_zero @@ -29,32 +24,25 @@ lemma composite_of_not_prime {n : ℕ} (h : 2 ≤ n) (hnp : ¬ n.Prime) : -- have := ne_of_lt mlt -- simp only [zero_dvd_iff] at mdvd -- simp only [mdvd] at this - - apply lt_of_le_of_ne _ (Ne.symm mne) - rw [ne_eq] at mne - apply Nat.pos_of_ne_zero - rintro rfl - have := ne_of_lt mlt - -- this doesn't work: - -- duper [zero_dvd_iff, mdvd, this] - -- but this does: - duper [zero_dvd_iff.mp mdvd, this] - use mge1 - have ndivmge1 : 1 < n / m := by - -- this doesn't work - -- duper [lt_of_mul_lt_mul_left, Nat.zero_le m, mul_one, neq, mlt] - apply lt_of_mul_lt_mul_left _ (Nat.zero_le m) - -- rw [mul_one, ←neq]; exact mlt - -- this doesn't work: + have : 1 ≤ m ↔ 0 < m := Iff.refl _ + duper [zero_dvd_iff, mdvd, ne_of_lt, mlt, Nat.pos_of_ne_zero, ne_eq, this, lt_of_le_of_ne, mne] + use mgt1 + have ndivmgt1 : 1 < n / m := by + duper [lt_of_mul_lt_mul_left, Nat.zero_le, mul_one, neq, mlt] + -- this also works: + -- apply lt_of_mul_lt_mul_left _ (Nat.zero_le m) -- duper [mul_one, neq, mlt] - -- but this does: - duper [mul_one m, neq, mlt] - use ndivmge1 + -- but this fails: + -- apply lt_of_mul_lt_mul_left _ (Nat.zero_le m) + -- duper [mul_one, neq, mlt, lt_of_mul_lt_mul_left] + use ndivmgt1 constructor - . rw [←mul_one m, neq] - exact Nat.mul_lt_mul_of_pos_left ndivmge1 (zero_lt_one.trans mge1) + . have : 0 < m := zero_lt_one.trans mgt1 + duper [mul_one, neq, Nat.mul_lt_mul_of_pos_left, ndivmgt1, this] + -- also works: + -- duper [mul_one, neq, Nat.mul_lt_mul_of_pos_left, ndivmgt1, zero_lt_one, lt_trans, gt_iff_lt, mgt1] have : 1 * (n / m) < m * (n / m) := by - apply Nat.mul_lt_mul_of_pos_right mge1 (zero_lt_one.trans ndivmge1) + duper [Nat.mul_lt_mul_of_pos_right, mgt1, zero_lt_one.trans ndivmgt1] rwa [one_mul, ←neq] at this lemma composite_of_not_prime_alt (n : ℕ) (h : 2 ≤ n) (hnp : ¬ n.Prime) : @@ -64,17 +52,17 @@ lemma composite_of_not_prime_alt (n : ℕ) (h : 2 ≤ n) (hnp : ¬ n.Prime) : intros m k neq mne1 have : m ≠ 0 := by contrapose! nne0 - simp [neq, nne0] - have mge1 : 1 < m := by + simp only [neq, nne0, zero_mul] + have mgt1 : 1 < m := by apply lt_of_le_of_ne _ (Ne.symm mne1) rwa [Nat.succ_le_iff, Nat.pos_iff_ne_zero] - use mge1 + use mgt1 have : 0 < k := by rw [Nat.pos_iff_ne_zero] contrapose! nne0 simp [neq, nne0] rw [←one_mul k, neq] - apply Nat.mul_lt_mul_of_pos_right mge1 this + apply Nat.mul_lt_mul_of_pos_right mgt1 this have nne1 : n ≠ 1 := by linarith have : ∃ m, m ≠ 1 ∧ ∃ k, n = m * k ∧ k ≠ 1 := by simpa [←Nat.irreducible_iff_nat_prime, irreducible_iff, nne1, not_or] using hnp @@ -152,21 +140,21 @@ lemma composite_of_not_prime {n : ℕ} (h : 2 ≤ n) (hnp : ¬ n.Prime) : rcases this with ⟨m, mdvd, mlt, mne⟩ have neq : n = m * (n / m) := by symm; rwa [Nat.mul_div_eq_iff_dvd] use m, n / m, neq - have mge1 : 1 < m := by + have mgt1 : 1 < m := by apply lt_of_le_of_ne _ (Ne.symm mne) apply Nat.pos_of_ne_zero rintro rfl simp at mdvd; linarith - use mge1 - have ndivmge1 : 1 < n / m := by + use mgt1 + have ndivmgt1 : 1 < n / m := by apply lt_of_mul_lt_mul_left _ (Nat.zero_le m) rwa [mul_one, ←neq] - use ndivmge1 + use ndivmgt1 constructor . rw [←mul_one m, neq] - exact Nat.mul_lt_mul_of_pos_left ndivmge1 (zero_lt_one.trans mge1) + exact Nat.mul_lt_mul_of_pos_left ndivmgt1 (zero_lt_one.trans mgt1) have : 1 * (n / m) < m * (n / m) := by - apply Nat.mul_lt_mul_of_pos_right mge1 (zero_lt_one.trans ndivmge1) + apply Nat.mul_lt_mul_of_pos_right mgt1 (zero_lt_one.trans ndivmgt1) rwa [one_mul, ←neq] at this lemma composite_of_not_prime_alt (n : ℕ) (h : 2 ≤ n) (hnp : ¬ n.Prime) : @@ -177,16 +165,16 @@ lemma composite_of_not_prime_alt (n : ℕ) (h : 2 ≤ n) (hnp : ¬ n.Prime) : have : m ≠ 0 := by contrapose! nne0 simp [neq, nne0] - have mge1 : 1 < m := by + have mgt1 : 1 < m := by apply lt_of_le_of_ne _ (Ne.symm mne1) rwa [Nat.succ_le_iff, Nat.pos_iff_ne_zero] - use mge1 + use mgt1 have : 0 < k := by rw [Nat.pos_iff_ne_zero] contrapose! nne0 simp [neq, nne0] rw [←one_mul k, neq] - apply Nat.mul_lt_mul_of_pos_right mge1 this + apply Nat.mul_lt_mul_of_pos_right mgt1 this have nne1 : n ≠ 1 := by linarith have : ∃ m, m ≠ 1 ∧ ∃ k, n = m * k ∧ k ≠ 1 := by simpa [←Nat.irreducible_iff_nat_prime, irreducible_iff, nne1, not_or] using hnp @@ -253,4 +241,4 @@ theorem infinite_primes_three_mod_four : ∀ s : Finset ℕ, have : 2 ≤ p := primep.two_le linarith -end +end original