b-mehta

import data.set.basic
import data.set.finite
import order.closure
import order.zorn
import tactic.by_contra

inductive prop (L : Type)
| prim : L → prop
| false : prop
| impl : prop → prop → prop

b-mehta

import data.nat.prime
import tactic

open nat

lemma thing' {a b c : ℕ} (ha : 0 < a) (hab : a < b) (hbc : b < c)
  (recip : (a : ℚ)⁻¹ + (b : ℚ)⁻¹ + (c : ℚ)⁻¹ = 1) :
  prime (a + b + c) :=
begin
  cases lt_or_ge a 3,

b-mehta

import control.bifunctor
import data.multiset.basic
import tactic

example {α} {x : α} {xs : multiset α} : {x} ≤ x :: xs :=
begin
  rw multiset.singleton_eq_singleton,
  apply multiset.cons_le_cons,
  apply zero_le,
end

b-mehta

import analysis.special_functions.trigonometric

noncomputable theory
open real

lemma thingy {u : ℝ} (h : -1 ≤ u) (ha : u ≤ 1) : u ^ 2 ≤ 1 :=
begin
  have : abs u ≤ 1,
    rw abs_le, simp [h, ha],
  have : (abs u)^2 ≤ 1^2,

b-mehta

import topology.compact_open
import category_theory.closed.cartesian
import topology.category.Top
import category_theory.limits.shapes

open_locale topological_space
namespace category_theory
open limits

universes v u

b-mehta

Here's a quick list of things I'd like to see done in Lean, some of these could form good student projects depending on the student's background: They're a mix of category theory and combinatorics since those are the things I've done most in Lean. I'll add a disclaimer that there are people who believe category theory in Lean is hard for beginners, I disagree but of course your experience may differ from mine. An advantage of category theory in Lean though is that the Isabelle people are nowhere close to getting any, so you get to flex on them.
- Adjoint functor theorems
  - For someone who's seen a small amount of category theory either of these should be pretty manageable: I don't think there are any steps of the proof which are particularly hard in Lean.
- Enriched categories
  - Requires familiarity with category theory, some work has already been done in special cases by Scott Morrison and Markus Himmel, might be hard in Lean.
- Filtered colimits (+commuting with finite limits in Set)
  - Requires famili

b-mehta

import data.finset
import category_theory.category
import category_theory.isomorphism

namespace category_theory
open set category_theory.category

universes v u

/-- A partition of the type s into finitely many bits -/

b-mehta

 Freeze display
Tactic State
4 goals
α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_functor : α ⥤ β,
e_inverse : β ⥤ α,
e_unit_iso : 𝟭 α ≅ e_functor ⋙ e_inverse,

b-mehta

 Freeze display
Tactic State
1 goal
α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_inverse_obj : β → α,
e_inverse_map : Π {X Y : β}, (X ⟶ Y) → (e_inverse_obj X ⟶ e_inverse_obj Y),
e_inverse_map_id' :

b-mehta

import category_theory.monad.algebra
import data.sigma

namespace category_theory

open category_theory category_theory.category category_theory.limits comonad

universes v u

variables {C : Type u} [small_category C]