chore(data/finset): rename ext/ext'/ext_iff (#3069)

Now

* `ext` is the `@[ext]` lemma;
* `ext_iff` is the lemma `s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂`.

Also add 2 `norm_cast` attributes and a lemma `ssubset_iff_of_subset`.

src/algebra/big_operators.lean

@@ -850,12 +850,12 @@ theorem card_eq_sum_card_image [decidable_eq β] (f : α → β) (s : finset α)
   s.card = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :=
 by letI := classical.dec_eq α; exact
 calc s.card = ((s.image f).bind (λ a, s.filter (λ x, f x = a))).card :
-  congr_arg _ (finset.ext.2 $ λ x,
+  congr_arg _ (finset.ext $ λ x,
     ⟨λ hs, mem_bind.2 ⟨f x, mem_image_of_mem _ hs,
       mem_filter.2 ⟨hs, rfl⟩⟩,
     λ h, let ⟨a, ha₁, ha₂⟩ := mem_bind.1 h in by convert filter_subset s ha₂⟩)
 ... = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :
-  card_bind (by simp [disjoint_left, finset.ext] {contextual := tt})
+  card_bind (by simp [disjoint_left, finset.ext_iff] {contextual := tt})
 
 lemma gsmul_sum [add_comm_group β] {f : α → β} {s : finset α} (z : ℤ) :
   gsmul z (∑ a in s, f a) = ∑ a in s, gsmul z (f a) :=
@@ -972,7 +972,7 @@ calc ∏ a in s, (f a + g a)
         _ _ _
         (λ b hb, ⟨b, by cases b; finish⟩));
     intros; simp * at *; simp * at * },
-  { finish [function.funext_iff, finset.ext, subset_iff] },
+  { finish [function.funext_iff, finset.ext_iff, subset_iff] },
   { assume f hf,
     exact ⟨s.filter (λ a : α, ∃ h : a ∈ s, f a h),
       by simp, by funext; intros; simp *⟩ }

src/data/complex/exponential.lean

