CanLift !4#2256

Stream: mathlib4

[Johan Commelin]

The lift tactic has been ported. So we should add some CanLift instances back and look for porting notes about proofs using lift.

[Johan Commelin]

I'm currently :fencing: but can look at it afterwards if nobody else is faster

[Ruben Van de Velde]

Huh, I thought I'd caught them all in !4#1425 and !4#1426

[Johan Commelin]

Mathlib/Data/Rat/Lemmas.lean
204:    -- Porting note: was `lift (m : ℚ) / n to ℤ using h with k hk`
215:  -- Porting note: was `lift b to ℕ using le_of_lt hb0`
222:  -- Porting note: was `lift b to ℕ using le_of_lt hb0`

Mathlib/Data/Set/Intervals/OrdConnectedComponent.lean
231:    -- porting note: lift not implemented yet