Qiu233

import Lean

open Lean Parser.Term

local instance : Monad List where
  pure x := [x]
  bind la alb := la.map alb |>.join

local instance : Alternative List where
  failure := []

Qiu233

import Lean

inductive LamTerm where
| var (n : Nat)
| app (M N : LamTerm)
| abs (M : LamTerm)

instance : ToString LamTerm where
  toString :=
    let rec f := fun t =>

Qiu233

import Mathlib

theorem Equiv.comp_of_invFun [Nonempty α] [Nonempty β] (f : α ≃ β) (g : β ≃ γ) :
    f.invFun ∘ g.invFun = (g ∘ f).invFun := by
  ext t
  unfold Function.invFun
  if h : ∃ x, (g ∘ f) x = t
    then
      rw [dif_pos h]
      apply (Function.Injective.comp g.injective f.injective ·)

Qiu233

import Mathlib

/-
The `Partition α` is a `partitions : Set (Set α)` such that:
* `⋃₀ partitions = Set.univ`,
* every distinct pair `A B ∈ partitions` are disjoint.

A `Partition α` is called **uniform** if all of its `S ∈ partitions` have the same cardinal.
Existence of `Fin n ≃ α ` equivalently means `Nat.card α = n`, for any finite type `α`.