mathlib
documentation
core
/
init
.
meta
.
widget
.
replace_save_info
Google site search
core
/
init
.
meta
.
widget
.
replace_save_info
source
Imports
init.meta.widget.interactive_expr
Imported by
tactic
.
save_info_with_widgets
source
meta
def
tactic
.
save_info_with_widgets
(p :
pos
)
:
tactic
unit
General documentation
index
tactics
commands
hole commands
attributes
notes
references
Additional documentation
Library
core
data
buffer
dlist
vector
init
algebra
classes
functions
order
control
alternative
applicative
combinators
except
functor
id
lawful
lift
monad
monad_fail
option
reader
state
data
array
basic
slice
bool
basic
lemmas
char
basic
classes
lemmas
fin
basic
ops
int
basic
bitwise
comp_lemmas
order
list
basic
instances
lemmas
qsort
nat
basic
bitwise
div
gcd
lemmas
option
basic
instances
ordering
basic
lemmas
sigma
basic
lex
string
basic
ops
subtype
basic
instances
sum
basic
unsigned
basic
ops
prod
punit
quot
repr
set
setoid
to_string
meta
converter
conv
interactive
lean
parser
smt
congruence_closure
ematch
interactive
rsimp
smt_tactic
widget
basic
html_cmd
interactive_expr
replace_save_info
tactic_component
ac_tactics
async_tactic
attribute
backward
case_tag
comp_value_tactics
congr_lemma
congr_tactic
constructor_tactic
contradiction_tactic
declaration
derive
environment
exceptional
expr
expr_address
feature_search
float
format
fun_info
has_reflect
hole_command
injection_tactic
instance_cache
interaction_monad
interactive
interactive_base
json
level
local_context
match_tactic
mk_dec_eq_instance
mk_has_reflect_instance
mk_has_sizeof_instance
mk_inhabited_instance
module_info
name
occurrences
options
pexpr
rb_map
rec_util
ref
relation_tactics
rewrite_tactic
set_get_option_tactics
simp_tactic
tactic
tagged_format
task
type_context
vm
well_founded_tactics
cc_lemmas
classical
coe
core
default
function
funext
ite_simp
logic
propext
util
version
wf
system
io
io_interface
random
ideles
adeles_R
adeles_function_field
adeles_number_field
examples
fractional_ideal
function_field
galois
ideles_R
ideles_function_field
ideles_number_field
main_theorem_GCFT
valuation
mathlib
algebra
algebra
subalgebra
basic
pointwise
basic
bilinear
operations
restrict_scalars
tower
big_operators
associated
basic
fin
finprod
finsupp
intervals
multiset
nat_antidiagonal
option
order
pi
ring
category
CommRing
basic
Group
basic
Mon
basic
char_p
basic
two
direct_sum
basic
finsupp
module
field
basic
opposite
gcd_monoid
basic
finset
multiset
group
basic
commute
conj
defs
inj_surj
opposite
pi
prod
semiconj
to_additive
type_tags
units
with_one
group_power
basic
lemmas
order
group_with_zero
basic
defs
power
hom
aut
equiv
group
group_action
group_instances
iterate
non_unital_alg
units
module
basic
equiv
hom
linear_map
opposites
pi
prod
submodule
submodule_lattice
submodule_pointwise
monoid_algebra
basic
order
absolute_value
archimedean
field
floor
group
monoid
monoid_lemmas
nonneg
ring
sub
with_zero
polynomial
big_operators
group_ring_action
regular
basic
smul
ring
aut
basic
comp_typeclasses
equiv
opposite
pi
prod
star
basic
pi
abs
associated
bounds
char_zero
covariant_and_contravariant
direct_limit
divisibility
euclidean_domain
field_power
free_monoid
geom_sum
group_ring_action
indicator_function
invertible
is_prime_pow
opposites
parity
periodic
punit_instances
quotient
smul_with_zero
squarefree
support
algebraic_geometry
prime_spectrum
basic
noetherian
category_theory
adjunction
basic
category
basic
concrete_category
basic
bundled
bundled_hom
reflects_isomorphisms
functor
basic
category
fully_faithful
reflects_isomorphisms
pi
basic
products
basic
endomorphism
epi_mono
eq_to_hom
equivalence
essential_image
full_subcategory
groupoid
isomorphism
natural_isomorphism
natural_transformation
opposites
types
whiskering
combinatorics
quiver
basic
composition
partition
control
monad
basic
traversable
basic
derive
equiv
instances
lemmas
applicative
basic
bifunctor
equiv_functor
functor
data
array
lemmas
bool
all_any
basic
set
complex
basic
dfinsupp
basic
dlist
basic
fin
tuple
basic
basic
interval
vec_notation
finset
basic
card
fin
finsupp
fold
lattice
locally_finite
nat_antidiagonal
noncomm_prod
option
order
pairwise
pi
pointwise
powerset
preimage
prod
sigma
sort
finsupp
antidiagonal
basic
indicator
interval
multiset
order
pwo
to_dfinsupp
fintype
basic
card
fin
sort
fun_like
basic
embedding
equiv
int
basic
cast
char_zero
gcd
interval
least_greatest
modeq
order
parity
succ_pred
list
basic
big_operators
chain
count
dedup
defs
duplicate
forall2
infix
join
lattice
lex
min_max
nat_antidiagonal
nodup
nodup_equiv_fin
of_fn
pairwise
perm
permutation
prime
range
rotate
sort
sublists
tfae
zip
matrix
basic
basis
block
char_p
dmatrix
pequiv
multiset
antidiagonal
basic
bind
dedup
finset_ops
fold
lattice
nat_antidiagonal
nodup
pi
powerset
range
sort
mv_polynomial
basic
comm_ring
equiv
monad
rename
variables
nat
choose
basic
dvd
sum
factorial
basic
basic
cast
count
enat
factorization
gcd
interval
lattice
modeq
pairing
parity
periodic
pow
prime
sqrt
sqrt_norm_num
succ_pred
totient
with_bot
num
basic
option
basic
defs
pnat
basic
interval
polynomial
degree
definitions
lemmas
trailing_degree
algebra_map
basic
cancel_leads
coeff
derivative
div
erase_lead
eval
field_division
induction
inductions
integral_normalization
monic
monomial
reverse
ring_division
rat
basic
cast
floor
meta_defs
order
rbmap
basic
rbtree
default_lt
init
real
basic
cau_seq
cau_seq_completion
ennreal
nnreal
sqrt
set
intervals
basic
disjoint
image_preimage
ord_connected
pi
unordered_interval
Union_lift
accumulate
basic
countable
finite
function
functor
lattice
pairwise
pointwise
prod
sigma
set_like
basic
setoid
basic
sigma
basic
string
basic
defs
sum
basic
order
sym
basic
vector
basic
zmod
algebra
basic
bracket
char
mllist
opposite
part
pequiv
pfun
pi
pprod
prod
quot
rel
subtype
tree
ulift
dynamics
fixed_points
basic
periodic_pts
field_theory
finite
basic
is_alg_closed
algebraic_closure
basic
adjoin
finiteness
fixed
galois
intermediate_field
krull_topology
minpoly
normal
perfect_closure
primitive_element
ratfunc
separable
splitting_field
subfield
tower
group_theory
group_action
basic
big_operators
conj_act
defs
fixing_subgroup
group
opposite
pi
prod
sub_mul_action
units
perm
basic
cycle_type
cycles
fin
option
sign
subgroup
support
specific_groups
cyclic
subgroup
basic
pointwise
submonoid
basic
center
centralizer
inverses
membership
operations
pointwise
subsemigroup
basic
abelianization
archimedean
commutator
congruence
coset
exponent
finiteness
free_abelian_group
free_group
monoid_localization
order_of_element
quotient_group
solvable
linear_algebra
charpoly
basic
direct_sum
finsupp
tensor_product
free_module
finite
basic
rank
basic
rank
strong_rank_condition
matrix
charpoly
basic
coeff
adjugate
basis
bilinear_form
determinant
finite_dimensional
mv_polynomial
nondegenerate
nonsingular_inverse
polynomial
reindex
to_lin
to_linear_equiv
trace
multilinear
basic
basis
tensor_product
alternating
basic
basis
bilinear_form
bilinear_map
contraction
determinant
dfinsupp
dimension
dual
finite_dimensional
finsupp
finsupp_vector_space
invariant_basis_number
isomorphisms
linear_independent
linear_pmap
pi
prod
projection
quotient
sesquilinear_form
span
std_basis
tensor_product
tensor_product_basis
trace
vandermonde
logic
encodable
basic
lattice
equiv
basic
fin
fintype
functor
list
nat
option
set
function
basic
conjugate
iterate
basic
denumerable
embedding
is_empty
nonempty
nontrivial
relation
relator
small
unique
meta
expr
expr_lens
rb_map
number_theory
legendre_symbol
gauss_eisenstein_lemmas
quadratic_reciprocity
padics
padic_norm
zsqrtd
basic
gaussian_int
divisors
function_field
number_field
order
filter
archimedean
at_top_bot
bases
basic
cofinite
interval
lift
n_ary
partial
pi
pointwise
ultrafilter
hom
basic
bounded
complete_lattice
lattice
order
succ_pred
basic
relation
antichain
atoms
basic
boolean_algebra
bounded
bounded_order
bounds
chain
compactly_generated
compare
complete_boolean_algebra
complete_lattice
complete_lattice_intervals
conditionally_complete_lattice
copy
cover
directed
fixed_points
galois_connection
iterate
lattice
lattice_intervals
lexicographic
locally_finite
max
min_max
modular_lattice
monotone
omega_complete_partial_order
order_dual
order_iso_nat
partial_sups
pilex
rel_classes
rel_iso
sup_indep
symm_diff
well_founded
well_founded_set
zorn
ring_theory
adjoin
basic
fg
coprime
basic
lemmas
dedekind_domain
basic
ideal
integral_closure
ideal
basic
local_ring
operations
over
prod
quotient
int
basic
localization
at_prime
away
basic
fraction_ring
ideal
integer
integral
num_denom
submodule
polynomial
basic
content
gauss_lemma
rational_root
scale_roots
tower
power_series
basic
subring
basic
pointwise
subsemiring
basic
pointwise
valuation
basic
integers
adjoin_root
algebra_tower
algebraic
class_group
euclidean_domain
finiteness
fractional_ideal
free_comm_ring
free_ring
hahn_series
integral_closure
integral_domain
integrally_closed
laurent_series
matrix_algebra
multiplicity
nilpotent
noetherian
non_zero_divisors
polynomial_algebra
power_basis
principal_ideal_domain
tensor_product
trace
unique_factorization_domain
set_theory
cardinal
basic
cofinality
finite
ordinal
ordinal
arithmetic
basic
principal
schroeder_bernstein
tactic
converter
apply_congr
interactive
old_conv
linarith
datatypes
elimination
frontend
lemmas
parsing
preprocessing
verification
lint
basic
default
frontend
misc
simp
type_classes
monotonicity
basic
interactive
lemmas
nth_rewrite
basic
congr
default
abel
algebra
alias
apply
apply_fun
auto_cases
binder_matching
by_contra
cache
cancel_denoms
chain
choose
clear
congr
core
dec_trivial
delta_instance
dependencies
derive_inhabited
doc_commands
elementwise
elide
explode
ext
field_simp
fin_cases
find
finish
fix_reflect_string
fresh_names
generalize_proofs
generalizes
group
hint
interactive
interactive_expr
interval_cases
itauto
lean_core_docs
lift
localized
mk_iff_of_inductive_prop
norm_cast
norm_fin
norm_num
norm_swap
obviously
pi_instances
pretty_cases
project_dir
protected
push_neg
rcases
reassoc_axiom
rename_var
replacer
reserved_notation
restate_axiom
rewrite
ring
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
slice
solve_by_elim
split_ifs
squeeze
suggest
tauto
tfae
tidy
transform_decl
trunc_cases
unify_equations
where
with_local_reducibility
wlog
zify
topology
algebra
module
basic
nonarchimedean
bases
basic
order
basic
compact
intermediate_value
left_right
monotone_continuity
monotone_convergence
const_mul_action
constructions
field
filter_basis
group
group_completion
group_with_zero
infinite_sum
localization
monoid
mul_action
open_subgroup
ring
uniform_field
uniform_filter_basis
uniform_group
uniform_ring
valuation
valued_field
with_zero_topology
bornology
basic
continuous_function
basic
instances
int
nnreal
real
metric_space
basic
emetric_space
sets
closeds
compacts
opens
uniform_space
abstract_completion
basic
cauchy
complete_separated
completion
pi
separation
uniform_convergence
uniform_embedding
bases
basic
compact_open
connected
constructions
continuous_on
dense_embedding
homeomorph
maps
nhds_set
order
separation
sober
subset_properties
support
tactic
Color scheme
dark
system
light