add some test data

DuperOnMathlib/DuperOnMathlib/CSB.lean

@@ -0,0 +1,93 @@
+import Mathlib.Data.Nat.Basic
+import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Function
+import Mathlib.Tactic.Set
+import Mathlib.Tactic.WLOG
+
+open Set
+open Function
+
+/-
+From *Mathematics in Lean*.
+-/
+
+noncomputable section
+open Classical
+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
+    contrapose! hx
+    rw [sbSet, mem_iUnion]
+    use 0
+    rw [sbAux, mem_diff]
+    exact ⟨mem_univ _, hx⟩
+  have : ∃ y, g y = x := by
+    simp at this
+    assumption
+  exact invFun_eq 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⟩

DuperOnMathlib/DuperOnMathlib/Cantor.lean

@@ -0,0 +1,53 @@
+import Mathlib.Data.Nat.Basic
+import Mathlib.Tactic
+import DuperOnMathlib.DuperInterface
+
+open Function
+
+variable {α : Type*}
+
+theorem Cantor : ∀ f : α → Set α, ¬ Surjective f := by
+  intro f Surjf
+  rcases Surjf {i | i ∉ f i} with ⟨a, h⟩
+  have : ¬ a ∉ f a := by
+    -- nice
+    duper [h, Set.mem_setOf_eq]
+  apply this
+  rw [h]
+  exact this
+
+theorem Cantor2 : ∀ f : α → Set α, ¬ Surjective f := by
+  intro f Surjf
+  rcases Surjf {i | i ∉ f i} with ⟨a, h⟩
+  have : a ∈ f a ↔ a ∉ f a := by
+    duper [h, Set.mem_setOf_eq]
+  duper [this]
+
+-- Nice!
+theorem Cantor3 : ∀ f : α → Set α, ¬ Surjective f := by
+  intro f Surjf
+  have := Surjf {i | i ∉ f i}
+  duper [Set.mem_setOf_eq, this]
+
+namespace original
+
+theorem Cantor : ∀ f : α → Set α, ¬ Surjective f := by
+  intro f Surjf
+  rcases Surjf {i | i ∉ f i} with ⟨a, h⟩
+  have : ¬ a ∉ f a := by
+    intro h'
+    apply h'
+    rw [h]
+    exact h'
+  apply this
+  rw [h]
+  exact this
+
+theorem Cantor_alt : ∀ f : α → Set α, ¬ Surjective f := by
+  intro f Surjf
+  rcases Surjf {i | i ∉ f i} with ⟨a, h⟩
+  have : a ∈ f a ↔ a ∉ f a := by
+    nth_rewrite 1 [h]; rfl
+  tauto
+
+end original

DuperOnMathlib/DuperOnMathlib/IVT.lean

