Index

A

absolute value absurd

anonyomous 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 contradiction contrapose convert

D

definitional equality

divisibility dsimp

E

erw exact excluded middle

exfalso exponential ext extentionality

F

filter

from

G

gcd goal

group (algebraic structure) (tactic)

H

have, [1]

I

implicit argument include

inequalities injective function intros

L

lambda abstraction lattice lcm left

let linarith local context logarithm

M

max metric space

min monotone function

N

namespace

norm_num

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

tactics abel apply assumption by_cases by_contra and by_contradiction calc cases change congr 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 topology

U

use