* `Exists.intro c h` -> `Exists.intro c h.symm` in the proof of `Dvd.intro`
  (`h : a * c = b` no longer unifies with `b = a * c`?)

This one sounds like it should be fixed wherever the definition is (std?), since that issue is going to keep coming up and there isn't any strong preference for one statement over the other other than easing porting issues.

* `Exists.intro c h` -> `Exists.intro c h.symm` in the proof of `Dvd.intro`
  (`h : a * c = b` no longer unifies with `b = a * c`?)

This one sounds like it should be fixed wherever the definition is (std?), since that issue is going to keep coming up and there isn't any strong preference for one statement over the other other than easing porting issues.

Oh actually, I just forgot to check the original mathlib file. Mathport didn't translate
exists.intro c h^.symm correctly. It spat out Exists.intro c h, so no change should be required for that.

The only other change in behavior is the other thing I pointed out.

oh that's bad. Do you have a MWE? (That is, a lean 3 file with a minimum of imports with the syntax that got eaten)

I may not be greping totally correctly, but it appears this syntax is only used in the following files:

ring_theory/dedekind_domain/ideal.lean
ring_theory/adjoin_root.lean
ring_theory/nilpotent.lean
ring_theory/polynomial/basic.lean
ring_theory/ideal/quotient.lean
ring_theory/ideal/minimal_prime.lean
ring_theory/ideal/operations.lean
ring_theory/ideal/cotangent.lean
linear_algebra/quotient.lean
algebra/divisibility/basic.lean
set_theory/ordinal/notation.lean (false positive: it appears in a docstring)
number_theory/ramification_inertia.lean
number_theory/kummer_dedekind.lean

Of these, I think this file, algebra.divisibility.basic is probably the one with the least imports.

Almost all the others look like they are I^.quotient.mk for an ideal/submodule.

(I should also say: from a cursory glance, it appears that the syntax is eaten up in these other files too)

I finally got oneshot working, and this:

-- Insert lean 3 code here.

namespace foo

/-- test -/
theorem foo {A: Type} {a b : A} (h : a = b) : b = a := h^.symm

end foo

turned into this:

-- Insert lean 3 code here.

namespace Foo

/-- test -/
theorem foo {A : Type} {a b : A} (h : a = b) : b = a :=
  h
#align foo.foo Foo.foo

end Foo

(it lost the ^.symm and obviously doesn't typecheck anymore)

I'm going to assuming Mario is going to deal with the ^. issue separately, and this doesn't need to wait on that.

bors d+

✌️ mpenciak can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Please change the status to Yes at https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status/_edit when you merge.

bors r+

bors r-

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style