refactor(data/fin,*): redefine insert_nth, add lemmas (#9349)

### `data/fin`

* add `fin.succ_above_cast_lt`, `fin.succ_above_pred`,
  `fin.cast_lt_succ_above`, `fin.pred_succ_above`;
* add `fin.exists_succ_above_eq` and `fin.exists_succ_above_eq_iff`,
  use the latter to prove `fin.range_succ_above`;
* add `@[simp]` to `fin.succ_above_left_inj`;
* add `fin.cases_succ_above` induction principle, redefine
  `fin.insert_nth` to be `fin.cases_succ_above`;
* add lemmas about `fin.insert_nth` and some algebraic operations.

### `data/fintype/basic`

* add `finset.insert_compl_self`;
* add `fin.image_succ_above_univ`, `fin.image_succ_univ`,
  `fin.image_cast_succ` and use them to prove `fin.univ_succ`,
  `fin.univ_cast_succ`, and `fin.univ_succ_above` using `by simp`;

### `data/fintype/card`

* slightly golf the proof of `fin.prod_univ_succ_above`;
* use `@[to_additive]` to generate some proofs.

### `topology/*`

* prove continuity of `fin.insert_nth` in both arguments and add all
  the standard dot-notation `*.fin_insert_nth` lemmas (`*` is one of
  `filter.tendsto`, `continuous_at`, `continuous_within_at`,
  `continuous_on`, `continuous`).

Author: urkud

src/data/fin.lean

@@ -1137,28 +1137,43 @@ begin
   { simpa [succ_above_above _ _ (le_of_not_lt H)] using succ_pos _ },
 end
 
-/-- The range of `p.succ_above` is everything except `p`. -/
-lemma range_succ_above (p : fin (n + 1)) : set.range (p.succ_above) = { i | i ≠ p } :=
+@[simp] lemma succ_above_cast_lt {x y : fin (n + 1)} (h : x < y)
+  (hx : x.1 < n := lt_of_lt_of_le h y.le_last) :
+  y.succ_above (x.cast_lt hx) = x :=
+by { rw [succ_above_below, cast_succ_cast_lt], exact h }
+
+@[simp] lemma succ_above_pred {x y : fin (n + 1)} (h : x < y)
+  (hy : y ≠ 0 := (x.zero_le.trans_lt h).ne') :
+  x.succ_above (y.pred hy) = y :=
+by { rw [succ_above_above, succ_pred], simpa [le_iff_coe_le_coe] using nat.le_pred_of_lt h }
+
+lemma cast_lt_succ_above {x : fin n} {y : fin (n + 1)} (h : cast_succ x < y)
+  (h' : (y.succ_above x).1 < n := lt_of_lt_of_le ((succ_above_lt_iff _ _).2 h) (le_last y)) :
+  (y.succ_above x).cast_lt h' = x :=
+by simp only [succ_above_below _ _ h, cast_lt_cast_succ]
+
+lemma pred_succ_above {x : fin n} {y : fin (n + 1)} (h : y ≤ cast_succ x)
+  (h' : y.succ_above x ≠ 0 := (y.zero_le.trans_lt $ (lt_succ_above_iff _ _).2 h).ne') :
+  (y.succ_above x).pred h' = x :=
+by simp only [succ_above_above _ _ h, pred_succ]
+
+lemma exists_succ_above_eq {x y : fin (n + 1)} (h : x ≠ y) : ∃ z, y.succ_above z = x :=
 begin
-  ext,
-  simp only [set.mem_range, ne.def, set.mem_set_of_eq],
-  split,
-  { rintro ⟨y, rfl⟩,
-    exact succ_above_ne _ _ },
-  { intro h,
-    cases lt_or_gt_of_ne h with H H,
-    { refine ⟨x.cast_lt _, _⟩,
-      { exact lt_of_lt_of_le H p.le_last },
-      { rw succ_above_below,
-        { simp },
-        { exact H } } },
-    { refine ⟨x.pred _, _⟩,
-      { exact (ne_of_lt (lt_of_le_of_lt p.zero_le H)).symm },
-      { rw succ_above_above,
-        { simp },
-        { simpa [le_iff_coe_le_coe] using nat.le_pred_of_lt H } } } }
+  cases h.lt_or_lt with hlt hlt,
+  exacts [⟨_, succ_above_cast_lt hlt⟩, ⟨_, succ_above_pred hlt⟩],
+end
+
+@[simp] lemma exists_succ_above_eq_iff {x y : fin (n + 1)} : (∃ z, x.succ_above z = y) ↔ y ≠ x :=
+begin
+  refine ⟨_, exists_succ_above_eq⟩,
+  rintro ⟨y, rfl⟩,
+  exact succ_above_ne _ _
 end
 
+/-- The range of `p.succ_above` is everything except `p`. -/
+@[simp] lemma range_succ_above (p : fin (n + 1)) : set.range (p.succ_above) = {p}ᶜ :=
+set.ext $ λ _, exists_succ_above_eq_iff
+
 /-- Given a fixed pivot `x : fin (n + 1)`, `x.succ_above` is injective -/
 lemma succ_above_right_injective {x : fin (n + 1)} : injective (succ_above x) :=
 (succ_above x).injective
@@ -1173,7 +1188,7 @@ lemma succ_above_left_injective : injective (@succ_above n) :=
 λ _ _ h, by simpa [range_succ_above] using congr_arg (λ f : fin n ↪o fin (n + 1), (set.range f)ᶜ) h
 
 /-- `succ_above` is injective at the pivot -/
-lemma succ_above_left_inj {x y : fin (n + 1)} :
+@[simp] lemma succ_above_left_inj {x y : fin (n + 1)} :
   x.succ_above = y.succ_above ↔ x = y :=
 succ_above_left_injective.eq_iff
 
@@ -1390,24 +1405,6 @@ begin
     simp }
 end
 
-lemma forall_iff_succ_above {p : fin (n + 1) → Prop} (i : fin (n + 1)) :
-  (∀ j, p j) ↔ p i ∧ ∀ j, p (i.succ_above j) :=
-⟨λ h, ⟨h _, λ j, h _⟩,
-  λ h j, if hj : j = i then (hj.symm ▸ h.1) else
-  begin
-    cases n,
-    { convert h.1 },
-    { cases lt_or_gt_of_ne hj with lt gt,
-      { rcases j.zero_le.eq_or_lt with rfl|H,
-        { convert h.2 0, rw succ_above_below; simp [lt] },
-        { have ltl : j < last _ := lt.trans_le i.le_last,
-          convert h.2 j.cast_pred,
-          simp [succ_above_below, cast_succ_cast_pred ltl, lt] } },
-      { convert h.2 (j.pred (i.zero_le.trans_lt gt).ne.symm),
-        rw succ_above_above;
-        simp [le_cast_succ_iff, gt.lt] } }
-  end⟩
-
 end pred_above
 
 /-- `min n m` as an element of `fin (m + 1)` -/
@@ -1721,58 +1718,49 @@ section insert_nth
 
 variables {α : fin (n+1) → Type u} {β : Type v}
 
-/-- Insert an element into a tuple at a given position, auxiliary definition.
-For the general definition, see `insert_nth`. -/
-def insert_nth' {α : fin (n + 2) → Type u} (i : fin (n + 2)) (x : α i)
-  (p : Π j : fin (n + 1), α (i.succ_above j)) (j : fin (n + 2)) : α j :=
-if h : i = j
-then _root_.cast (congr_arg α h) x
-else if h' : j < i then _root_.cast (congr_arg α $ begin
-  obtain ⟨k, hk⟩ : ∃ (k : fin (n + 1)), k.cast_succ = j,
-    { refine ⟨⟨(j : ℕ), _⟩, _⟩,
-      { exact lt_of_lt_of_le h' i.is_le, },
-      { simp } },
-  subst hk,
-  simp [succ_above_below, h'],
-end)
-  (p j.cast_pred) else _root_.cast (congr_arg α $ begin
-  have lt : i < j := lt_of_le_of_ne (le_of_not_lt h') h,
-  have : j ≠ 0 := (ne_of_gt (lt_of_le_of_lt i.zero_le lt)),
-  rw [←succ_pred j this, ←le_cast_succ_iff] at lt,
-  simp [pred_above_zero this, succ_above_above _ _ lt]
-end) (p (fin.pred_above 0 j))
+/-- Define a function on `fin (n + 1)` from a value on `i : fin (n + 1)` and values on each
+`fin.succ_above i j`, `j : fin n`. This version is elaborated as eliminator and works for
+propositions, see also `fin.insert_nth` for a version without an `@[elab_as_eliminator]`
+attribute. -/
+@[elab_as_eliminator]
+def succ_above_cases {α : fin (n + 1) → Sort u} (i : fin (n + 1)) (x : α i)
+  (p : Π j : fin n, α (i.succ_above j)) (j : fin (n + 1)) : α j :=
+if hj : j = i then eq.rec x hj.symm
+else if hlt : j < i then eq.rec_on (succ_above_cast_lt hlt) (p _)
+else eq.rec_on (succ_above_pred $ (ne.lt_or_lt hj).resolve_left hlt) (p _)
+
+lemma forall_iff_succ_above {p : fin (n + 1) → Prop} (i : fin (n + 1)) :
+  (∀ j, p j) ↔ p i ∧ ∀ j, p (i.succ_above j) :=
+⟨λ h, ⟨h _, λ j, h _⟩, λ h, succ_above_cases i h.1 h.2⟩
 
 /-- Insert an element into a tuple at a given position. For `i = 0` see `fin.cons`,
-for `i = fin.last n` see `fin.snoc`. -/
-def insert_nth : Π {n : ℕ} {α : fin (n + 1) → Type u} (i : fin (n + 1)) (x : α i)
-  (p : Π j : fin n, α (i.succ_above j)) (j : fin (n + 1)), α j
-| 0       _ _ x _ _ := _root_.cast (by congr) x
-| (n + 1) _ i x p j := insert_nth' i x p j
+for `i = fin.last n` see `fin.snoc`. See also `fin.succ_above_cases` for a version elaborated
+as an eliminator. -/
+def insert_nth (i : fin (n + 1)) (x : α i) (p : Π j : fin n, α (i.succ_above j)) (j : fin (n + 1)) :
+  α j :=
+succ_above_cases i x p j
 
 @[simp] lemma insert_nth_apply_same (i : fin (n + 1)) (x : α i) (p : Π j, α (i.succ_above j)) :
   insert_nth i x p i = x :=
-by { cases n; simp [insert_nth, insert_nth'] }
+by simp [insert_nth, succ_above_cases]
 
 @[simp] lemma insert_nth_apply_succ_above (i : fin (n + 1)) (x : α i) (p : Π j, α (i.succ_above j))
   (j : fin n) :
   insert_nth i x p (i.succ_above j) = p j :=
 begin
-  cases n,
-  { exact j.elim0 },
-  simp only [insert_nth, insert_nth', dif_neg (succ_above_ne _ _).symm],
-  cases succ_above_lt_ge i j with h h,
-  { rw dif_pos,
-    refine eq_of_heq ((cast_heq _ _).trans _),
-    { simp [h] },
-    { congr,
-      simp [succ_above_below, h] } },
-  { rw dif_neg,
-    refine eq_of_heq ((cast_heq _ _).trans _),
-    { simp [h] },
-    { congr,
-      simp [succ_above_above, h, succ_ne_zero] } }
+  simp only [insert_nth, succ_above_cases, dif_neg (succ_above_ne _ _)],
+  by_cases hlt : j.cast_succ < i,
+  { rw [dif_pos ((succ_above_lt_iff _ _).2 hlt)],
+    apply eq_of_heq ((eq_rec_heq _ _).trans _),
+    rw [cast_lt_succ_above hlt] },
+  { rw [dif_neg (mt (succ_above_lt_iff _ _).1 hlt)],
+    apply eq_of_heq ((eq_rec_heq _ _).trans _),
+    rw [pred_succ_above (le_of_not_lt hlt)] }
 end
 
+@[simp] lemma succ_above_cases_eq_insert_nth :
+  @succ_above_cases.{u + 1} = @insert_nth.{u} := rfl
+
 @[simp] lemma insert_nth_comp_succ_above (i : fin (n + 1)) (x : β) (p : fin n → β) :
   insert_nth i x p ∘ i.succ_above = p :=
 funext $ insert_nth_apply_succ_above i x p
@@ -1814,6 +1802,41 @@ end
   @insert_nth _ (λ _, β) (last n) x p = snoc p x :=
 by simp [insert_nth_last]
 
+@[simp] lemma insert_nth_zero_right [Π j, has_zero (α j)] (i : fin (n + 1)) (x : α i) :
+  i.insert_nth x 0 = pi.single i x :=
+insert_nth_eq_iff.2 $ by simp [succ_above_ne, pi.zero_def]
+
+lemma insert_nth_binop (op : Π j, α j → α j → α j) (i : fin (n + 1))
+  (x y : α i) (p q : Π j, α (i.succ_above j)) :
+  i.insert_nth (op i x y) (λ j, op _ (p j) (q j)) =
+    λ j, op j (i.insert_nth x p j) (i.insert_nth y q j) :=
+insert_nth_eq_iff.2 $ by simp
+
+@[simp] lemma insert_nth_mul [Π j, has_mul (α j)] (i : fin (n + 1))
+  (x y : α i) (p q : Π j, α (i.succ_above j)) :
+  i.insert_nth (x * y) (p * q) = i.insert_nth x p * i.insert_nth y q :=
+insert_nth_binop (λ _, (*)) i x y p q
+
+@[simp] lemma insert_nth_add [Π j, has_add (α j)] (i : fin (n + 1))
+  (x y : α i) (p q : Π j, α (i.succ_above j)) :
+  i.insert_nth (x + y) (p + q) = i.insert_nth x p + i.insert_nth y q :=
+insert_nth_binop (λ _, (+)) i x y p q
+
+@[simp] lemma insert_nth_div [Π j, has_div (α j)] (i : fin (n + 1))
+  (x y : α i) (p q : Π j, α (i.succ_above j)) :
+  i.insert_nth (x / y) (p / q) = i.insert_nth x p / i.insert_nth y q :=
+insert_nth_binop (λ _, (/)) i x y p q
+
+@[simp] lemma insert_nth_sub [Π j, has_sub (α j)] (i : fin (n + 1))
+  (x y : α i) (p q : Π j, α (i.succ_above j)) :
+  i.insert_nth (x - y) (p - q) = i.insert_nth x p - i.insert_nth y q :=
+insert_nth_binop (λ _, has_sub.sub) i x y p q
+
+@[simp] lemma insert_nth_sub_same [Π j, add_group (α j)] (i : fin (n + 1))
+  (x y : α i) (p : Π j, α (i.succ_above j)) :
+  i.insert_nth x p - i.insert_nth y p = pi.single i (x - y) :=
+by simp_rw [← insert_nth_sub, ← insert_nth_zero_right, pi.sub_def, sub_self, pi.zero_def]
+
 variables [Π i, preorder (α i)]
 
 lemma insert_nth_le_iff {i : fin (n + 1)} {x : α i} {p : Π j, α (i.succ_above j)} {q : Π j, α j} :

src/data/fintype/basic.lean

@@ -130,6 +130,9 @@ set.ext $ λ x, mem_compl
 @[simp] theorem union_compl [decidable_eq α] (s : finset α) : s ∪ sᶜ = finset.univ :=
 sup_compl_eq_top
 
+@[simp] theorem insert_compl_self [decidable_eq α] (x : α) : insert x ({x}ᶜ : finset α) = univ :=
+by { ext y, simp [eq_or_ne] }
+
 @[simp] lemma compl_filter [decidable_eq α] (p : α → Prop) [decidable_pred p]
   [Π x, decidable (¬p x)] :
   (univ.filter p)ᶜ = univ.filter (λ x, ¬p x) :=
@@ -661,57 +664,32 @@ by simpa only [fintype.card_fin] using s.card_le_univ
 lemma fin.equiv_iff_eq {m n : ℕ} : nonempty (fin m ≃ fin n) ↔ m = n :=
   ⟨λ ⟨h⟩, by simpa using fintype.card_congr h, λ h, ⟨equiv.cast $ h ▸ rfl ⟩ ⟩
 
+@[simp] lemma fin.image_succ_above_univ {n : ℕ} (i : fin (n + 1)) :
+  univ.image i.succ_above = {i}ᶜ :=
+by { ext m, simp }
+
+@[simp] lemma fin.image_succ_univ (n : ℕ) : (univ : finset (fin n)).image fin.succ = {0}ᶜ :=
+by rw [← fin.succ_above_zero, fin.image_succ_above_univ]
+
+@[simp] lemma fin.image_cast_succ (n : ℕ) :
+  (univ : finset (fin n)).image fin.cast_succ = {fin.last n}ᶜ :=
+by rw [← fin.succ_above_last, fin.image_succ_above_univ]
+
 /-- Embed `fin n` into `fin (n + 1)` by prepending zero to the `univ` -/
 lemma fin.univ_succ (n : ℕ) :
   (univ : finset (fin (n + 1))) = insert 0 (univ.image fin.succ) :=
-begin
-  ext m,
-  simp only [mem_univ, mem_insert, true_iff, mem_image, exists_prop],
-  exact fin.cases (or.inl rfl) (λ i, or.inr ⟨i, trivial, rfl⟩) m
-end
+by simp
 
 /-- Embed `fin n` into `fin (n + 1)` by appending a new `fin.last n` to the `univ` -/
 lemma fin.univ_cast_succ (n : ℕ) :
   (univ : finset (fin (n + 1))) = insert (fin.last n) (univ.image fin.cast_succ) :=
-begin
-  ext m,
-  simp only [mem_univ, mem_insert, true_iff, mem_image, exists_prop, true_and],
-  by_cases h : m.val < n,
-  { right,
-    use fin.cast_lt m h,
-    rw fin.cast_succ_cast_lt },
-  { left,
-    exact fin.eq_last_of_not_lt h }
-end
+by simp
 
 /-- Embed `fin n` into `fin (n + 1)` by inserting
 around a specified pivot `p : fin (n + 1)` into the `univ` -/
 lemma fin.univ_succ_above (n : ℕ) (p : fin (n + 1)) :
   (univ : finset (fin (n + 1))) = insert p (univ.image (fin.succ_above p)) :=
-begin
-  obtain hl | rfl := (fin.le_last p).lt_or_eq,
-  { ext m,
-    simp only [finset.mem_univ, finset.mem_insert, true_iff, finset.mem_image, exists_prop],
-    refine or_iff_not_imp_left.mpr (λ h, _),
-    cases n,
-    { have : m = p := by simp,
-      exact absurd this h },
-    use p.cast_pred.pred_above m,
-    rw fin.pred_above,
-    split_ifs with H,
-    { simp only [fin.coe_cast_succ, true_and, fin.coe_coe_eq_self, coe_coe],
-      rw fin.lt_last_iff_coe_cast_pred at hl,
-      rw fin.succ_above_above,
-      { simp },
-      { simp only [fin.lt_iff_coe_lt_coe, fin.coe_cast_succ] at H,
-        simpa [fin.le_iff_coe_le_coe, ←hl] using nat.le_pred_of_lt H } },
-    { rw fin.succ_above_below,
-      { simp },
-      { simp only [fin.cast_succ_cast_pred hl, not_lt] at H,
-        simpa using lt_of_le_of_ne H h } } },
-  { rw fin.succ_above_last,
-    exact fin.univ_cast_succ n }
-end
+by simp
 
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 fintype.of_subsingleton (default α)

src/data/fintype/card.lean

@@ -126,51 +126,35 @@ theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : ∏ i, f i = 1
 
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f x`, for some `x : fin (n + 1)` times the remaining product -/
-theorem fin.prod_univ_succ_above [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
+@[to_additive
+/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
+is the sum of `f x`, for some `x : fin (n + 1)` plus the remaining product -/]
+theorem fin.prod_univ_succ_above [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β)
+  (x : fin (n + 1)) :
   ∏ i, f i = f x * ∏ i : fin n, f (x.succ_above i) :=
 begin
-  rw [fin.univ_succ_above, finset.prod_insert, finset.prod_image],
-  { intros x _ y _ hxy, exact fin.succ_above_right_inj.mp hxy },
-  { simp [fin.succ_above_ne] }
+  rw [fintype.prod_eq_mul_prod_compl x, ← fin.image_succ_above_univ, prod_image],
+  exact λ _ _ _ _ h, x.succ_above.injective h
 end
 
-/-- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
-is the sum of `f x`, for some `x : fin (n + 1)` plus the remaining product -/
-theorem fin.sum_univ_succ_above [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β)
-  (x : fin (n + 1)) :
-  ∑ i, f i = f x + ∑ i : fin n, f (x.succ_above i) :=
-by apply @fin.prod_univ_succ_above (multiplicative β)
-
-attribute [to_additive] fin.prod_univ_succ_above
-
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f 0` plus the remaining product -/
+@[to_additive
+/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
+is the sum of `f 0` plus the remaining product -/]
 theorem fin.prod_univ_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
   ∏ i, f i = f 0 * ∏ i : fin n, f i.succ :=
 fin.prod_univ_succ_above f 0
 
-/-- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
-is the sum of `f 0` plus the remaining product -/
-theorem fin.sum_univ_succ [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
-  ∑ i, f i = f 0 + ∑ i : fin n, f i.succ :=
-fin.sum_univ_succ_above f 0
-
-attribute [to_additive] fin.prod_univ_succ
-
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f (fin.last n)` plus the remaining product -/
+@[to_additive
+/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
+is the sum of `f (fin.last n)` plus the remaining sum -/]
 theorem fin.prod_univ_cast_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
   ∏ i, f i = (∏ i : fin n, f i.cast_succ) * f (fin.last n) :=
 by simpa [mul_comm] using fin.prod_univ_succ_above f (fin.last n)
 
-/-- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
-is the sum of `f (fin.last n)` plus the remaining sum -/
-theorem fin.sum_univ_cast_succ [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
-  ∑ i, f i = ∑ i : fin n, f i.cast_succ + f (fin.last n) :=
-by apply @fin.prod_univ_cast_succ (multiplicative β)
-
-attribute [to_additive] fin.prod_univ_cast_succ
-
 open finset
 
 @[simp] theorem fintype.card_sigma {α : Type*} (β : α → Type*)