[Merged by Bors] - refactor(tactic/lift): remove attribute/simp-set and swap side goal

src/algebra/add_torsor.lean

@@ -335,7 +335,7 @@ def const_vadd_hom : multiplicative G →* equiv.perm P :=
 
 variable {P}
 
-open function
+open _root_.function
 
 /-- Point reflection in `x` as a permutation. -/
 def point_reflection (x : P) : perm P := (const_vsub x).trans (vadd_const x)

src/algebra/group/units.lean

@@ -353,10 +353,8 @@ lemma is_unit_of_subsingleton [monoid M] [subsingleton M] (a : M) : is_unit a :=
 
 attribute [nontriviality] is_add_unit_of_subsingleton
 
-@[to_additive] instance [monoid M] : can_lift M Mˣ :=
-{ coe := coe,
-  cond := is_unit,
-  prf := λ _, id }
+@[to_additive] instance [monoid M] : can_lift M Mˣ coe is_unit :=
+{ prf := λ _, id }
 
 @[to_additive] instance [monoid M] [subsingleton M] : unique Mˣ :=
 { default := 1,

src/algebra/group/with_one.lean

@@ -94,10 +94,8 @@ lemma ne_one_iff_exists {x : with_one α} : x ≠ 1 ↔ ∃ (a : α), ↑a = x :
 option.ne_none_iff_exists
 
 @[to_additive]
-instance : can_lift (with_one α) α :=
-{ coe := coe,
-  cond := λ a, a ≠ 1,
-  prf := λ a, ne_one_iff_exists.1 }
+instance can_lift : can_lift (with_one α) α coe (λ a, a ≠ 1) :=
+{ prf := λ a, ne_one_iff_exists.1 }
 
 @[simp, norm_cast, to_additive]
 lemma coe_inj {a b : α} : (a : with_one α) = b ↔ a = b :=

src/analysis/complex/upper_half_plane/basic.lean

@@ -48,7 +48,7 @@ namespace upper_half_plane
 
 instance : inhabited ℍ := ⟨⟨complex.I, by simp⟩⟩
 
-instance : can_lift ℂ ℍ := subtype.can_lift (λ z, 0 < z.im)
+instance can_lift : can_lift ℂ ℍ coe (λ z, 0 < z.im) := subtype.can_lift (λ z, 0 < z.im)
 
 /-- Imaginary part -/
 def im (z : ℍ) := (z : ℂ).im

src/data/complex/basic.lean

@@ -66,10 +66,8 @@ lemma of_real_def (r : ℝ) : (r : ℂ) = ⟨r, 0⟩ := rfl
 theorem of_real_injective : function.injective (coe : ℝ → ℂ) :=
 λ z w, congr_arg re
 
-instance : can_lift ℂ ℝ :=
-{ cond := λ z, z.im = 0,
-  coe := coe,
-  prf := λ z hz, ⟨z.re, ext rfl hz.symm⟩ }
+instance can_lift : can_lift ℂ ℝ coe (λ z, z.im = 0) :=
+{ prf := λ z hz, ⟨z.re, ext rfl hz.symm⟩ }
 
 /-- The product of a set on the real axis and a set on the imaginary axis of the complex plane,
 denoted by `s ×ℂ t`. -/

src/data/finset/basic.lean

@@ -212,18 +212,15 @@ instance {α : Type u} : has_coe_to_sort (finset α) (Type u) := ⟨λ s, {x //
 
 instance pi_finset_coe.can_lift (ι : Type*) (α : Π i : ι, Type*) [ne : Π i, nonempty (α i)]
   (s : finset ι) :
-can_lift (Π i : s, α i) (Π i, α i) :=
-{ coe := λ f i, f i,
-  .. pi_subtype.can_lift ι α (∈ s) }
+  can_lift (Π i : s, α i) (Π i, α i) (λ f i, f i) (λ _, true) :=
+pi_subtype.can_lift ι α (∈ s)
 
 instance pi_finset_coe.can_lift' (ι α : Type*) [ne : nonempty α] (s : finset ι) :
-  can_lift (s → α) (ι → α) :=
+  can_lift (s → α) (ι → α) (λ f i, f i) (λ _, true) :=
 pi_finset_coe.can_lift ι (λ _, α) s
 
-instance finset_coe.can_lift (s : finset α) : can_lift α s :=
-{ coe := coe,
-  cond := λ a, a ∈ s,
-  prf := λ a ha, ⟨⟨a, ha⟩, rfl⟩ }
+instance finset_coe.can_lift (s : finset α) : can_lift α s coe (λ a, a ∈ s) :=
+{ prf := λ a ha, ⟨⟨a, ha⟩, rfl⟩ }
 
 @[simp, norm_cast] lemma coe_sort_coe (s : finset α) :
   ((s : set α) : Sort*) = s := rfl
@@ -2163,10 +2160,9 @@ by { rw mem_image, simp only [exists_prop, const_apply, exists_and_distrib_right
 lemma mem_image_const_self : b ∈ s.image (const α b) ↔ s.nonempty :=
 mem_image_const.trans $ and_iff_left rfl
 
-instance [can_lift β α] : can_lift (finset β) (finset α) :=
-{ cond := λ s, ∀ x ∈ s, can_lift.cond α x,
-  coe := image can_lift.coe,
-  prf :=
+instance can_lift (c) (p) [can_lift β α c p] :
+  can_lift (finset β) (finset α) (image c) (λ s, ∀ x ∈ s, p x) :=
+{ prf :=
     begin
       rintro ⟨⟨l⟩, hd : l.nodup⟩ hl,
       lift l to list α using hl,
@@ -2445,7 +2441,7 @@ begin
   split, swap,
   { rintro ⟨t, ht, rfl⟩, rw [coe_image], exact set.image_subset f ht },
   intro h,
-  letI : can_lift β s := ⟨f ∘ coe, λ y, y ∈ f '' s, λ y ⟨x, hxt, hy⟩, ⟨⟨x, hxt⟩, hy⟩⟩,
+  letI : can_lift β s (f ∘ coe) (λ y, y ∈ f '' s) := ⟨λ y ⟨x, hxt, hy⟩, ⟨⟨x, hxt⟩, hy⟩⟩,
   lift t to finset s using h,
   refine ⟨t.map (embedding.subtype _), map_subtype_subset _, _⟩,
   ext y, simp

src/data/finsupp/defs.lean

@@ -524,10 +524,8 @@ noncomputable def of_support_finite
 lemma of_support_finite_coe {f : α → M} {hf : (function.support f).finite} :
   (of_support_finite f hf : α → M) = f := rfl
 
-instance : can_lift (α → M) (α →₀ M) :=
-{ coe := coe_fn,
-  cond := λ f, (function.support f).finite,
-  prf := λ f hf, ⟨of_support_finite f hf, rfl⟩ }
+instance can_lift : can_lift (α → M) (α →₀ M) coe_fn (λ f, (function.support f).finite) :=
+{ prf := λ f hf, ⟨of_support_finite f hf, rfl⟩ }
 
 end of_support_finite
 

src/data/list/basic.lean

@@ -208,10 +208,9 @@ by rw [range_map, subtype.range_coe]
 
 /-- If each element of a list can be lifted to some type, then the whole list can be lifted to this
 type. -/
-instance [h : can_lift α β] : can_lift (list α) (list β) :=
-{ coe := list.map h.coe,
-  cond := λ l, ∀ x ∈ l, can_lift.cond β x,
-  prf  := λ l H,
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (list α) (list β) (list.map c) (λ l, ∀ x ∈ l, p x) :=
+{ prf  := λ l H,
     begin
       rw [← set.mem_range, range_map],
       exact λ a ha, can_lift.prf a (H a ha),

src/data/multiset/basic.lean

@@ -822,10 +822,9 @@ quotient.induction_on₂ s t $ λ l₁ l₂, congr_arg coe $ map_append _ _ _
 
 /-- If each element of `s : multiset α` can be lifted to `β`, then `s` can be lifted to
 `multiset β`. -/
-instance [can_lift α β] : can_lift (multiset α) (multiset β) :=
-{ cond := λ s, ∀ x ∈ s, can_lift.cond β x,
-  coe := map can_lift.coe,
-  prf := by { rintro ⟨l⟩ hl, lift l to list β using hl, exact ⟨l, coe_map _ _⟩ } }
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (multiset α) (multiset β) (map c) (λ s, ∀ x ∈ s, p x) :=
+{ prf := by { rintro ⟨l⟩ hl, lift l to list β using hl, exact ⟨l, coe_map _ _⟩ } }
 
 /-- `multiset.map` as an `add_monoid_hom`. -/
 def map_add_monoid_hom (f : α → β) : multiset α →+ multiset β :=

src/data/nat/enat.lean

@@ -35,7 +35,7 @@ variables {m n : ℕ∞}
 @[simp, norm_cast] lemma coe_sub (m n : ℕ) : ↑(m - n) = (m - n : ℕ∞) := rfl
 @[simp, norm_cast] lemma coe_mul (m n : ℕ) : ↑(m * n) = (m * n : ℕ∞) := with_top.coe_mul
 
-instance : can_lift ℕ∞ ℕ := with_top.can_lift
+instance can_lift : can_lift ℕ∞ ℕ coe (λ n, n ≠ ⊤) := with_top.can_lift
 
 /-- Conversion of `ℕ∞` to `ℕ` sending `∞` to `0`. -/
 def to_nat : monoid_with_zero_hom ℕ∞ ℕ :=

src/data/pnat/basic.lean

@@ -422,11 +422,11 @@ end pnat
 
 section can_lift
 
-instance nat.can_lift_pnat : can_lift ℕ ℕ+ :=
-⟨coe, λ n, 0 < n, λ n hn, ⟨nat.to_pnat' n, pnat.to_pnat'_coe hn⟩⟩
+instance nat.can_lift_pnat : can_lift ℕ ℕ+ coe ((<) 0) :=
+⟨λ n hn, ⟨nat.to_pnat' n, pnat.to_pnat'_coe hn⟩⟩
 
-instance int.can_lift_pnat : can_lift ℤ ℕ+ :=
-⟨coe, λ n, 0 < n, λ n hn, ⟨nat.to_pnat' (int.nat_abs n),
+instance int.can_lift_pnat : can_lift ℤ ℕ+ coe ((<) 0) :=
+⟨λ n hn, ⟨nat.to_pnat' (int.nat_abs n),
   by rw [coe_coe, nat.to_pnat'_coe, if_pos (int.nat_abs_pos_of_ne_zero hn.ne'),
     int.nat_abs_of_nonneg hn.le]⟩⟩
 

src/data/rat/defs.lean

@@ -764,8 +764,8 @@ by { conv_rhs { rw [←(@num_denom q), hq] }, rw [coe_int_eq_mk], refl }
 lemma denom_eq_one_iff (r : ℚ) : r.denom = 1 ↔ ↑r.num = r :=
 ⟨rat.coe_int_num_of_denom_eq_one, λ h, h ▸ rat.coe_int_denom r.num⟩
 
-instance : can_lift ℚ ℤ :=
-⟨coe, λ q, q.denom = 1, λ q hq, ⟨q.num, coe_int_num_of_denom_eq_one hq⟩⟩
+instance can_lift : can_lift ℚ ℤ coe (λ q, q.denom = 1) :=
+⟨λ q hq, ⟨q.num, coe_int_num_of_denom_eq_one hq⟩⟩
 
 theorem coe_nat_eq_mk (n : ℕ) : ↑n = n /. 1 :=
 by rw [← int.cast_coe_nat, coe_int_eq_mk]

src/data/rat/nnrat.lean

@@ -41,10 +41,8 @@ instance : has_coe ℚ≥0 ℚ := ⟨subtype.val⟩
 /- Simp lemma to put back `n.val` into the normal form given by the coercion. -/
 @[simp] lemma val_eq_coe (q : ℚ≥0) : q.val = q := rfl
 
-instance : can_lift ℚ ℚ≥0 :=
-{ coe := coe,
-  cond := λ q, 0 ≤ q,
-  prf := λ q hq, ⟨⟨q, hq⟩, rfl⟩ }
+instance can_lift : can_lift ℚ ℚ≥0 coe (λ q, 0 ≤ q) :=
+{ prf := λ q hq, ⟨⟨q, hq⟩, rfl⟩ }
 
 @[ext] lemma ext : (p : ℚ) = (q : ℚ) → p = q := subtype.ext
 

src/data/real/ennreal.lean

@@ -104,10 +104,8 @@ instance : inhabited ℝ≥0∞ := ⟨0⟩
 
 instance : has_coe ℝ≥0 ℝ≥0∞ := ⟨ option.some ⟩
 
-instance : can_lift ℝ≥0∞ ℝ≥0 :=
-{ coe := coe,
-  cond := λ r, r ≠ ∞,
-  prf := λ x hx, ⟨option.get $ option.ne_none_iff_is_some.1 hx, option.some_get _⟩ }
+instance can_lift : can_lift ℝ≥0∞ ℝ≥0 coe (λ r, r ≠ ∞) :=
+{ prf := λ x hx, ⟨option.get $ option.ne_none_iff_is_some.1 hx, option.some_get _⟩ }
 
 @[simp] lemma none_eq_top : (none : ℝ≥0∞) = ∞ := rfl
 @[simp] lemma some_eq_coe (a : ℝ≥0) : (some a : ℝ≥0∞) = (↑a : ℝ≥0∞) := rfl

src/data/real/ereal.lean

@@ -101,10 +101,8 @@ protected def rec {C : ereal → Sort*} (h_bot : C ⊥) (h_real : Π a : ℝ, C
 
 /-! ### Real coercion -/
 
-instance : can_lift ereal ℝ :=
-{ coe := coe,
-  cond := λ r, r ≠ ⊤ ∧ r ≠ ⊥,
-  prf := λ x hx,
+instance can_lift : can_lift ereal ℝ coe (λ r, r ≠ ⊤ ∧ r ≠ ⊥) :=
+{ prf := λ x hx,
   begin
     induction x using ereal.rec,
     { simpa using hx },
@@ -160,10 +158,10 @@ lemma to_real_le_to_real {x y : ereal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y 
   x.to_real ≤ y.to_real :=
 begin
   lift x to ℝ,
+  { simp [hx, (h.trans_lt (lt_top_iff_ne_top.2 hy)).ne], },
   lift y to ℝ,
-  { simpa using h },
   { simp [hy, ((bot_lt_iff_ne_bot.2 hx).trans_le h).ne'] },
-  { simp [hx, (h.trans_lt (lt_top_iff_ne_top.2 hy)).ne], },
+  simpa using h
 end
 
 lemma coe_to_real {x : ereal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) : (x.to_real : ereal) = x :=
@@ -287,8 +285,8 @@ def ne_top_bot_equiv_real : ({⊥, ⊤}ᶜ : set ereal) ≃ ℝ :=
   inv_fun := λ x, ⟨x, by simp⟩,
   left_inv := λ ⟨x, hx⟩, subtype.eq $ begin
     lift x to ℝ,
+    { simpa [not_or_distrib, and_comm] using hx },
     { simp },
-    { simpa [not_or_distrib, and_comm] using hx }
   end,
   right_inv := λ x, by simp }
 

src/data/real/nnreal.lean

@@ -68,7 +68,7 @@ instance : has_coe ℝ≥0 ℝ := ⟨subtype.val⟩
 /- Simp lemma to put back `n.val` into the normal form given by the coercion. -/
 @[simp] lemma val_eq_coe (n : ℝ≥0) : n.val = n := rfl
 
-instance : can_lift ℝ ℝ≥0 := subtype.can_lift _
+instance can_lift : can_lift ℝ ℝ≥0 coe (λ r, 0 ≤ r) := subtype.can_lift _
 
 protected lemma eq {n m : ℝ≥0} : (n : ℝ) = (m : ℝ) → n = m := subtype.eq
 

src/data/set/basic.lean

@@ -115,12 +115,11 @@ instance {α : Type u} : has_coe_to_sort (set α) (Type u) := ⟨λ s, {x // x 
 
 instance pi_set_coe.can_lift (ι : Type u) (α : Π i : ι, Type v) [ne : Π i, nonempty (α i)]
   (s : set ι) :
-  can_lift (Π i : s, α i) (Π i, α i) :=
-{ coe := λ f i, f i,
-  .. pi_subtype.can_lift ι α s }
+  can_lift (Π i : s, α i) (Π i, α i) (λ f i, f i) (λ _, true) :=
+pi_subtype.can_lift ι α s
 
 instance pi_set_coe.can_lift' (ι : Type u) (α : Type v) [ne : nonempty α] (s : set ι) :
-  can_lift (s → α) (ι → α) :=
+  can_lift (s → α) (ι → α) (λ f i, f i) (λ _, true) :=
 pi_set_coe.can_lift ι (λ _, α) s
 
 end set
@@ -2159,10 +2158,9 @@ is_compl.compl_eq is_compl_range_inl_range_inr.symm
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq
 
-instance can_lift [can_lift α β] : can_lift (set α) (set β) :=
-{ coe := λ s, can_lift.coe '' s,
-  cond := λ s, ∀ x ∈ s, can_lift.cond β x,
-  prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
+{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
 
 @[simp] theorem range_quotient_mk [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_quot_mk _

src/data/set/finite.lean

@@ -104,10 +104,8 @@ theorem finite.exists_finset_coe {s : set α} (h : s.finite) :
 by { casesI h, exact ⟨s.to_finset, s.coe_to_finset⟩ }
 
 /-- Finite sets can be lifted to finsets. -/
-instance : can_lift (set α) (finset α) :=
-{ coe := coe,
-  cond := set.finite,
-  prf := λ s hs, hs.exists_finset_coe }
+instance : can_lift (set α) (finset α) coe set.finite :=
+{ prf := λ s hs, hs.exists_finset_coe }
 
 /-- A set is infinite if it is not finite.
 

src/linear_algebra/quadratic_form/basic.lean

@@ -629,10 +629,9 @@ abbreviation associated' : quadratic_form R M →ₗ[ℤ] bilin_form R M :=
 associated_hom ℤ
 
 /-- Symmetric bilinear forms can be lifted to quadratic forms -/
-instance : can_lift (bilin_form R M) (quadratic_form R M) :=
-{ coe := associated_hom ℕ,
-  cond := bilin_form.is_symm,
-  prf := λ B hB, ⟨B.to_quadratic_form, associated_left_inverse _ hB⟩ }
+instance can_lift :
+  can_lift (bilin_form R M) (quadratic_form R M) (associated_hom ℕ) bilin_form.is_symm :=
+{ prf := λ B hB, ⟨B.to_quadratic_form, associated_left_inverse _ hB⟩ }
 
 /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated
 bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/

src/logic/embedding.lean

@@ -34,10 +34,8 @@ instance {α : Sort u} {β : Sort v} : embedding_like (α ↪ β) α β :=
   injective' := embedding.inj',
   coe_injective' := λ f g h, by { cases f, cases g, congr' } }
 
-instance {α β : Sort*} : can_lift (α → β) (α ↪ β) :=
-{ coe := coe_fn,
-  cond := injective,
-  prf := λ f hf, ⟨⟨f, hf⟩, rfl⟩ }
+instance {α β : Sort*} : can_lift (α → β) (α ↪ β) coe_fn injective :=
+{ prf := λ f hf, ⟨⟨f, hf⟩, rfl⟩ }
 
 end function
 

src/logic/equiv/basic.lean

@@ -1657,10 +1657,8 @@ lemma of_bijective_apply_symm_apply (f : α → β) (hf : bijective f) (x : β)
   (of_bijective f hf).symm (f x) = x :=
 (of_bijective f hf).symm_apply_apply x
 
-instance : can_lift (α → β) (α ≃ β) :=
-{ coe := coe_fn,
-  cond := bijective,
-  prf := λ f hf, ⟨of_bijective f hf, rfl⟩ }
+instance : can_lift (α → β) (α ≃ β) coe_fn bijective :=
+{ prf := λ f hf, ⟨of_bijective f hf, rfl⟩ }
 
 section
 

src/order/bounded_order.lean

@@ -599,10 +599,8 @@ by { cases x, simpa using h, refl, }
 @[simp] lemma unbot_coe (x : α) (h : (x : with_bot α) ≠ ⊥ := coe_ne_bot) :
   (x : with_bot α).unbot h = x := rfl
 
-instance : can_lift (with_bot α) α :=
-{ coe := coe,
-  cond := λ r, r ≠ ⊥,
-  prf := λ x h, ⟨x.unbot h, coe_unbot _ _⟩ }
+instance can_lift : can_lift (with_bot α) α coe (λ r, r ≠ ⊥) :=
+{ prf := λ x h, ⟨x.unbot h, coe_unbot _ _⟩ }
 
 section has_le
 variables [has_le α]
@@ -949,10 +947,8 @@ with_bot.coe_unbot x h
 @[simp] lemma untop_coe (x : α) (h : (x : with_top α) ≠ ⊤ := coe_ne_top) :
   (x : with_top α).untop h = x := rfl
 
-instance : can_lift (with_top α) α :=
-{ coe := coe,
-  cond := λ r, r ≠ ⊤,
-  prf := λ x h, ⟨x.untop h, coe_untop _ _⟩ }
+instance can_lift : can_lift (with_top α) α coe (λ r, r ≠ ⊤) :=
+{ prf := λ x h, ⟨x.untop h, coe_untop _ _⟩ }
 
 section has_le
 variables [has_le α]

src/order/filter/basic.lean

@@ -1799,10 +1799,9 @@ end
 lemma map_comap_of_mem {f : filter β} {m : α → β} (hf : range m ∈ f) : (f.comap m).map m = f :=
 by rw [map_comap, inf_eq_left.2 (le_principal_iff.2 hf)]
 
-instance [can_lift α β] : can_lift (filter α) (filter β) :=
-{ coe := map can_lift.coe,
-  cond := λ f, ∀ᶠ x : α in f, can_lift.cond β x,
-  prf := λ f hf, ⟨comap can_lift.coe f, map_comap_of_mem $ hf.mono can_lift.prf⟩ }
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (filter α) (filter β) (map c) (λ f, ∀ᶠ x : α in f, p x) :=
+{ prf := λ f hf, ⟨comap c f, map_comap_of_mem $ hf.mono can_lift.prf⟩ }
 
 lemma comap_le_comap_iff {f g : filter β} {m : α → β} (hf : range m ∈ f) :
   comap m f ≤ comap m g ↔ f ≤ g :=

src/order/hom/basic.lean

@@ -175,10 +175,8 @@ lemma ext (f g : α →o β) (h : (f : α → β) = g) : f = g := fun_like.coe_i
 lemma coe_eq (f : α →o β) : coe f = f := by ext ; refl
 
 /-- One can lift an unbundled monotone function to a bundled one. -/
-instance : can_lift (α → β) (α →o β) :=
-{ coe := coe_fn,
-  cond := monotone,
-  prf := λ f h, ⟨⟨f, h⟩, rfl⟩ }
+instance : can_lift (α → β) (α →o β) coe_fn monotone :=
+{ prf := λ f h, ⟨⟨f, h⟩, rfl⟩ }
 
 /-- Copy of an `order_hom` with a new `to_fun` equal to the old one. Useful to fix definitional
 equalities. -/

src/order/interval.lean

@@ -169,7 +169,8 @@ section has_le
 variables [has_le α] {s t : interval α}
 
 instance : has_coe_t (nonempty_interval α) (interval α) := with_bot.has_coe_t
-instance : can_lift (interval α) (nonempty_interval α) := with_bot.can_lift
+instance can_lift : can_lift (interval α) (nonempty_interval α) coe (λ r, r ≠ ⊥) :=
+with_bot.can_lift
 
 lemma coe_injective : injective (coe : nonempty_interval α → interval α) := with_bot.coe_injective
 @[simp, norm_cast] lemma coe_inj {s t : nonempty_interval α} : (s : interval α) = t ↔ s = t :=