Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
38 commits
Select commit Hold shift + click to select a range
32052aa
init
vasnesterov Mar 27, 2025
0a5f3a9
some
vasnesterov Mar 27, 2025
6e9958f
fix
vasnesterov Mar 27, 2025
2ae7f84
fix test
vasnesterov Mar 27, 2025
f658174
unused import
vasnesterov Mar 27, 2025
6dd4126
noshake
vasnesterov Mar 27, 2025
bf47ed2
speedup?
vasnesterov Mar 27, 2025
7b196eb
docstrings
vasnesterov Mar 27, 2025
6c0e637
to test
vasnesterov Mar 27, 2025
8e6058f
Merge branch 'master' into vasnesterov/exists_eq_nested_simproc
vasnesterov Mar 28, 2025
dcaf56d
to test
vasnesterov Mar 28, 2025
a58369b
remove some simp-lemmas
vasnesterov Mar 28, 2025
3df2cac
fix todos
vasnesterov Mar 28, 2025
c403bd5
suggestions
vasnesterov Mar 29, 2025
e1de23b
docs & style
vasnesterov Mar 29, 2025
29b92eb
cleanup
JovanGerb Mar 30, 2025
4204aed
more cleanup
JovanGerb Mar 31, 2025
a37edee
docs & failure
vasnesterov Apr 2, 2025
8ca6dc7
fix
vasnesterov Apr 2, 2025
bff6a58
perf: avoid ~q(_) match, for faster failure
JovanGerb Apr 2, 2025
5cb82b5
turn it into a pre simproc with `↓`
JovanGerb Apr 2, 2025
bf67931
fix test
JovanGerb Apr 2, 2025
ee50372
.
JovanGerb Apr 2, 2025
755a881
remove existsAndEq
vasnesterov Apr 8, 2025
e689696
update test
vasnesterov Apr 8, 2025
febdccb
revert noshake
vasnesterov Apr 8, 2025
a9fe3c8
Merge branch 'master' into vasnesterov/exists_eq_nested_simproc
vasnesterov Jul 7, 2025
8be544b
fix
vasnesterov Jul 7, 2025
e5020a4
Merge branch 'master' into vasnesterov/exists_eq_nested_simproc
vasnesterov Jul 31, 2025
595cefb
Merge branch 'master' into vasnesterov/exists_eq_nested_simproc
vasnesterov Aug 1, 2025
b31d85e
Merge branch 'master' into vasnesterov/exists_eq_nested_simproc
vasnesterov Aug 30, 2025
daad2ef
fix
vasnesterov Aug 31, 2025
88a9fbd
fix
vasnesterov Aug 31, 2025
d025c01
fix variables in tests
vasnesterov Aug 31, 2025
91c418d
suggestions
vasnesterov Oct 11, 2025
a210397
Merge branch 'master' into vasnesterov/exists_eq_nested_simproc
vasnesterov Oct 11, 2025
ee662cc
error messages
vasnesterov Oct 14, 2025
015862e
fix typo
vasnesterov Oct 15, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Combinatorics/SimpleGraph/Maps.lean
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ theorem map_monotone (f : V ↪ W) : Monotone (SimpleGraph.map f) := by

theorem support_map (f : V ↪ W) (G : SimpleGraph V) :
(G.map f).support = f '' G.support := by
ext; simp [mem_support]; tauto
ext; simp [mem_support]

/-- Given a function, there is a contravariant induced map on graphs by pulling back the
adjacency relation.
Expand Down
3 changes: 1 addition & 2 deletions Mathlib/Data/List/ProdSigma.lean
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,7 @@ theorem product_nil : ∀ l : List α, l ×ˢ (@nil β) = []
@[simp]
theorem mem_product {l₁ : List α} {l₂ : List β} {a : α} {b : β} :
(a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ := by
simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, and_left_comm,
exists_and_left, exists_eq_left, exists_eq_right]
simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, and_left_comm]

theorem length_product (l₁ : List α) (l₂ : List β) :
length (l₁ ×ˢ l₂) = length l₁ * length l₂ := by
Expand Down
Loading