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 -/

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

/-
This file is intended for Lean beginners. The goal is to demonstrate what it feels like to prove
things using Lean and mathlib. Complicated definitions and theory building are not covered.
-/

-- We want real numbers and their basic properties
import data.real.basic

-- We want to be able to define functions using the law of excluded middle
local attribute [instance, priority 0] classical.prop_decidable

PatrickMassot

import tactic.interactive
import algebra.order



open tactic expr

namespace push_neg
section

PatrickMassot

{
	"Type*": {
                "prefix": "Type*",
                "body": [
                  "{$1 : Type*}$0"
                ],
        "description": "Type* variable",
        },
        "Variables": {
                "prefix": "var",

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 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

/-
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 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

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,