PatrickMassot

import order.basic .simplex_category data.finset data.finsupp algebra.group

local notation ` [`n`] ` := fin (n+1)

/-- Simplicial set -/
class simplicial_set :=
(objs : Π n : ℕ, Type*)
(maps {m n : ℕ} {f : [m] → [n]} (hf : monotone f) : objs n → objs m)
(comp {l m n : ℕ} {f : [l] → [m]} {g : [m] → [n]} (hf : monotone f) (hg : monotone g) :
  (maps hf) ∘ (maps hg) = (maps (monotone_comp hf hg)))

PatrickMassot

import algebra.ring
import group_theory.submonoid
import tactic.interactive

namespace tactic

open tactic.interactive

meta def derive_field_subtype : tactic unit :=
do b ← target >>= is_prop,

PatrickMassot

/- The goal of this file is to explain why it's important that using extends in
   command `class foo extends bar` creates a `foo.to_bar` function with an 
   instance implicit parameter.
   
   We will define magmas with law denoted by ◆ and a commutative version.
   Then we want products of such things. The goal is to reuse the work on product
   magmas when defining product commutative magmas, and do so in a completely
   transparent way. -/

-- Defining magmas with some notation is already covered in TPIL

PatrickMassot

import analysis.topology.topological_structures
import group_theory.quotient_group

open function set

variables {α : Type*} [topological_space α] {β : Type*} [topological_space β]
variables {γ : Type*} [topological_space γ] {δ : Type*} [topological_space δ]

def is_open_map (f : α → β) := ∀ U : set α, is_open U → is_open (f '' U)

PatrickMassot

/-
This file defines the I-adic topology on a commutative ring R with ideal I.

The ring is wrapped in `adic_ring I := R`, which then receive all relevant type classes.
The end-product is `instance : topological_ring (adic_ring I)`.
-/

import tactic.ring
import data.pnat
import ring_theory.ideal_operations

PatrickMassot

import tempfile
from pathlib import Path
from invoke import task

LEAN_CONTROL="""Package: lean
Version: {}
Section: math
Priority: optional
Architecture: amd64
Depends: git (>= 1.2)

PatrickMassot

import tactic.interactive
import tactic.linarith

@[derive decidable_eq]
inductive people : Type | Brown | Jones | Smith

constant only_child : people → Prop
constant salary : people → ℕ

@[derive decidable_eq]

PatrickMassot

import tactic.interactive
import algebra.order



open tactic expr

namespace push_neg
section

PatrickMassot

import order.basic

open tactic interactive (parse) interactive (loc.ns)
     interactive.types (texpr location) lean.parser (tk)

local postfix `?`:9001 := optional

meta def apply_fun_name (e : expr) (h : name) (M : option pexpr) : tactic unit :=
do {
  H ← get_local h,

PatrickMassot

import tactic.interactive

open tactic declaration environment

/-- test that name was not auto-generated -/
@[reducible] def name.is_not_auto (n : name) : Prop :=
n.components.ilast ∉ [`no_confusion, `rec_on, `cases_on, `no_confusion_type, `sizeof, 
                      `rec, `mk, `sizeof_spec, `inj_arrow, `has_sizeof_inst, `inj_eq, `inj]

/-- Print the declaration name if it's a definition without a docstring -/