@@ -218,7 +218,7 @@ begin
   rw [← sum_sdiff (@filter_subset _ (λ k, n ≤ k) _ (range m)),
     sub_eq_iff_eq_add, ← eq_sub_iff_add_eq, add_sub_cancel'],
   refine finset.sum_congr
-    (finset.ext.2 $ λ a, ⟨λ h, by simp at *; finish,
+    (finset.ext $ λ a, ⟨λ h, by simp at *; finish,
     λ h, have ham : a < m := lt_of_lt_of_le (mem_range.1 h) hnm,
       by simp * at *⟩)
     (λ _ _, rfl),

src/data/dfinsupp.lean

@@ -498,7 +498,7 @@ lemma mem_support_iff (f : Π₀ i, β i) : ∀i:ι, i ∈ f.support ↔ f i ≠
 f.mem_support_to_fun
 
 @[simp] lemma support_eq_empty {f : Π₀ i, β i} : f.support = ∅ ↔ f = 0 :=
-⟨λ H, ext $ by simpa [finset.ext] using H, by simp {contextual:=tt}⟩
+⟨λ H, ext $ by simpa [finset.ext_iff] using H, by simp {contextual:=tt}⟩
 
 instance decidable_zero : decidable_pred (eq (0 : Π₀ i, β i)) :=
 λ f, decidable_of_iff _ $ support_eq_empty.trans eq_comm

src/data/equiv/denumerable.lean

@@ -220,7 +220,7 @@ have h₁ : (of_nat s n : ℕ) ∉ (range (of_nat s n)).filter s, by simp,
 have h₂ : (range (succ (of_nat s n))).filter s =
     insert (of_nat s n) ((range (of_nat s n)).filter s),
   begin
-    simp only [finset.ext, mem_insert, mem_range, mem_filter],
+    simp only [finset.ext_iff, mem_insert, mem_range, mem_filter],
     assume m,
     exact ⟨λ h, by simp only [h.2, and_true]; exact or.symm
         (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),

src/data/finmap.lean

@@ -333,7 +333,7 @@ induction_on₂ s₁ s₂ $ λ _ _, mem_union
 by simp [(∪), union]
 
 theorem keys_union {s₁ s₂ : finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys :=
-induction_on₂ s₁ s₂ $ λ s₁ s₂, finset.ext' $ by simp [keys]
+induction_on₂ s₁ s₂ $ λ s₁ s₂, finset.ext $ by simp [keys]
 
 @[simp] theorem lookup_union_left {a} {s₁ s₂ : finmap β} :
   a ∈ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₁ :=

src/data/finsupp.lean

@@ -94,7 +94,7 @@ lemma ext_iff {f g : α →₀ β} : f = g ↔ (∀a:α, f a = g a) :=
 ⟨by rintros rfl a; refl, ext⟩
 
 @[simp] lemma support_eq_empty {f : α →₀ β} : f.support = ∅ ↔ f = 0 :=
-⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext.1 h a).1 $
+⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext_iff.1 h a).1 $
   mem_support_iff.2 H, by rintro rfl; refl⟩
 
 instance finsupp.decidable_eq [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
@@ -945,7 +945,7 @@ lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid
    comap_domain f l hf.inj_on = 0 → l = 0 :=
 begin
   rw [← support_eq_empty, ← support_eq_empty, comap_domain],
-  simp only [finset.ext, finset.not_mem_empty, iff_false, mem_preimage],
+  simp only [finset.ext_iff, finset.not_mem_empty, iff_false, mem_preimage],
   assume h a ha,
   cases hf.2.2 ha with b hb,
   exact h b (hb.2.symm ▸ ha)
@@ -985,7 +985,7 @@ if_pos h
 if_neg h
 
 @[simp] lemma support_filter : (f.filter p).support = f.support.filter p :=
-finset.ext.mpr $ assume a, if H : p a
+finset.ext $ assume a, if H : p a
 then by simp only [mem_support_iff, filter_apply_pos _ _ H, mem_filter, H, and_true]
 else by simp only [mem_support_iff, filter_apply_neg _ _ H, mem_filter, H, and_false, ne.def,
   ne_self_iff_false]
@@ -1580,7 +1580,7 @@ def split_comp [has_zero γ] (g : Π i, (αs i →₀ β) → γ)
   end }
 
 lemma sigma_support : l.support = l.split_support.sigma (λ i, (l.split i).support) :=
-by simp only [finset.ext, split_support, split, comap_domain, mem_image,
+by simp only [finset.ext_iff, split_support, split, comap_domain, mem_image,
   mem_preimage, sigma.forall, mem_sigma]; tauto
 
 lemma sigma_sum [add_comm_monoid γ] (f : (Σ (i : ι), αs i) → β → γ) :

src/data/fintype/basic.lean

@@ -37,10 +37,10 @@ by ext; simp
 theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 
 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
-by simp [ext]
+by simp [ext_iff]
 
 @[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
-  univ ∩ s = s := ext' $ λ a, by simp
+  univ ∩ s = s := ext $ λ a, by simp
 
 @[simp] lemma inter_univ [decidable_eq α] (s : finset α) :
   s ∩ univ = s :=
@@ -154,7 +154,7 @@ equiv.of_bijective (mono_of_fin univ h) begin
 end
 
 instance (α : Type*) : subsingleton (fintype α) :=
-⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext, h₁, h₂]⟩
+⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext_iff, h₁, h₂]⟩
 
 protected def subtype {p : α → Prop} (s : finset α)
   (H : ∀ x : α, x ∈ s ↔ p x) : fintype {x // p x} :=
@@ -840,7 +840,7 @@ by rw [perms_of_list, list.nodup_append, list.nodup_bind, pairwise_iff_nth_le];
 def perms_of_finset (s : finset α) : finset (perm α) :=
 quotient.hrec_on s.1 (λ l hl, ⟨perms_of_list l, nodup_perms_of_list hl⟩)
   (λ a b hab, hfunext (congr_arg _ (quotient.sound hab))
-    (λ ha hb _, heq_of_eq $ finset.ext.2 $
+    (λ ha hb _, heq_of_eq $ finset.ext $
       by simp [mem_perms_of_list_iff, hab.mem_iff]))
   s.2
 

src/data/fintype/card.lean

@@ -215,7 +215,7 @@ begin
   resetI,
   subst p,
   congr,
-  simp [finset.ext]
+  simp [finset.ext_iff]
 end
 
 @[to_additive] lemma finset.prod_fiberwise [fintype β] [decidable_eq β] [comm_monoid γ]
@@ -258,7 +258,7 @@ begin
   rw [← prod_sdiff (subset_univ s),
       ← @prod_image (α₁ ⊕ α₂) _ _ _ _ _ _ sum.inl,
       ← @prod_image (α₁ ⊕ α₂) _ _ _ _ _ _ sum.inr],
-  { congr, rw finset.ext, rintro (a|a);
+  { congr, rw finset.ext_iff, rintro (a|a);
     { simp only [mem_image, exists_eq, mem_sdiff, mem_univ, exists_false,
         exists_prop_of_true, not_false_iff, and_self, not_true, and_false], } },
   all_goals { intros, solve_by_elim [sum.inl.inj, sum.inr.inj], }

src/data/nat/multiplicity.lean

@@ -33,7 +33,7 @@ lemma multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm1 : m ≠ 1) (hn0 : 0 < n) (
 calc multiplicity m n = ↑(Ico 1 $ ((multiplicity m n).get (finite_nat_iff.2 ⟨hm1, hn0⟩) + 1)).card :
   by simp
 ... = ↑((finset.Ico 1 b).filter (λ i, m ^ i ∣ n)).card : congr_arg coe $ congr_arg card $
-  finset.ext.2 $ λ i,
+  finset.ext $ λ i,
   have hmn : ¬ m ^ n ∣ n,
     from if hm0 : m = 0
     then λ _, by cases n; simp [*, lt_irrefl, nat.pow_succ] at *

src/data/nat/totient.lean

@@ -65,7 +65,7 @@ calc ∑ m in (range n.succ).filter (∣ n), φ m
 ... = ((filter (∣ n) (range n.succ)).bind (λ d, (range n).filter (λ m, gcd n m = d))).card :
   (card_bind (by intros; apply disjoint_filter.2; cc)).symm
 ... = (range n).card :
-  congr_arg card (finset.ext.2 (λ m, ⟨by finish,
+  congr_arg card (finset.ext (λ m, ⟨by finish,
     λ hm, have h : m < n, from mem_range.1 hm,
       mem_bind.2 ⟨gcd n m, mem_filter.2 ⟨mem_range.2 (lt_succ_of_le (le_of_dvd (lt_of_le_of_lt (nat.zero_le _) h)
         (gcd_dvd_left _ _))), gcd_dvd_left _ _⟩, mem_filter.2 ⟨hm, rfl⟩⟩⟩))

src/data/set/basic.lean

@@ -205,6 +205,9 @@ not_subset.1 h.2
 lemma ssubset_iff_subset_ne {s t : set α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t :=
 by split; simp [set.ssubset_def, ne.def, set.subset.antisymm_iff] {contextual := tt}
 
+lemma ssubset_iff_of_subset {s t : set α} (h : s ⊆ t) : s ⊂ t ↔ ∃ x ∈ t, x ∉ s :=
+⟨exists_of_ssubset, λ ⟨x, hxt, hxs⟩, ⟨h, λ h, hxs $ h hxt⟩⟩
+
 theorem not_mem_empty (x : α) : ¬ (x ∈ (∅ : set α)) :=
 assume h : x ∈ ∅, h
 

src/data/set/finite.lean

@@ -126,7 +126,7 @@ end
 
 lemma to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : finite s) :
   (finite_insert a hs).to_finset = insert a hs.to_finset :=
-finset.ext.mpr $ by simp
+finset.ext $ by simp
 
 @[elab_as_eliminator]
 theorem finite.induction_on {C : set α → Prop} {s : set α} (h : finite s)

src/field_theory/finite.lean

@@ -53,7 +53,7 @@ lemma card_image_polynomial_eval [fintype R] [decidable_eq R] {p : polynomial R}
   fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
 finset.card_le_mul_card_image _ _
   (λ a _, calc _ = (p - C a).roots.card : congr_arg card
-    (by simp [finset.ext, mem_roots_sub_C hp, -sub_eq_add_neg])
+    (by simp [finset.ext_iff, mem_roots_sub_C hp, -sub_eq_add_neg])
     ... ≤ _ : card_roots_sub_C' hp)
 
 /-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution. -/

src/group_theory/order_of_element.lean

@@ -161,7 +161,7 @@ lemma sum_card_order_of_eq_card_pow_eq_one {n : ℕ} (hn : 0 < n) :
   = (finset.univ.filter (λ a : α, a ^ n = 1)).card :=
 calc ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ a : α, order_of a = m)).card
     = _ : (finset.card_bind (by { intros, apply finset.disjoint_filter.2, cc })).symm
-... = _ : congr_arg finset.card (finset.ext.2 (begin
+... = _ : congr_arg finset.card (finset.ext (begin
   assume a,
   suffices : order_of a ≤ n ∧ order_of a ∣ n ↔ a ^ n = 1,
   { simpa [nat.lt_succ_iff], },
@@ -443,7 +443,7 @@ have h : ∑ m in (range d.succ).filter (∣ d.succ),
             nat.div_div_self hm (succ_pos _)]⟩⟩)),
 have hinsert : insert d.succ ((range d.succ).filter (∣ d.succ))
     = (range d.succ.succ).filter (∣ d.succ),
-  from (finset.ext.2 $ λ x, ⟨λ h, (mem_insert.1 h).elim (λ h, by simp [h, range_succ])
+  from (finset.ext $ λ x, ⟨λ h, (mem_insert.1 h).elim (λ h, by simp [h, range_succ])
     (by clear _let_match; simp [range_succ]; tauto), by clear _let_match; simp [range_succ] {contextual := tt}; tauto⟩),
 have hinsert₁ : d.succ ∉ (range d.succ).filter (∣ d.succ),
   by simp [mem_range, zero_le_one, le_succ],
@@ -471,15 +471,15 @@ let c := fintype.card α in
 have hc0 : 0 < c, from fintype.card_pos_iff.2 ⟨1⟩,
 lt_irrefl c $
   calc c = (univ.filter (λ a : α, a ^ c = 1)).card :
-    congr_arg card $ by simp [finset.ext, c]
+    congr_arg card $ by simp [finset.ext_iff, c]
   ... = ∑ m in (range c.succ).filter (∣ c),
       (univ.filter (λ a : α, order_of a = m)).card :
     (sum_card_order_of_eq_card_pow_eq_one hc0).symm
   ... = ∑ m in ((range c.succ).filter (∣ c)).erase d,
       (univ.filter (λ a : α, order_of a = m)).card :
     eq.symm (sum_subset (erase_subset _ _) (λ m hm₁ hm₂,
       have m = d, by simp at *; cc,
-      by simp [*, finset.ext] at *; exact h0))
+      by simp [*, finset.ext_iff] at *; exact h0))
   ... ≤ ∑ m in ((range c.succ).filter (∣ c)).erase d, φ m :
     sum_le_sum (λ m hm,
       have hmc : m ∣ c, by simp at hm; tauto,

src/group_theory/perm/sign.lean

@@ -191,7 +191,7 @@ end
 lemma support_swap_mul_eq [fintype α] {f : perm α} {x : α}
   (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
 have hfx : f x ≠ x, from λ hfx, by simpa [hfx] using hffx,
-finset.ext.2 $ λ y,
+finset.ext $ λ y,
 ⟨λ hy, have hy' : (swap x (f x) * f) y ≠ y, from mem_support.1 hy,
     mem_erase.2 ⟨λ hyx, by simp [hyx, mul_apply, *] at *,
     mem_support.2 $ λ hfy,
@@ -666,11 +666,11 @@ lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
   is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
 
 @[simp] lemma support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
-finset.ext.2 $ λ a, by simp [swap_apply_def]; split_ifs; cc
+finset.ext $ λ a, by simp [swap_apply_def]; split_ifs; cc
 
 lemma card_support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
 show (swap x y).support.card = finset.card ⟨x::y::0, by simp [hxy]⟩,
-from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext]; cc
+from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext_iff]; cc
 
 lemma sign_cycle [fintype α] : ∀ {f : perm α} (hf : is_cycle f),
   sign f = -(-1) ^ f.support.card

src/linear_algebra/basis.lean

@@ -1138,8 +1138,7 @@ assume t, finset.induction_on t
           hsu, by simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
 begin
   have eq : t.filter (λx, x ∈ s) ∪ t.filter (λx, x ∉ s) = t,
-  { apply finset.ext.mpr,
-    intro x,
+  { ext1 x,
     by_cases x ∈ s; simp * },
   apply exists.elim (this (t.filter (λx, x ∉ s)) (t.filter (λx, x ∈ s))
     (by simp [set.subset_def]) (by simp [set.ext_iff] {contextual := tt}) (by rwa [eq])),

src/measure_theory/outer_measure.lean

@@ -86,12 +86,12 @@ begin
     rwa [← e, mem_decode2.1 (option.get_mem (H m hm))] at this },
   { intros b h,
     refine ⟨encode b, _, _⟩,
-    { convert h, simp [ext_iff, encodek2] },
+    { convert h, simp [set.ext_iff, encodek2] },
     { exact option.get_of_mem _ (encodek2 _) } },
   { intros n h,
     transitivity, swap,
     rw [show decode2 β n = _, from option.get_mem (H n h)],
-    congr, simp [ext_iff, -option.some_get] }
+    congr, simp [set.ext_iff, -option.some_get] }
 end
 
 protected theorem Union (m : outer_measure α)

src/number_theory/quadratic_reciprocity.lean

@@ -281,7 +281,7 @@ lemma div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) : a / b
   ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :=
 calc a / b = (Ico 1 (a / b).succ).card : by simp
 ... = ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :
-  congr_arg _$ finset.ext.2 $ λ x,
+  congr_arg _ $ finset.ext $ λ x,
     have x * b ≤ a → x ≤ c,
       from λ h, le_trans (by rwa [le_div_iff_mul_le _ _ hb0]) hc,
     by simp [lt_succ_iff, le_div_iff_mul_le _ _ hb0]; tauto
@@ -292,7 +292,7 @@ private lemma sum_Ico_eq_card_lt {p q : ℕ} :
   ∑ a in Ico 1 (p / 2).succ, (a * q) / p =
   (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
   (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q)).card :=
-if hp0 : p = 0 then by simp [hp0, finset.ext]
+if hp0 : p = 0 then by simp [hp0, finset.ext_iff]
 else
   calc ∑ a in Ico 1 (p / 2).succ, (a * q) / p =
     ∑ a in Ico 1 (p / 2).succ,
@@ -348,7 +348,7 @@ have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
     ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
       (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p) =
     ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)),
-  from finset.ext.2 $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
+  from finset.ext $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
 by rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
     card_product];
   simp

src/topology/metric_space/emetric_space.lean

@@ -494,12 +494,12 @@ instance emetric_space_pi [∀b, emetric_space (π b)] : emetric_space (Πb, π
     end,
   to_uniform_space := Pi.uniform_space _,
   uniformity_edist := begin
-    simp only [Pi.uniformity, emetric_space.uniformity_edist, comap_infi, gt_iff_lt, preimage_set_of_eq,
-          comap_principal],
+    simp only [Pi.uniformity, emetric_space.uniformity_edist, comap_infi, gt_iff_lt,
+      preimage_set_of_eq, comap_principal],
     rw infi_comm, congr, funext ε,
     rw infi_comm, congr, funext εpos,
     change 0 < ε at εpos,
-    simp [ext_iff, εpos]
+    simp [set.ext_iff, εpos]
   end }
 
 end pi