mfld_set_tac broken

Stream: mathlib4

[Winston Yin (尹維晨)]

It looks like mfld_set_tac is currently broken, and that's been blocking mathlib4#1052. Would any of the tactic gurus please take a look at this?

Speaking of mathlib4#1052, some proofs that used to be golfed by simp in mathlib3 don't work in mathlib4, but rw [the, lemmas, printed, by, tracing, the, simp] work. I would've thought that simp should be strictly more powerful than rw in these kinds of cases, but I haven't gotten to the bottom of this.

[Heather Macbeth]

@Winston Yin (尹維晨) I see that the mathport base used by Chris three weeks ago
https://github.com/leanprover-community/mathlib4/pull/1052/commits/cf6c85053f1e55e8b9d4577d415360f7ed344bee
differs substantially from current mathport output
https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Logic/Equiv/LocalEquiv.lean
In particular it's missing

attribute [mfld_simps]
  id.def Function.comp.left_id Set.mem_setOf_eq Set.image_eq_empty Set.univ_inter Set.preimage_univ Set.prod_mk_mem_set_prod_eq and_true_iff Set.mem_univ Set.mem_image_of_mem true_and_iff Set.mem_inter_iff Set.mem_preimage Function.comp_apply Set.inter_subset_left Set.mem_prod Set.range_id Set.range_prod_map and_self_iff Set.mem_range_self eq_self_iff_true forall_const forall_true_iff Set.inter_univ Set.preimage_id Function.comp.right_id not_false_iff and_imp Set.prod_inter_prod Set.univ_prod_univ true_or_iff or_true_iff Prod.map_mk Set.preimage_inter heq_iff_eq Equiv.sigma_equiv_prod_apply Equiv.sigma_equiv_prod_symm_apply Subtype.coe_mk Equiv.to_fun_as_coe Equiv.inv_fun_as_coe

[Heather Macbeth]

Having those lemmas not marked as mfld_simps would definitely make mfld_set_tac toothless!

[Winston Yin (尹維晨)]

Oh! I was wondering why the test file for mfld_set_tac had Set.mem_setOf_eq but there's no mfld_simps attribute on its definition. Thanks!

[Winston Yin (尹維晨)]

mathlib4#1052 now compiles, preserving old functionality!