feat(*): small lemmas from the sensitivity formalization (#1352)

* feat(set_theory/cardinal): norm_cast attributes and extra lemma

* feat(logic/basic): ne.symm_iff

* feat(data/fin): succ_ne_zero

* feat(data/bool): bxor_of_ne

* feat(algebra/big_operators, data/fintype): {finset,fintype}.card_eq_sum_ones

* feat(data/set): range_restrict

* feat(data/finset): inter lemmas

* Reid's corrections

* fixes

* fix cardinal power lemma

* fixes

* Update bool.lean

Author: robertylewis

src/algebra/big_operators.lean

@@ -642,6 +642,10 @@ lemma sum_range_id (n : ℕ) : (finset.range n).sum (λi, i) = (n * (n - 1)) / 2
 by rw [← sum_range_id_mul_two n, nat.mul_div_cancel]; exact dec_trivial
 
 end gauss_sum
+
+lemma card_eq_sum_ones (s : finset α) : s.card = s.sum (λ _, 1) :=
+by simp
+
 end finset
 
 section group

src/data/bool.lean

@@ -115,4 +115,6 @@ theorem eq_ff_of_bnot_eq_tt : ∀ {a : bool}, bnot a = tt → a = ff := dec_triv
 
 @[simp] theorem bxor_left_comm : ∀ a b c, bxor a (bxor b c) = bxor b (bxor a c) := dec_trivial
 
+lemma bxor_iff_ne : ∀ {x y : bool}, bxor x y = tt ↔ x ≠ y := dec_trivial
+
 end bool

src/data/fin.lean

@@ -58,6 +58,9 @@ by cases j; simp [fin.succ]
 protected theorem succ.inj (p : fin.succ a = fin.succ b) : a = b :=
 by cases a; cases b; exact eq_of_veq (nat.succ.inj (veq_of_eq p))
 
+lemma succ_ne_zero {n} : ∀ k : fin n, fin.succ k ≠ 0
+| ⟨k, hk⟩ heq := nat.succ_ne_zero k $ (fin.ext_iff _ _).1 heq
+
 @[simp] lemma pred_val (j : fin (n+1)) (h : j ≠ 0) : (j.pred h).val = j.val.pred :=
 by cases j; simp [fin.pred]
 

src/data/finset.lean

@@ -401,6 +401,19 @@ by rw [inter_comm, singleton_inter_of_mem h]
 @[simp] theorem inter_singleton_of_not_mem {a : α} {s : finset α} (h : a ∉ s) : s ∩ ι a = ∅ :=
 by rw [inter_comm, singleton_inter_of_not_mem h]
 
+lemma inter_subset_inter {x y s t : finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ s ⊆ y ∩ t :=
+begin
+  intros a a_in,
+  rw finset.mem_inter at a_in ⊢,
+  exact ⟨h a_in.1, h' a_in.2⟩
+end
+
+lemma inter_subset_inter_right {x y s : finset α} (h : x ⊆ y) : x ∩ s ⊆ y ∩ s :=
+finset.inter_subset_inter h (finset.subset.refl _)
+
+lemma inter_subset_inter_left {x y s : finset α} (h : x ⊆ y) : s ∩ x ⊆ s ∩ y :=
+finset.inter_subset_inter (finset.subset.refl _) h
+
 /- lattice laws -/
 
 instance : lattice (finset α) :=

src/data/fintype.lean

@@ -161,21 +161,24 @@ theorem card_congr {α β} [fintype α] [fintype β] (f : α ≃ β) : card α =
 by rw ← of_equiv_card f; congr
 
 theorem card_eq {α β} [F : fintype α] [G : fintype β] : card α = card β ↔ nonempty (α ≃ β) :=
-⟨λ h, ⟨by classical; 
+⟨λ h, ⟨by classical;
   calc α ≃ fin (card α) : trunc.out (equiv_fin α)
      ... ≃ fin (card β) : by rw h
-     ... ≃ β : (trunc.out (equiv_fin β)).symm⟩, 
+     ... ≃ β : (trunc.out (equiv_fin β)).symm⟩,
 λ ⟨f⟩, card_congr f⟩
 
 def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 ⟨finset.singleton a, λ b, finset.mem_singleton.2 (subsingleton.elim _ _)⟩
 
-@[simp] theorem fintype.univ_of_subsingleton (a : α) [subsingleton α] :
+@[simp] theorem univ_of_subsingleton (a : α) [subsingleton α] :
   @univ _ (of_subsingleton a) = finset.singleton a := rfl
 
-@[simp] theorem fintype.card_of_subsingleton (a : α) [subsingleton α] :
+@[simp] theorem card_of_subsingleton (a : α) [subsingleton α] :
   @fintype.card _ (of_subsingleton a) = 1 := rfl
 
+lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
+finset.card_eq_sum_ones _
+
 end fintype
 
 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=
@@ -436,20 +439,20 @@ instance finset.fintype [fintype α] : fintype (finset α) :=
 instance subtype.fintype [fintype α] (p : α → Prop) [decidable_pred p] : fintype {x // p x} :=
 set_fintype _
 
-instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] : 
-  fintype (Σ' a, β a) := 
+instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
+  fintype (Σ' a, β a) :=
 fintype.of_equiv _ (equiv.psigma_equiv_sigma _).symm
 
-instance psigma.fintype_prop_left {α : Prop} {β : α → Type*} [∀ a, fintype (β a)] [decidable α] : 
+instance psigma.fintype_prop_left {α : Prop} {β : α → Type*} [∀ a, fintype (β a)] [decidable α] :
   fintype (Σ' a, β a) :=
-if h : α then fintype.of_equiv (β h) ⟨λ x, ⟨h, x⟩, psigma.snd, λ _, rfl, λ ⟨_, _⟩, rfl⟩ 
+if h : α then fintype.of_equiv (β h) ⟨λ x, ⟨h, x⟩, psigma.snd, λ _, rfl, λ ⟨_, _⟩, rfl⟩
 else ⟨∅, λ x, h x.1⟩
 
-instance psigma.fintype_prop_right {α : Type*} {β : α → Prop} [fintype α] [∀ a, decidable (β a)] : 
+instance psigma.fintype_prop_right {α : Type*} {β : α → Prop} [fintype α] [∀ a, decidable (β a)] :
   fintype (Σ' a, β a) :=
 fintype.of_equiv {a // β a} ⟨λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, rfl, λ ⟨x, y⟩, rfl⟩
 
-instance psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [∀ a, decidable (β a)] : 
+instance psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [∀ a, decidable (β a)] :
   fintype (Σ' a, β a) :=
 if h : ∃ a, β a then ⟨{⟨h.fst, h.snd⟩}, λ ⟨_, _⟩, by simp⟩ else ⟨∅, λ ⟨x, y⟩, h ⟨x, y⟩⟩
 

src/data/set/function.lean

@@ -292,4 +292,8 @@ theorem bij_on_of_inv_on {g : β → α} {f : α → β} {a : set α} {b : set 
   (h₂ : maps_to g b a) (h₃ : inv_on g f a b) : bij_on f a b :=
 ⟨h₁, inj_on_of_left_inv_on h₃.left, surj_on_of_right_inv_on h₂ h₃.right⟩
 
+lemma range_restrict {α : Type*} {β : Type*} (f : α → β) (p : set α) :
+  range (restrict f p) = f '' (p : set α) :=
+by { ext x, simp [restrict], refl }
+
 end set

src/logic/basic.lean

@@ -74,6 +74,8 @@ assume ⟨h⟩, h.elim
 -- missing [symm] attribute for ne in core.
 attribute [symm] ne.symm
 
+lemma ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨ne.symm, ne.symm⟩
+
 end miscellany
 
 /-

src/set_theory/cardinal.lean

@@ -212,6 +212,11 @@ by rw [_root_.mul_comm b c];
 from (quotient.induction_on₃ a b c $ assume α β γ,
   quotient.sound ⟨equiv.arrow_arrow_equiv_prod_arrow γ β α⟩)
 
+@[simp] lemma pow_cast_right (κ : cardinal.{u}) :
+  ∀ n : ℕ, (κ ^ (↑n : cardinal.{u})) = @has_pow.pow _ _ monoid.has_pow κ n
+| 0 := by simp
+| (_+1) := by rw [nat.cast_succ, power_add, power_one, _root_.mul_comm, pow_succ, pow_cast_right]
+
 section order_properties
 open sum
 
@@ -581,10 +586,10 @@ begin
   rw [cardinal.fintype_card, fintype.card_coe]
 end
 
-@[simp] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
+@[simp, elim_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
 by induction n; simp [nat.pow_succ, -_root_.add_comm, power_add, *]
 
-@[simp] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
+@[simp, elim_cast] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
 by rw [← lift_mk_fin, ← lift_mk_fin, lift_le]; exact
 ⟨λ ⟨⟨f, hf⟩⟩, begin
   have : _ = fintype.card _ := finset.card_image_of_injective finset.univ hf,
@@ -595,13 +600,13 @@ end,
 λ h, ⟨⟨λ i, ⟨i.1, lt_of_lt_of_le i.2 h⟩, λ a b h,
   have _, from fin.veq_of_eq h, fin.eq_of_veq this⟩⟩⟩
 
-@[simp] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
+@[simp, elim_cast] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
 by simp [lt_iff_le_not_le, -not_le]
 
-@[simp] theorem nat_cast_inj {m n : ℕ} : (m : cardinal) = n ↔ m = n :=
+@[simp, elim_cast] theorem nat_cast_inj {m n : ℕ} : (m : cardinal) = n ↔ m = n :=
 by simp [le_antisymm_iff]
 
-@[simp] theorem nat_succ (n : ℕ) : succ n = n.succ :=
+@[simp, elim_cast] theorem nat_succ (n : ℕ) : succ n = n.succ :=
 le_antisymm (succ_le.2 $ nat_cast_lt.2 $ nat.lt_succ_self _) (add_one_le_succ _)
 
 @[simp] theorem succ_zero : succ 0 = 1 :=