mathlib3
feat(tactic/conv/apply_congr): using congruence lemmas inside conv
#2221
Merged
Merged
feat(tactic/conv/apply_congr): using congruence lemmas inside conv #2221
mergify
merged
34 commits into
master
from
apply_congr
Merge pull request #1 from leanprover-community/master
4a7c517b
Update interactive.lean
9bd3f589
Add files via upload
9bade296
Add files via upload
b9679407
Rename operand_test.lean to operand.lean
0094245e
Update and rename zoom_test.lean to zoom.lean
eb8e6e22
Update operand.lean
42cf8d49
Update tactics.md
722e98d6
Update operand.lean
13d467d2
Update operand.lean
d4e92157
Update operand.lean
1945af34
Update operand.lean
10862734
Update operand.lean
097f439b
Update zoom.lean
4adc0733
Update operand.lean
a49097d4
Update interactive.lean
aeba4372
Update tactics.md
7f4f3511
Update operand.lean
3730372e
Merge branch 'master' into operand
ed52b7b5
merge
2faf7a04
merge
8bc4750d
feat(tactic/converter/apply_congr): apply congruence lemmas in conv
26fb0883
last example
3d348711
fix docs
73a0f96b
Apply suggestions from code review
3492cf86
remove docs from tactics.md
386a16d8
Merge branch 'apply_congr' of github.com:leanprover-community/mathlib…
6cce9eff
merge doc comment fragments
0449c43c
import in tactic.basic
8f1e9d41
Merge remote-tracking branch 'origin/master' into apply_congr
22dee328
Merge remote-tracking branch 'origin/master' into apply_congr
31753be5
docs
90482a51
add to conv doc tactic
550458bf
robertylewis
approved these changes
on 2020-03-24
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into apply_congr
746382dc
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub