local properties on charted spaces

Stream: maths

[Heather Macbeth]

@Scott Morrison I did this as an experiment

[Heather Macbeth]

https://github.com/leanprover-community/mathlib/tree/local_invariant_prop

[Heather Macbeth]

I was trying to get local_invariant_prop working as a local_predicate, as we discussed the other day.

[Scott Morrison]

le_of_hom should solve at least some of your sorries

[Heather Macbeth]

Oh good!

[Heather Macbeth]

The other two sorries are goals of the following form: f (⇑i ⟨y, hy⟩) = f ⟨y, _⟩

[Heather Macbeth]

Can that be deduced from i: U ⟶ V?

[Scott Morrison]

They both work by refl!

[Scott Morrison]

nicely done!

[Scott Morrison]

Just earlier this evening I was feeling guilty about not having attempted this :-)

[Heather Macbeth]

OK, I pushed an updated version with the sorries solved. If it fits well into your PR, feel free to (clean up and) use it.