theorem euclid_lemma (p a b : ℕ) (hp : p.Prime) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b := hp.dvd_or_dvd h

theorem ivt {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (y : ℝ) (hy : y ∈ Set.Icc (f a) (f b)) : ∃ c ∈ Set.Icc a b, f c = y := intermediate_value_Icc hab hf hy

theorem mean_value_thm {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a) := exists_deriv_eq_slope f hab hf hf'

theorem inverse_function_thm {f : ℝ → ℝ} {a : ℝ} (hf : ContDiffAt ℝ 1 f a) (hf' : deriv f a ≠ 0) : ∃ g : ℝ → ℝ, ∃ U ∈ nhds a, ∀ x ∈ U, g (f x) = x ∧ f (g x) = x := sorry

theorem vandermonde (m n r : ℕ) : Nat.choose (m + n) r = ∑ k ∈ Finset.range (r + 1), Nat.choose m k * Nat.choose n (r - k) := by rw [Nat.add_choose_eq] rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]

theorem geom_sum_finite {R : Type*} [CommRing R] (x : R) (n : ℕ) (h : x ≠ 1) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1 := by have _ := h exact geom_sum_mul x n

theorem powerset_card {α : Type*} [Fintype α] : Fintype.card (Set α) = 2 ^ Fintype.card α := Fintype.card_set

theorem crt {m n : ℕ} (h : Nat.Coprime m n) (a b : ℤ) : ∃ x : ℤ, x ≡ a [ZMOD m] ∧ x ≡ b [ZMOD n] := by by_cases hm : m = 0 · subst hm have hn : n = 1 := by rwa [Nat.Coprime, Nat...

theorem lagrange_thm {G : Type*} [Group G] [Fintype G] (H : Subgroup G) [Fintype H] : Fintype.card H ∣ Fintype.card G := by rw [← Nat.card_eq_fintype_card, ← Nat.card_eq_fintype_card] exact Subgroup...

theorem incl_excl_two {α : Type*} [DecidableEq α] (A B : Finset α) : (A ∪ B).card = A.card + B.card - (A ∩ B).card := by have := Finset.card_union_add_card_inter A B omega