theorem sylow_one {G : Type*} [Group G] [Fintype G] (p : ℕ) (hp : p.Prime) (n : ℕ) (h : p ^ n ∣ Fintype.card G) : ∃ H : Subgroup G, Nat.card H = p ^ n := by haveI : Fact p.Prime := ⟨hp⟩ rw [← Nat.card_eq_fintype_card] at h exact Sy...

theorem cayley_thm {G : Type*} [Group G] : ∃ f : G →* Equiv.Perm G, Function.Injective f := ⟨{ toFun x := { toFun y := x * y invFun y := x⁻¹ * y left_inv y := inv_mul_ca...

theorem picard_little (f : ℂ → ℂ) (hf : Differentiable ℂ f) (h : ¬ ∃ c, ∀ z, f z = c) : ∀ a b : ℂ, a ≠ b → (Set.range f)ᶜ ⊆ {a, b} := sorry

theorem liouville_thm (f : ℂ → ℂ) (hf : Differentiable ℂ f) (hb : ∃ M, ∀ z, ‖f z‖ ≤ M) : ∃ c, ∀ z, f z = c := by apply hf.exists_const_forall_eq_of_bounded rw [isBounded_iff_forall_norm_l...

theorem stone_weierstrass (a b : ℝ) (hab : a ≤ b) (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc a b)) (ε : ℝ) (hε : 0 < ε) : ∃ p : Polynomial ℝ, ∀ x ∈ Set.Icc a b, |f x - p.eval x| < ε := by have _ := hab let f_cont : C(Set.Icc a b, ℝ) := ⟨Set.restrict (Set.Icc a b...

theorem bolzano_weierstrass {s : Set ℝ} (h : Bornology.IsBounded s) (hs : s.Infinite) : ∃ x, AccPt x (Filter.principal s) := by have hK_closed : IsClosed (closure s) := isClosed_closure have hK_bounded ...

theorem heine_borel (s : Set ℝ) : IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s := Metric.isCompact_iff_isClosed_bounded

theorem banach_fixed {X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} (hf : ContractingWith (1/2 : NNReal) f) : ∃! x, f x = x := by use ContractingWith.fixedPoint f hf constructor · show f (ContractingWith....

theorem brouwer_disc {n : ℕ} (f : Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 → Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1) (hf : Continuous f) : ∃ x, f x = x := sorry

theorem pythag_thm (a b c : ℝ) (h : c = Real.sqrt (a ^ 2 + b ^ 2)) : a ^ 2 + b ^ 2 = c ^ 2 := by rw [h] symm apply Real.sq_sqrt positivity