chore(data/finset/basic): use has_coe_t for coercion of finset to set (#4917)

Author: urkud

src/data/finset/basic.lean

@@ -64,20 +64,20 @@ multiset.decidable_mem _ _
 /-! ### set coercion -/
 
 /-- Convert a finset to a set in the natural way. -/
-instance : has_lift (finset α) (set α) := ⟨λ s, {x | x ∈ s}⟩
+instance : has_coe_t (finset α) (set α) := ⟨λ s, {x | x ∈ s}⟩
 
-@[simp, norm_cast] lemma mem_coe {a : α} {s : finset α} : a ∈ (↑s : set α) ↔ a ∈ s := iff.rfl
+@[simp, norm_cast] lemma mem_coe {a : α} {s : finset α} : a ∈ (s : set α) ↔ a ∈ s := iff.rfl
 
-@[simp] lemma set_of_mem {α} {s : finset α} : {a | a ∈ s} = ↑s := rfl
+@[simp] lemma set_of_mem {α} {s : finset α} : {a | a ∈ s} = s := rfl
 
-@[simp] lemma coe_mem {s : finset α} (x : (↑s : set α)) : ↑x ∈ s := x.2
+@[simp] lemma coe_mem {s : finset α} (x : (s : set α)) : ↑x ∈ s := x.2
 
-@[simp] lemma mk_coe {s : finset α} (x : (↑s : set α)) {h} :
-  (⟨↑x, h⟩ : (↑s : set α)) = x :=
-by { apply subtype.eq, refl, }
+@[simp] lemma mk_coe {s : finset α} (x : (s : set α)) {h} :
+  (⟨x, h⟩ : (s : set α)) = x :=
+subtype.coe_eta _ _
 
 instance decidable_mem' [decidable_eq α] (a : α) (s : finset α) :
-  decidable (a ∈ (↑s : set α)) := s.decidable_mem _
+  decidable (a ∈ (s : set α)) := s.decidable_mem _
 
 /-! ### extensionality -/
 theorem ext_iff {s₁ s₂ : finset α} : s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂ :=
@@ -87,7 +87,7 @@ val_inj.symm.trans $ nodup_ext s₁.2 s₂.2
 theorem ext {s₁ s₂ : finset α} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ :=
 ext_iff.2
 
-@[simp, norm_cast] theorem coe_inj {s₁ s₂ : finset α} : (↑s₁ : set α) = ↑s₂ ↔ s₁ = s₂ :=
+@[simp, norm_cast] theorem coe_inj {s₁ s₂ : finset α} : (s₁ : set α) = s₂ ↔ s₁ = s₂ :=
 set.ext_iff.trans ext_iff.symm
 
 lemma coe_injective {α} : function.injective (coe : finset α → set α) :=
@@ -119,7 +119,7 @@ ext $ λ a, ⟨@H₁ a, @H₂ a⟩
 theorem subset_iff {s₁ s₂ : finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x⦄, x ∈ s₁ → x ∈ s₂ := iff.rfl
 
 @[simp, norm_cast] theorem coe_subset {s₁ s₂ : finset α} :
-  (↑s₁ : set α) ⊆ ↑s₂ ↔ s₁ ⊆ s₂ := iff.rfl
+  (s₁ : set α) ⊆ s₂ ↔ s₁ ⊆ s₂ := iff.rfl
 
 @[simp] theorem val_le_iff {s₁ s₂ : finset α} : s₁.1 ≤ s₂.1 ↔ s₁ ⊆ s₂ := le_iff_subset s₁.2
 
@@ -138,8 +138,8 @@ le_antisymm_iff
 @[simp] theorem le_iff_subset {s₁ s₂ : finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂ := iff.rfl
 @[simp] theorem lt_iff_ssubset {s₁ s₂ : finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂ := iff.rfl
 
-@[simp, norm_cast] lemma coe_ssubset {s₁ s₂ : finset α} : (↑s₁ : set α) ⊂ ↑s₂ ↔ s₁ ⊂ s₂ :=
-show (↑s₁ : set α) ⊂ ↑s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁,
+@[simp, norm_cast] lemma coe_ssubset {s₁ s₂ : finset α} : (s₁ : set α) ⊂ s₂ ↔ s₁ ⊂ s₂ :=
+show (s₁ : set α) ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁,
   by simp only [set.ssubset_def, finset.coe_subset]
 
 @[simp] theorem val_lt_iff {s₁ s₂ : finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
@@ -155,7 +155,7 @@ in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives ac
 to the dot notation. -/
 protected def nonempty (s : finset α) : Prop := ∃ x:α, x ∈ s
 
-@[simp, norm_cast] lemma coe_nonempty {s : finset α} : (↑s:set α).nonempty ↔ s.nonempty := iff.rfl
+@[simp, norm_cast] lemma coe_nonempty {s : finset α} : (s:set α).nonempty ↔ s.nonempty := iff.rfl
 
 lemma nonempty.bex {s : finset α} (h : s.nonempty) : ∃ x:α, x ∈ s := h
 
@@ -207,7 +207,7 @@ theorem nonempty_iff_ne_empty {s : finset α} : s.nonempty ↔ s ≠ ∅ :=
 theorem eq_empty_or_nonempty (s : finset α) : s = ∅ ∨ s.nonempty :=
 classical.by_cases or.inl (λ h, or.inr (nonempty_of_ne_empty h))
 
-@[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl
+@[simp] lemma coe_empty : ((∅ : finset α) : set α) = ∅ := rfl
 
 /-- A `finset` for an empty type is empty. -/
 lemma eq_empty_of_not_nonempty (h : ¬ nonempty α) (s : finset α) : s = ∅ :=
@@ -236,7 +236,8 @@ theorem singleton_nonempty (a : α) : ({a} : finset α).nonempty := ⟨a, mem_si
 
 @[simp] theorem singleton_ne_empty (a : α) : ({a} : finset α) ≠ ∅ := (singleton_nonempty a).ne_empty
 
-@[simp] lemma coe_singleton (a : α) : ↑({a} : finset α) = ({a} : set α) := by { ext, simp }
+@[simp, norm_cast] lemma coe_singleton (a : α) : (({a} : finset α) : set α) = {a} :=
+by { ext, simp }
 
 lemma eq_singleton_iff_unique_mem {s : finset α} {a : α} :
   s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a :=
@@ -324,7 +325,7 @@ theorem mem_of_mem_insert_of_ne {a b : α} {s : finset α} (h : b ∈ insert a s
 ext $ λ a, by simp
 
 @[simp, norm_cast] lemma coe_insert (a : α) (s : finset α) :
-  ↑(insert a s) = (insert a ↑s : set α) :=
+  ↑(insert a s) = (insert a s : set α) :=
 set.ext $ λ x, by simp only [mem_coe, mem_insert, set.mem_insert_iff]
 
 instance : is_lawful_singleton α (finset α) := ⟨λ a, by { ext, simp }⟩
@@ -364,7 +365,7 @@ theorem insert_subset_insert (a : α) {s t : finset α} (h : s ⊆ t) : insert a
 insert_subset.2 ⟨mem_insert_self _ _, subset.trans h (subset_insert _ _)⟩
 
 lemma ssubset_iff {s t : finset α} : s ⊂ t ↔ (∃a ∉ s, insert a s ⊆ t) :=
-by exact_mod_cast @set.ssubset_iff_insert α ↑s ↑t
+by exact_mod_cast @set.ssubset_iff_insert α s t
 
 lemma ssubset_insert {s : finset α} {a : α} (h : a ∉ s) : s ⊂ insert a s :=
 ssubset_iff.mpr ⟨a, h, subset.refl _⟩
@@ -432,7 +433,7 @@ theorem not_mem_union {a : α} {s₁ s₂ : finset α} : a ∉ s₁ ∪ s₂ ↔
 by rw [mem_union, not_or_distrib]
 
 @[simp, norm_cast]
-lemma coe_union (s₁ s₂ : finset α) : ↑(s₁ ∪ s₂) = (↑s₁ ∪ ↑s₂ : set α) := set.ext $ λ x, mem_union
+lemma coe_union (s₁ s₂ : finset α) : ↑(s₁ ∪ s₂) = (s₁ ∪ s₂ : set α) := set.ext $ λ x, mem_union
 
 theorem union_subset {s₁ s₂ s₃ : finset α} (h₁ : s₁ ⊆ s₃) (h₂ : s₂ ⊆ s₃) : s₁ ∪ s₂ ⊆ s₃ :=
 val_le_iff.1 (ndunion_le.2 ⟨h₁, val_le_iff.2 h₂⟩)
@@ -538,7 +539,7 @@ theorem subset_inter {s₁ s₂ s₃ : finset α} : s₁ ⊆ s₂ → s₁ ⊆ s
 by simp only [subset_iff, mem_inter] {contextual:=tt}; intros; split; trivial
 
 @[simp, norm_cast]
-lemma coe_inter (s₁ s₂ : finset α) : ↑(s₁ ∩ s₂) = (↑s₁ ∩ ↑s₂ : set α) := set.ext $ λ _, mem_inter
+lemma coe_inter (s₁ s₂ : finset α) : ↑(s₁ ∩ s₂) = (s₁ ∩ s₂ : set α) := set.ext $ λ _, mem_inter
 
 @[simp] theorem union_inter_cancel_left {s t : finset α} : (s ∪ t) ∩ s = s :=
 by rw [← coe_inj, coe_inter, coe_union, set.union_inter_cancel_left]
@@ -697,7 +698,7 @@ val_le_iff.1 $ erase_le_erase _ $ val_le_iff.2 h
 
 theorem erase_subset (a : α) (s : finset α) : erase s a ⊆ s := erase_subset _ _
 
-@[simp, norm_cast] lemma coe_erase (a : α) (s : finset α) : ↑(erase s a) = (↑s \ {a} : set α) :=
+@[simp, norm_cast] lemma coe_erase (a : α) (s : finset α) : ↑(erase s a) = (s \ {a} : set α) :=
 set.ext $ λ _, mem_erase.trans $ by rw [and_comm, set.mem_diff, set.mem_singleton_iff]; refl
 
 lemma erase_ssubset {a : α} {s : finset α} (h : a ∈ s) : s.erase a ⊂ s :=
@@ -776,7 +777,7 @@ theorem sdiff_subset_self {s₁ s₂ : finset α} : s₁ \ s₂ ⊆ s₁ :=
 suffices s₁ \ s₂ ⊆ s₁ \ ∅, by simpa [sdiff_empty] using this,
 sdiff_subset_sdiff (subset.refl _) (empty_subset _)
 
-@[simp, norm_cast] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (↑s₁ \ ↑s₂ : set α) :=
+@[simp, norm_cast] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : set α) :=
 set.ext $ λ _, mem_sdiff
 
 @[simp] theorem union_sdiff_self_eq_union {s t : finset α} : s ∪ (t \ s) = s ∪ t :=
@@ -805,14 +806,14 @@ lemma insert_sdiff_of_not_mem (s : finset α) {t : finset α} {x : α} (h : x 
   (insert x s) \ t = insert x (s \ t) :=
 begin
   rw [← coe_inj, coe_insert, coe_sdiff, coe_sdiff, coe_insert],
-  exact set.insert_diff_of_not_mem ↑s h
+  exact set.insert_diff_of_not_mem s h
 end
 
 lemma insert_sdiff_of_mem (s : finset α) {t : finset α} {x : α} (h : x ∈ t) :
   (insert x s) \ t = s \ t :=
 begin
   rw [← coe_inj, coe_sdiff, coe_sdiff, coe_insert],
-  exact set.insert_diff_of_mem ↑s h
+  exact set.insert_diff_of_mem s h
 end
 
 @[simp] lemma insert_sdiff_insert (s t : finset α) (x : α) :
@@ -887,8 +888,8 @@ by { ext i, simp [piecewise] }
 
 variable [∀j, decidable (j ∈ s)]
 
-@[norm_cast] lemma piecewise_coe [∀j, decidable (j ∈ (↑s : set α))] :
-  (↑s : set α).piecewise f g = s.piecewise f g :=
+@[norm_cast] lemma piecewise_coe [∀j, decidable (j ∈ (s : set α))] :
+  (s : set α).piecewise f g = s.piecewise f g :=
 by { ext, congr }
 
 @[simp, priority 980]

src/data/polynomial/monic.lean

@@ -143,7 +143,7 @@ lemma coeff_nat_degree {p : polynomial R} (hp : p.monic) : p.coeff (p.nat_degree
 
 @[simp]
 lemma degree_eq_zero_iff_eq_one {p : polynomial R} (hp : p.monic) :
-p.nat_degree = 0 ↔ p = 1 :=
+  p.nat_degree = 0 ↔ p = 1 :=
 begin
   split; intro h,
   swap, { rw h, exact nat_degree_one },
@@ -158,41 +158,37 @@ lemma nat_degree_mul [nontrivial R] {p q : polynomial R} (hp : p.monic) (hq : q.
 by { apply nat_degree_mul', rw [hp.leading_coeff, hq.leading_coeff], simp }
 
 lemma next_coeff_mul {p q : polynomial R} (hp : monic p) (hq : monic q) :
-next_coeff (p * q) = next_coeff p + next_coeff q :=
+  next_coeff (p * q) = next_coeff p + next_coeff q :=
 begin
-  nontriviality,
-  dsimp only [next_coeff],
-  simp only [monic.nat_degree_mul hp hq, add_eq_zero_iff, degree_eq_zero_iff_eq_one, hp, hq],
-  by_cases hp0 : p = 1; by_cases hq0 : q = 1;
-  simp only [hp0, hq0, true_and, and_true, false_and, one_mul, mul_one, if_true, if_false,
-    add_zero, zero_add, nat.zero_sub, nat_degree_one, coeff_one_zero, eq_self_iff_true],
-  simp only [← degree_eq_zero_iff_eq_one, hp, hq] at hp0 hq0,
-  -- we've reduced to the case where the degrees of p and q are nonzero
+  classical,
+  nontriviality R,
+  simp only [next_coeff, monic.nat_degree_mul hp hq],
+  simp only [hp, hq, degree_eq_zero_iff_eq_one, add_eq_zero_iff],
   set dp := p.nat_degree, set dq := q.nat_degree,
+  suffices : p ≠ 1 → q ≠ 1 → (p * q).coeff (dp + dq - 1) = p.coeff (dp - 1) + q.coeff (dq - 1),
+  { by_cases hp0 : p = 1; by_cases hq0 : q = 1; simp [dp, dq, hp0, hq0, this] },
+  intros hp0 hq0,
+  replace hp0 : dp ≠ 0 := mt hp.degree_eq_zero_iff_eq_one.1 hp0,
+  replace hq0 : dq ≠ 0 := mt hq.degree_eq_zero_iff_eq_one.1 hq0,
   rw coeff_mul,
-  have : {(dp, dq - 1), (dp - 1, dq)} ⊆ nat.antidiagonal (dp + dq - 1),
-  { simp only [insert_subset, singleton_subset_iff, nat.mem_antidiagonal],
-    split,
-    { rw nat.add_sub_assoc, exact nat.pos_of_ne_zero hq0 },
-    { apply nat.sub_add_eq_add_sub, exact nat.pos_of_ne_zero hp0 } },
-  rw ← sum_subset this; clear this,
-  { rw [sum_insert, sum_singleton],
-    { rw [coeff_nat_degree hp, coeff_nat_degree hq, mul_one, one_mul, add_comm] },
-    { simp only [not_and, prod.mk.inj_iff, mem_singleton], revert hp0, omega manual } },
-  simp only [prod.forall, mem_insert, prod.mk.inj_iff, nat.mem_antidiagonal, mem_singleton],
-  push_neg, rintros i j h1 ⟨h2, h3⟩,
-  suffices : p.coeff i = 0 ∨ q.coeff j = 0,
-  { exact mul_eq_zero_of_ne_zero_imp_eq_zero this.resolve_left },
-  suffices : dp < i ∨ dq < j, { apply this.imp _ _; exact coeff_eq_zero_of_nat_degree_lt },
-  rw or_iff_not_imp_left, push_neg, intro h,
-  have aux1 : i ≠ dp,
-  { intro hi, subst i,
-    rw nat.add_sub_assoc (nat.pos_of_ne_zero hq0) at h1,
-    exact h2 rfl (nat.add_left_cancel h1) },
-  rw nat.sub_add_comm (nat.pos_of_ne_zero hp0) at h1,
-  have aux2 : i ≠ dp - 1, { rintro rfl, exact h3 rfl (nat.add_left_cancel h1) },
-  have aux3 : i < dp - 1, { revert h aux1 aux2, omega manual },
-  revert aux3 h1, omega manual
+  have : {(dp - 1, dq), (dp, dq - 1)} ⊆ nat.antidiagonal (dp + dq - 1),
+  { suffices : dp - 1 + dq = dp + dq - 1 ∧ dp + (dq - 1) = dp + dq - 1,
+      by simpa [insert_subset, singleton_subset_iff],
+    omega },
+  rw [← sum_subset this, sum_pair],
+  { simp [hp, hq] },
+  { suffices : dp - 1 ≠ dp, from mt (congr_arg prod.fst) this,
+    omega },
+  { rintros ⟨x, y⟩ hx hx1,
+    simp only [nat.mem_antidiagonal] at hx,
+    simp only [mem_insert, mem_singleton] at hx1,
+    contrapose! hx1,
+    have hxp : x ≤ dp, from le_nat_degree_of_ne_zero (left_ne_zero_of_mul hx1),
+    have hyq : y ≤ dq, from le_nat_degree_of_ne_zero (right_ne_zero_of_mul hx1),
+    have : dq - 1 ≤ y, omega,
+    by_cases hy : y = dq,
+    { subst y, left, congr, omega },
+    { have : y = dq - 1, by omega, subst y, right, congr, omega } }
 end
 
 lemma next_coeff_prod