@@ -0,0 +1,83 @@
+import Mathlib.Data.Real.Basic
+
+def ApproachesAt (f : ℝ → ℝ) (b : ℝ) (a : ℝ) :=
+∀ ε, 0 < ε →  ∃ δ, 0 < δ ∧ ∀ x, abs (x - a) < δ → abs (f x - b) < ε
+
+def Continuous (f : ℝ → ℝ) := ∀ x, ApproachesAt f (f x) x
+
+theorem continuous_id : Continuous (λ x ↦ x) := by
+  intro x
+  intro ε εpos
+  use ε
+  constructor
+  exact εpos
+  intro x' h
+  simp [h]
+
+theorem ivt {f : ℝ → ℝ} {a b : ℝ} (aleb : a ≤ b)
+      (ctsf : Continuous f) (hfa : f a < 0) (hfb : 0 < f b) :
+    ∃ x, a ≤ x ∧ x ≤ b ∧ f x = 0 := by
+  set S := { x | f x ≤ 0 ∧ a ≤ x ∧ x ≤ b } with hS
+  have aS : a ∈ S := by
+    exact ⟨le_of_lt hfa, le_refl a, aleb⟩
+  have nonemptyS : S.Nonempty := ⟨a, aS⟩
+  have bddS : BddAbove S := by
+    use b
+    intro x xS
+    exact xS.2.2
+  set x₀ := sSup S with hx₀
+  have alex₀ : a ≤ x₀ := le_csSup bddS aS
+  have x₀leb : x₀ ≤ b := by
+    apply csSup_le nonemptyS
+    intro x xS
+    exact xS.2.2
+  have : ¬ 0 < f x₀ := by
+    intro h
+    rcases ctsf x₀ _ h with ⟨δ, δpos, hδ⟩
+    set x' := x₀ - δ / 2 with hx'
+    have : ∃ x'' ∈ S, x' < x'' := by
+      apply exists_lt_of_lt_csSup nonemptyS
+      rw [hx']; linarith
+    rcases this with ⟨x'', x''S, x'lt⟩
+    have : x'' ≤ x₀ := by
+      exact le_csSup bddS x''S
+    have : abs (f x'' - f x₀) < f x₀ := by
+      apply hδ
+      rw [abs_of_nonpos, neg_sub]
+      simp [hx₀] at *
+      linarith
+      linarith
+    rw [abs_lt] at this
+    simp [hS] at x''S
+    linarith
+  have : ¬ f x₀ < 0 := by
+    intro h
+    have : 0 < - f x₀ := by
+      linarith
+    rcases ctsf x₀ _ this with ⟨δ, δpos, hδ⟩
+    have x₀lt1 : x₀ < b := by
+      apply lt_of_le_of_ne x₀leb
+      intro h'
+      rw [h'] at h
+      exact lt_asymm hfb h
+    have minpos : 0 < min (δ / 2) (b - x₀) := by
+      apply lt_min; linarith
+      linarith
+    set x' := x₀ + min (δ / 2) (b - x₀) with hx'
+    have : abs (f x' - f x₀) < - f x₀ := by
+      apply hδ
+      simp [hx']
+      rw [abs_of_pos minpos]
+      apply lt_of_le_of_lt (min_le_left _ _)
+      linarith
+    have x'S : x' ∈ S := by
+      dsimp [hS, hx']
+      rw [abs_lt] at this
+      constructor; linarith
+      constructor; linarith
+      linarith [min_le_right (δ / 2) (b - x₀)]
+    have : x' ≤ x₀ := le_csSup bddS x'S
+    dsimp [hx'] at this
+    linarith
+  have : f x₀ = 0 := by linarith
+  use x₀, alex₀, x₀leb, this

DuperOnMathlib/DuperOnMathlib/ListExamples.lean

@@ -0,0 +1,40 @@
+import Mathlib.Data.List.Basic
+
+section
+variable {α : Type*} [LinearOrder α]
+
+/-- Returns a pair consisting of a minimal element of the list (or ⊥ if the list is empty) and the
+maximal element element of the list (or ⊤ if the list if empty) -/
+def foo : List α → WithBot α × WithTop α
+  | [] => (⊥, ⊤)
+  | (x :: xs) =>
+    let (min, max) := foo xs
+    (min ⊓ x, max ⊔ x)
+
+/-- An alternative definition, using `foldr` -/
+def foo' (xs : List α) : WithBot α × WithTop α :=
+  xs.foldr (fun (x : α) (p : WithBot α × WithTop α) => (Prod.fst p ⊓ x, Prod.snd p ⊔ x)) (⊥, ⊤)
+
+theorem foo'_cons (x : α) (xs : List α) : foo' (x :: xs) = ((foo' xs).fst ⊓ x, (foo' xs).snd ⊔ x) := by
+  simp [foo']
+
+theorem foo_eq_foo' (xs : List α) : foo xs = foo' xs := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih =>
+      simp [foo, foo'_cons, ih]
+
+theorem fst_foo_le (xs : List α) : ∀ x ∈ xs, (foo xs).fst ≤ x := by
+  induction xs with
+  | nil => simp [foo]
+  | cons x xs ih =>
+    intro y h
+    simp [foo]
+    simp at h
+    cases h with
+    | inl h =>
+      simp [h]
+    | inr h =>
+      simp [ih _ h]
+
+end