experiment with examples

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

DuperOnMathlib/DuperOnMathlib/PrimesModFour.lean

@@ -6,55 +6,43 @@ 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
     -- rintro rfl
     -- 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