Index

A

absolute value absurd

anonymous constructor apply assumption

B

bounded quantifiers by_cases

by_contra by_contradiction

C

calc cases change check command open commands check include

commutative ring congr continuity contradiction contrapose convert

D

definitional equality differential calculus

divisibility dsimp

E

elementary calculus erw exact excluded middle

exfalso exponential ext extensionality

F

field_simp

filter from

G

gcd goal

group (algebraic structure) (tactic)

H

have, [1]

I

implicit argument include inequalities

injective function integration, [1] intros

L

lambda abstraction lattice lcm left

let linarith local context logarithm

M

max measure theory

metric space, [1] min monotone function

N

namespace

norm_num 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) (tactic) rintros rw, [1] rwa

S

set operations show

simp, [1] split surjective function

T

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

this topological space topology

U

use