Index

A

abel absolute value absurd

anonymous constructor apply, [1] assumption

B

bounded quantifiers

by_cases by_contra

C

calc cases change check command open commands check

commutative ring congr constructor continuity contradiction contrapose convert

D

decide definitional equality

differential calculus divisibility dsimp

E

elementary calculus erw exact, [1], [2] excluded middle

exfalso exponential ext extensionality

F

field_simp

Filter from

G

gcd goal

group (algebraic structure), [1] (tactic), [1]

H

have, [1]

I

implicit argument inequalities

injective function integration, [1] intro

L

lambda abstraction lattice lcm left

let linarith linear map local context logarithm

M

matrices max measure theory

metric space, [1] min monoid monotone function

N

namespace

normed space

O

open	order relation

P

partial order

proof state push_neg

R

rcases real numbers reflexivity repeat rewrite rfl

right ring (algebraic structure), [1] (tactic) rintro rw, [1] rwa

S

set operations show

simp, [1] surjective function

T

tactics abel, [1] apply, [1] assumption by_cases by_contra and by_contradiction calc cases change congr constructor continuity contradiction contrapose convert decide dsimp erw exact, [1], [2] exfalso ext field_simp from group, [1] have, [1] intro left let linarith noncomm_ring push_neg rcases refl and reflexivity repeat right ring rintro rw and rewrite, [1] rwa show simp, [1] use

this topological space topology

U

use

V

vector space

vector subspace