Loogle!

Result

Found 212 declarations mentioning Fin.succAbove. Of these, only the first 200 are shown.

• Fin.predAbove_succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin n) : p.predAbove (p.castSucc.succAbove i) = i
• Fin.succAbove_last 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} : (Fin.last n).succAbove = Fin.castSucc
• Fin.succAbove_last_apply 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (i : Fin n) : (Fin.last n).succAbove i = i.castSucc
• Fin.succAbove_castSucc_self 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (j : Fin n) : j.castSucc.succAbove j = j.succ
• Fin.succAbove_succ_self 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (j : Fin n) : j.succ.succAbove j = j.castSucc
• Fin.succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1)
• Fin.succAbove_left_injective 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} : Function.Injective Fin.succAbove
• Fin.succAbove_right_injective 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} : Function.Injective p.succAbove
• Fin.succAbove_castSucc_of_le 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin n) (h : p ≤ i) : p.castSucc.succAbove i = i.succ
• Fin.succAbove_castSucc_of_lt 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin n) (h : i < p) : p.castSucc.succAbove i = i.castSucc
• Fin.succAbove_succ_of_le 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin n) (h : i ≤ p) : p.succ.succAbove i = i.castSucc
• Fin.succAbove_succ_of_lt 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin n) (h : p < i) : p.succ.succAbove i = i.succ
• Fin.ne_succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p ≠ p.succAbove i
• Fin.succAbove_ne 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i ≠ p
• Fin.succAbove_right_inj 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : p.succAbove i = p.succAbove j ↔ i = j
• Fin.succAbove_castPred_self 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (h : p ≠ Fin.last n) : p.succAbove (p.castPred h) = (p.castPred h).succ
• Fin.succAbove_predAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.castSucc) : p.castSucc.succAbove (p.predAbove i) = i
• Fin.succ_succAbove_predAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.succ) : p.succ.succAbove (p.predAbove i) = i
• Fin.succAbove_zero 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} : Fin.succAbove 0 = Fin.succ
• Fin.succAbove_zero_apply 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (i : Fin n) : Fin.succAbove 0 i = i.succ
• Fin.zero_succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (i : Fin n) : Fin.succAbove 0 i = i.succ
• Fin.succAbove_left_inj 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {x y : Fin (n + 1)} : x.succAbove = y.succAbove ↔ x = y
• Fin.exists_succAbove_eq 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {x y : Fin (n + 1)} (h : x ≠ y) : ∃ z, y.succAbove z = x
• Fin.exists_succAbove_eq_iff 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {x y : Fin (n + 1)} : (∃ z, x.succAbove z = y) ↔ y ≠ x
• Fin.succAbove_of_castSucc_lt 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.castSucc < p) : p.succAbove i = i.castSucc
• Fin.succAbove_of_le_castSucc 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p ≤ i.castSucc) : p.succAbove i = i.succ
• Fin.succAbove_of_lt_succ 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) : p.succAbove i = i.succ
• Fin.succAbove_of_succ_le 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.succ ≤ p) : p.succAbove i = i.castSucc
• Fin.succ_succAbove_zero 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} [NeZero n] (i : Fin n) : i.succ.succAbove 0 = 0
• Fin.lt_succAbove_iff_le_castSucc 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p ≤ i.castSucc
• Fin.lt_succAbove_iff_lt_castSucc 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p < i.succ
• Fin.succAbove_lt_iff_castSucc_lt 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.castSucc < p
• Fin.succAbove_lt_iff_succ_le 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.succ ≤ p
• Fin.coe_succAboveEmb 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) : ⇑p.succAboveEmb = p.succAbove
• Fin.succAboveEmb_apply 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAboveEmb i = p.succAbove i
• Fin.castSucc_succAbove_castSucc 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {i : Fin (n + 1)} {j : Fin n} : i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
• Fin.succ_succAbove_succ 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.succ.succAbove j.succ = (i.succAbove j).succ
• Fin.succAbove_ne_last_last 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {a : Fin (n + 2)} (h : a ≠ Fin.last (n + 1)) : a.succAbove (Fin.last n) = Fin.last (n + 1)
• Fin.succAbove_pred_self 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (h : p ≠ 0) : p.succAbove (p.pred h) = (p.pred h).castSucc
• Fin.succAbove_castPred_of_le 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hi : i ≠ Fin.last n) : p.succAbove (i.castPred hi) = (i.castPred hi).succ
• Fin.one_succAbove_succ 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (j : Fin n) : Fin.succAbove 1 j.succ = j.succ.succ
• Fin.succAbove_pos 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) : 0 < p.succAbove i
• Fin.range_succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) : Set.range p.succAbove = {p}ᶜ
• Fin.succAbove_ne_last 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n) : a.succAbove b ≠ Fin.last (n + 1)
• Fin.succAbove_eq_last_iff 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) : a.succAbove b = Fin.last (n + 1) ↔ b = Fin.last n
• Fin.succ_succAbove_one 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} [NeZero n] (i : Fin (n + 1)) : i.succ.succAbove 1 = (i.succAbove 0).succ
• Fin.succAbove_pred_of_le 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hi : i ≠ 0) : p.succAbove (i.pred hi) = (i.pred hi).castSucc
• Fin.succAbove_ne_zero_zero 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) : a.succAbove 0 = 0
• Fin.succAbove_ne_zero 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) (hb : b ≠ 0) : a.succAbove b ≠ 0
• Fin.succAbove_eq_zero_iff 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) : a.succAbove b = 0 ↔ b = 0
• Fin.castPred_succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : y.succAbove x ≠ Fin.last n := ⋯) : (y.succAbove x).castPred h' = x
• Fin.succAbove_castPred_of_lt 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin (n + 1)) (h : i < p) (hi : i ≠ Fin.last n := ⋯) : p.succAbove (i.castPred hi) = i
• Fin.pred_succAbove 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : y ≤ x.castSucc) (h' : y.succAbove x ≠ 0 := ⋯) : (y.succAbove x).pred h' = x
• Fin.castPred_succAbove_castPred 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n) (hk : a.succAbove b ≠ Fin.last (n + 1) := ⋯) : (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
• Fin.one_succAbove_one 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} : Fin.succAbove 1 1 = 2
• Fin.one_succAbove_zero 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} : Fin.succAbove 1 0 = 0
• Fin.succAbove_pred_of_lt 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} (p i : Fin (n + 1)) (h : p < i) (hi : i ≠ 0 := ⋯) : p.succAbove (i.pred hi) = i
• Fin.pred_succAbove_pred 📋 Mathlib.Data.Fin.Basic
  {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0) (hk : a.succAbove b ≠ 0 := ⋯) : (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
• Fin.rev_succAbove 📋 Mathlib.Data.Fin.Rev
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : (p.succAbove i).rev = p.rev.succAbove i.rev
• Fin.succAbove_rev_left 📋 Mathlib.Data.Fin.Rev
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.rev.succAbove i = (p.succAbove i.rev).rev
• Fin.succAbove_rev_right 📋 Mathlib.Data.Fin.Rev
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i.rev = (p.rev.succAbove i).rev
• Fin.insertNth_apply_same 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) : i.insertNth x p i = x
• Fin.removeNth 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) (i : Fin n) : α (p.succAbove i)
• Fin.insertNth 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : α j
• Fin.succAboveCases 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : α j
• Fin.forall_iff_succAbove 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∀ (i : Fin (n + 1)), P i) ↔ P p ∧ ∀ (i : Fin n), P (p.succAbove i)
• Fin.insertNthEquiv 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) : α p × ((i : Fin n) → α (p.succAbove i)) ≃ ((i : Fin (n + 1)) → α i)
• Fin.removeNth_insertNth 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (a : α p) (f : (i : Fin n) → α (p.succAbove i)) : p.removeNth (p.insertNth a f) = f
• Fin.succAbove_cases_eq_insertNth 📋 Mathlib.Data.Fin.Tuple.Basic
  : @Fin.succAboveCases = @Fin.insertNth
• Fin.insertNth_apply_succAbove 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin n) : i.insertNth x p (i.succAbove j) = p j
• Fin.insertNth_injective2 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} : Function.Injective2 p.insertNth
• Fin.insertNth_right_injective 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} (x : α p) : Function.Injective (p.insertNth x)
• Fin.insertNth_left_injective 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} (x : (i : Fin n) → α (p.succAbove i)) : Function.Injective fun x_1 => p.insertNth x_1 x
• Fin.removeNth.eq_1 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) (i : Fin n) : p.removeNth f i = f (p.succAbove i)
• Fin.insertNth_comp_succAbove 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {β : Sort u_2} (i : Fin (n + 1)) (x : β) (p : Fin n → β) : i.insertNth x p ∘ i.succAbove = p
• Fin.contractNth_apply_of_ne 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (hjk : ↑j ≠ ↑k) : j.contractNth op g k = g (j.succAbove k)
• Fin.eq_self_or_eq_succAbove 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} (p i : Fin (n + 1)) : i = p ∨ ∃ j, i = p.succAbove j
• Fin.exists_iff_succAbove 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∃ i, P i) ↔ P p ∨ ∃ i, P (p.succAbove i)
• Fin.insertNth.eq_1 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : i.insertNth x p j = i.succAboveCases x p j
• Fin.insertNth_inj 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {x y : (i : Fin n) → α (p.succAbove i)} {xₚ yₚ : α p} : p.insertNth xₚ x = p.insertNth yₚ y ↔ xₚ = yₚ ∧ x = y
• Fin.insertNth_last 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (j : Fin n) → α ((Fin.last n).succAbove j)) : (Fin.last n).insertNth x p = Fin.snoc (fun j => cast ⋯ (p j)) x
• Fin.removeNth_update 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (f : (j : Fin (n + 1)) → α j) : p.removeNth (Function.update f p x) = p.removeNth f
• Fin.eq_insertNth_iff 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {a : α p} {f : (i : Fin n) → α (p.succAbove i)} {g : (j : Fin (n + 1)) → α j} : g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f
• Fin.insertNth_eq_iff 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {a : α p} {f : (i : Fin n) → α (p.succAbove i)} {g : (j : Fin (n + 1)) → α j} : p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g
• Fin.update_insertNth 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x y : α p) (f : (i : Fin n) → α (p.succAbove i)) : Function.update (p.insertNth x f) p y = p.insertNth y f
• Fin.removeNth_update_succAbove 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (i : Fin n) (x : α (p.succAbove i)) (f : (j : Fin (n + 1)) → α j) : p.removeNth (Function.update f (p.succAbove i) x) = Function.update (p.removeNth f) i x
• Fin.insertNth_update 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (i : Fin n) (y : α (p.succAbove i)) (f : (j : Fin n) → α (p.succAbove j)) : p.insertNth x (Function.update f i y) = Function.update (p.insertNth x f) (p.succAbove i) y
• Fin.insertNth_binop 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (op : (j : Fin (n + 1)) → α j → α j → α j) (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : (i.insertNth (op i x y) fun j => op (i.succAbove j) (p j) (q j)) = fun j => op j (i.insertNth x p j) (i.insertNth y q j)
• Fin.removeNth_zero 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (f : (i : Fin (n + 1)) → α i) : Fin.removeNth 0 f = Fin.tail f
• Fin.insertNthEquiv_zero 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} (α : Fin (n + 1) → Type u_3) : Fin.insertNthEquiv α 0 = Fin.consEquiv α
• Fin.insertNthEquiv_apply 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) : (Fin.insertNthEquiv α p) f j = p.insertNth f.1 f.2 j
• Fin.insertNth_le_iff 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Type u_3} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} : i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (i.succAbove j)
• Fin.le_insertNth_iff 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Type u_3} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} : q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j => q (i.succAbove j)) ≤ p
• Fin.insertNthEquiv_symm_apply 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) : (Fin.insertNthEquiv α p).symm f = (f p, p.removeNth f)
• Fin.insertNth_zero 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α 0) (p : (j : Fin n) → α (Fin.succAbove 0 j)) : Fin.insertNth 0 x p = Fin.cons x fun j => cast ⋯ (p j)
• Fin.insertNth_apply_below 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {i j : Fin (n + 1)} (h : j < i) (x : α i) (p : (k : Fin n) → α (i.succAbove k)) : i.insertNth x p j = Eq.recOn ⋯ (p (j.castPred ⋯))
• Fin.succAboveCases.eq_1 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : i.succAboveCases x p j = if hj : j = i then ⋯ ▸ x else if hlt : j < i then Eq.recOn ⋯ (p (j.castPred ⋯)) else Eq.recOn ⋯ (p (j.pred ⋯))
• Fin.insertNth_apply_above 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {i j : Fin (n + 1)} (h : i < j) (x : α i) (p : (k : Fin n) → α (i.succAbove k)) : i.insertNth x p j = Eq.recOn ⋯ (p (j.pred ⋯))
• Fin.image_succAbove_univ 📋 Mathlib.Data.Fintype.Basic
  {n : ℕ} (i : Fin (n + 1)) : Finset.image i.succAbove Finset.univ = {i}ᶜ
• Fin.univ_succAbove 📋 Mathlib.Data.Fintype.Basic
  (n : ℕ) (p : Fin (n + 1)) : Finset.univ = Finset.cons p (Finset.map p.succAboveEmb Finset.univ) ⋯
• Fin.succAbove_inj 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : p.succAbove i = p.succAbove j ↔ i = j
• GCongr.Fin.succAbove_le_succAbove 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : i ≤ j → p.succAbove i ≤ p.succAbove j
• GCongr.Fin.succAbove_lt_succAbove 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : i < j → p.succAbove i < p.succAbove j
• Fin.succAbove_le_succAbove_iff 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : p.succAbove i ≤ p.succAbove j ↔ i ≤ j
• Fin.succAbove_lt_succAbove_iff 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : p.succAbove i < p.succAbove j ↔ i < j
• Fin.strictMono_succAbove 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) : StrictMono p.succAbove
• Fin.succAboveOrderEmb_apply 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAboveOrderEmb i = p.succAbove i
• Fin.succAboveOrderEmb_toEmbedding 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) : p.succAboveOrderEmb.toEmbedding = { toFun := p.succAbove, inj' := ⋯ }
• List.Vector.eraseIdx_insertIdx' 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {a : α} {v : List.Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} : List.Vector.eraseIdx (j.succAbove i) (List.Vector.insertIdx a j v) = List.Vector.insertIdx a (i.predAbove j) (List.Vector.eraseIdx i v)
• finSuccEquiv'_succAbove 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : (finSuccEquiv' i) (i.succAbove j) = some j
• finSuccEquiv'.eq_1 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} (i : Fin (n + 1)) : finSuccEquiv' i = { toFun := i.insertNth none some, invFun := fun x => x.casesOn' i i.succAbove, left_inv := ⋯, right_inv := ⋯ }
• finSuccEquiv'_symm_some 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : (finSuccEquiv' i).symm (some j) = i.succAbove j
• finSuccEquiv'_eq_some 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} {i j : Fin (n + 1)} {k : Fin n} : (finSuccEquiv' i) j = some k ↔ j = i.succAbove k
• finSuccAboveEquiv_apply 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : (finSuccAboveEquiv p) i = ⟨p.succAbove i, ⋯⟩
• Fin.prod_univ_succAbove 📋 Mathlib.Algebra.BigOperators.Fin
  {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)) : ∏ i, f i = f x * ∏ i, f (x.succAbove i)
• Fin.sum_univ_succAbove 📋 Mathlib.Algebra.BigOperators.Fin
  {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)) : ∑ i, f i = f x + ∑ i, f (x.succAbove i)
• Fin.inv_partialProd_mul_eq_contractNth 📋 Mathlib.Algebra.BigOperators.Fin
  {n : ℕ} {G : Type u_3} [Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) : (Fin.partialProd g (j.succ.succAbove k.castSucc))⁻¹ * Fin.partialProd g (j.succAbove k).succ = j.contractNth (fun x1 x2 => x1 * x2) g k
• Fin.neg_partialSum_add_eq_contractNth 📋 Mathlib.Algebra.BigOperators.Fin
  {n : ℕ} {G : Type u_3} [AddGroup G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) : -Fin.partialSum g (j.succ.succAbove k.castSucc) + Fin.partialSum g (j.succAbove k).succ = j.contractNth (fun x1 x2 => x1 + x2) g k
• Fin.insertNth_one_right 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → One (α j)] (i : Fin (n + 1)) (x : α i) : i.insertNth x 1 = Pi.mulSingle i x
• Fin.insertNth_zero_right 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Zero (α j)] (i : Fin (n + 1)) (x : α i) : i.insertNth x 0 = Pi.single i x
• Fin.insertNth_add 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Add (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x + y) (p + q) = i.insertNth x p + i.insertNth y q
• Fin.insertNth_div 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Div (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q
• Fin.insertNth_mul 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q
• Fin.insertNth_sub 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q
• Fin.insertNth_div_same 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Group (α j)] (i : Fin (n + 1)) (x y : α i) (p : (j : Fin n) → α (i.succAbove j)) : i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
• Fin.insertNth_sub_same 📋 Mathlib.Algebra.Group.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → AddGroup (α j)] (i : Fin (n + 1)) (x y : α i) (p : (j : Fin n) → α (i.succAbove j)) : i.insertNth x p - i.insertNth y p = Pi.single i (x - y)
• Matrix.submatrix_updateCol_succAbove 📋 Mathlib.Data.Matrix.Notation
  {α : Type u} {n : ℕ} {m' : Type uₘ} {o' : Type uₒ} (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m') (i : Fin n.succ) : (A.updateCol i v).submatrix f i.succAbove = A.submatrix f i.succAbove
• Matrix.submatrix_updateColumn_succAbove 📋 Mathlib.Data.Matrix.Notation
  {α : Type u} {n : ℕ} {m' : Type uₘ} {o' : Type uₒ} (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m') (i : Fin n.succ) : (A.updateCol i v).submatrix f i.succAbove = A.submatrix f i.succAbove
• Matrix.submatrix_updateRow_succAbove 📋 Mathlib.Data.Matrix.Notation
  {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix (Fin m.succ) n' α) (v : n' → α) (f : o' → n') (i : Fin m.succ) : (A.updateRow i v).submatrix i.succAbove f = A.submatrix i.succAbove f
• Fin.cycleRange_succAbove 📋 Mathlib.GroupTheory.Perm.Fin
  {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.cycleRange (i.succAbove j) = j.succ
• Fin.cycleRange_symm_succ 📋 Mathlib.GroupTheory.Perm.Fin
  {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : (Equiv.symm i.cycleRange) j.succ = i.succAbove j
• Fin.succAbove_cycleRange 📋 Mathlib.GroupTheory.Perm.Fin
  {n : ℕ} (i j : Fin n) : i.succ.succAbove (i.cycleRange j) = (Equiv.swap 0 i.succ) j.succ
• MultilinearMap.map_insertNth_add 📋 Mathlib.LinearAlgebra.Multilinear.Basic
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (p : Fin (n + 1)) (m : (i : Fin n) → M (p.succAbove i)) (x y : M p) : f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m)
• MultilinearMap.map_insertNth_smul 📋 Mathlib.LinearAlgebra.Multilinear.Basic
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (p : Fin (n + 1)) (m : (i : Fin n) → M (p.succAbove i)) (c : R) (x : M p) : f (p.insertNth (c • x) m) = c • f (p.insertNth x m)
• Matrix.det_succ_column_zero 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
  {R : Type v} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) : A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det
• Matrix.det_succ_row_zero 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
  {R : Type v} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) : A.det = ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
• Matrix.det_succ_column 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
  {R : Type v} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (j : Fin n.succ) : A.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
• Matrix.det_succ_row 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
  {R : Type v} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ) : A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
• Continuous.finInsertNth 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {n : ℕ} {π : Fin (n + 1) → Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : X → π i} {g : X → (j : Fin n) → π (i.succAbove j)} (hf : Continuous f) (hg : Continuous g) : Continuous fun a => i.insertNth (f a) (g a)
• Continuous.fin_insertNth 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {n : ℕ} {π : Fin (n + 1) → Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : X → π i} {g : X → (j : Fin n) → π (i.succAbove j)} (hf : Continuous f) (hg : Continuous g) : Continuous fun a => i.insertNth (f a) (g a)
• ContinuousAt.finInsertNth 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {n : ℕ} {π : Fin (n + 1) → Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : X → π i} {g : X → (j : Fin n) → π (i.succAbove j)} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun a => i.insertNth (f a) (g a)) x
• ContinuousAt.fin_insertNth 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {n : ℕ} {π : Fin (n + 1) → Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : X → π i} {g : X → (j : Fin n) → π (i.succAbove j)} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun a => i.insertNth (f a) (g a)) x
• Filter.Tendsto.finInsertNth 📋 Mathlib.Topology.Constructions
  {Y : Type v} {n : ℕ} {π : Fin (n + 1) → Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Y → π i} {g : Y → (j : Fin n) → π (i.succAbove j)} {l : Filter Y} {x : π i} {y : (j : Fin n) → π (i.succAbove j)} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun a => i.insertNth (f a) (g a)) l (nhds (i.insertNth x y))
• Filter.Tendsto.fin_insertNth 📋 Mathlib.Topology.Constructions
  {Y : Type v} {n : ℕ} {π : Fin (n + 1) → Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Y → π i} {g : Y → (j : Fin n) → π (i.succAbove j)} {l : Filter Y} {x : π i} {y : (j : Fin n) → π (i.succAbove j)} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun a => i.insertNth (f a) (g a)) l (nhds (i.insertNth x y))
• ContinuousOn.finInsertNth 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : α → π i} {g : α → (j : Fin n) → π (i.succAbove j)} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun a => i.insertNth (f a) (g a)) s
• ContinuousOn.fin_insertNth 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : α → π i} {g : α → (j : Fin n) → π (i.succAbove j)} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun a => i.insertNth (f a) (g a)) s
• ContinuousWithinAt.finInsertNth 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : α → π i} {g : α → (j : Fin n) → π (i.succAbove j)} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a
• ContinuousWithinAt.fin_insertNth 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : α → π i} {g : α → (j : Fin n) → π (i.succAbove j)} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a
• Fin.dist_insertNth_insertNth 📋 Mathlib.Topology.MetricSpace.Pseudo.Pi
  {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : (j : Fin n) → α (i.succAbove j)) : dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)
• Fin.nndist_insertNth_insertNth 📋 Mathlib.Topology.MetricSpace.Pseudo.Pi
  {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : (j : Fin n) → α (i.succAbove j)) : nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g)
• Fin.succAbove.eq_1 📋 Mathlib.LinearAlgebra.Matrix.Adjugate
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i = if i.castSucc < p then i.castSucc else i.succ
• Matrix.adjugate_fin_succ_eq_det_submatrix 📋 Mathlib.LinearAlgebra.Matrix.Adjugate
  {α : Type w} [CommRing α] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j : Fin n.succ) : A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
• LinearMap.uncurryMid 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) (f : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) : MultilinearMap R M M₂
• MultilinearMap.curryMid 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) (f : MultilinearMap R M M₂) : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂
• LinearMap.curryMid_uncurryMid 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (i : Fin (n + 1)) (f : M i →ₗ[R] MultilinearMap R (fun j => M (i.succAbove j)) M₂) : MultilinearMap.curryMid i (LinearMap.uncurryMid i f) = f
• MultilinearMap.curryMid_apply_apply 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) (f : MultilinearMap R M M₂) (x : M p) (m : (i : Fin n) → M (p.succAbove i)) : ((MultilinearMap.curryMid p f) x) m = f (p.insertNth x m)
• LinearMap.uncurryMid_apply 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) (f : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) (m : (i : Fin n.succ) → M i) : (LinearMap.uncurryMid p f) m = (f (m p)) (p.removeNth m)
• MultilinearMap.curryMidLinearEquiv 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) : MultilinearMap R M M₂ ≃ₗ[R] M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂
• MultilinearMap.curryMidLinearEquiv_apply 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) (f : MultilinearMap R M M₂) : (MultilinearMap.curryMidLinearEquiv R M M₂ p) f = MultilinearMap.curryMid p f
• MultilinearMap.curryMidLinearEquiv_symm_apply 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (p : Fin (n + 1)) (f : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) : (MultilinearMap.curryMidLinearEquiv R M M₂ p).symm f = LinearMap.uncurryMid p f
• MeasurableEquiv.piFinSuccAbove 📋 Mathlib.MeasureTheory.MeasurableSpace.Embedding
  {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) : ((j : Fin (n + 1)) → α j) ≃ᵐ α i × ((j : Fin n) → α (i.succAbove j))
• MeasurableEquiv.piFinSuccAbove_apply 📋 Mathlib.MeasureTheory.MeasurableSpace.Embedding
  {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) : ⇑(MeasurableEquiv.piFinSuccAbove α i) = ⇑(Fin.insertNthEquiv α i).symm
• MeasurableEquiv.piFinSuccAbove_symm_apply 📋 Mathlib.MeasureTheory.MeasurableSpace.Embedding
  {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) : ⇑(MeasurableEquiv.piFinSuccAbove α i).symm = ⇑(Fin.insertNthEquiv α i)
• MeasureTheory.measurePreserving_piFinSuccAbove 📋 Mathlib.MeasureTheory.Constructions.Pi
  {n : ℕ} {α : Fin (n + 1) → Type u} {m : (i : Fin (n + 1)) → MeasurableSpace (α i)} (μ : (i : Fin (n + 1)) → MeasureTheory.Measure (α i)) [∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite (μ i)] (i : Fin (n + 1)) : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) (MeasureTheory.Measure.pi μ) ((μ i).prod (MeasureTheory.Measure.pi fun j => μ (i.succAbove j)))
• MeasureTheory.volume_preserving_piFinSuccAbove 📋 Mathlib.MeasureTheory.Constructions.Pi
  {n : ℕ} (α : Fin (n + 1) → Type u) [(i : Fin (n + 1)) → MeasureTheory.MeasureSpace (α i)] [∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite MeasureTheory.volume] (i : Fin (n + 1)) : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) MeasureTheory.volume MeasureTheory.volume
• Fin.insertNthOrderIso 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) : α p × ((i : Fin n) → α (p.succAbove i)) ≃o ((i : Fin (n + 1)) → α i)
• Fin.preimage_insertNth_Icc_of_not_mem 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ q₂ : (j : Fin (n + 1)) → α j} (hx : x ∉ Set.Icc (q₁ i) (q₂ i)) : i.insertNth x ⁻¹' Set.Icc q₁ q₂ = ∅
• Fin.preimage_insertNth_Icc_of_mem 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ q₂ : (j : Fin (n + 1)) → α j} (hx : x ∈ Set.Icc (q₁ i) (q₂ i)) : i.insertNth x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
• Fin.insertNthOrderIso_toEquiv 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) : (Fin.insertNthOrderIso α p).toEquiv = Fin.insertNthEquiv α p
• Fin.insertNth_mem_Icc 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q₁ q₂ : (j : Fin (n + 1)) → α j} : i.insertNth x p ∈ Set.Icc q₁ q₂ ↔ x ∈ Set.Icc (q₁ i) (q₂ i) ∧ p ∈ Set.Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
• Fin.insertNthOrderIso.eq_1 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) : Fin.insertNthOrderIso α p = { toEquiv := Fin.insertNthEquiv α p, map_rel_iff' := ⋯ }
• Fin.insertNthOrderIso_apply 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) : (Fin.insertNthOrderIso α p) f j = p.insertNth f.1 f.2 j
• Fin.insertNthOrderIso_zero 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : Fin.insertNthOrderIso α 0 = Fin.consOrderIso α
• finSuccAboveOrderIso_apply 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : (finSuccAboveOrderIso p) i = ⟨p.succAbove i, ⋯⟩
• Fin.insertNthOrderIso_symm_apply 📋 Mathlib.Order.Fin.Tuple
  {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) : (RelIso.symm (Fin.insertNthOrderIso α p)) f = (f p, p.removeNth f)
• BoxIntegral.Box.face_lower 📋 Mathlib.Analysis.BoxIntegral.Box.Basic
  {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (a✝ : Fin n) : (I.face i).lower a✝ = I.lower (i.succAbove a✝)
• BoxIntegral.Box.face_upper 📋 Mathlib.Analysis.BoxIntegral.Box.Basic
  {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (a✝ : Fin n) : (I.face i).upper a✝ = I.upper (i.succAbove a✝)
• BoxIntegral.Box.face_mk 📋 Mathlib.Analysis.BoxIntegral.Box.Basic
  {n : ℕ} (l u : Fin (n + 1) → ℝ) (h : ∀ (i : Fin (n + 1)), l i < u i) (i : Fin (n + 1)) : { lower := l, upper := u, lower_lt_upper := h }.face i = { lower := l ∘ i.succAbove, upper := u ∘ i.succAbove, lower_lt_upper := ⋯ }
• BoxIntegral.Box.face.eq_1 📋 Mathlib.Analysis.BoxIntegral.Partition.Additive
  {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) : I.face i = { lower := I.lower ∘ i.succAbove, upper := I.upper ∘ i.succAbove, lower_lt_upper := ⋯ }
• Fin.insertNth_mem_piFinset_insertNth 📋 Mathlib.Data.Fin.Tuple.Finset
  {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} {x_pivot : α p} {x_remove : (i : Fin n) → α (p.succAbove i)} {s_pivot : Finset (α p)} {s_remove : (i : Fin n) → Finset (α (p.succAbove i))} : p.insertNth x_pivot x_remove ∈ Fintype.piFinset (p.insertNth s_pivot s_remove) ↔ x_pivot ∈ s_pivot ∧ x_remove ∈ Fintype.piFinset s_remove
• Fin.mem_piFinset_iff_pivot_removeNth 📋 Mathlib.Data.Fin.Tuple.Finset
  {n : ℕ} {α : Fin (n + 1) → Type u_1} {f : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)} (p : Fin (n + 1)) : f ∈ Fintype.piFinset s ↔ f p ∈ s p ∧ p.removeNth f ∈ Fintype.piFinset (p.removeNth s)
• Finset.card_insertNthEquiv_filter_piFinset 📋 Mathlib.Data.Fin.Tuple.Finset
  {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α (p.succAbove i)) → Prop) [DecidablePred P] : {r ∈ Fintype.piFinset S | P (p.removeNth r)}.card = (S p).card * {r ∈ Fintype.piFinset (p.removeNth S) | P r}.card
• Finset.filter_piFinset_eq_map_insertNthEquiv 📋 Mathlib.Data.Fin.Tuple.Finset
  {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α (p.succAbove i)) → Prop) [DecidablePred P] : {r ∈ Fintype.piFinset S | P (p.removeNth r)} = Finset.map (Fin.insertNthEquiv α p).toEmbedding (S p ×ˢ {r ∈ Fintype.piFinset (p.removeNth S) | P r})
• Finset.map_insertNthEquiv_filter_piFinset 📋 Mathlib.Data.Fin.Tuple.Finset
  {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α (p.succAbove i)) → Prop) [DecidablePred P] : Finset.map (Fin.insertNthEquiv α p).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (p.removeNth r)}) = S p ×ˢ {r ∈ Fintype.piFinset (p.removeNth S) | P r}
• ContinuousMultilinearMap.norm_map_insertNth_le 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) {i : Fin (n + 1)} (x : Ei i) (m : (j : Fin n) → Ei (i.succAbove j)) : ‖f (i.insertNth x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i_1, ‖m i_1‖
• ContinuousLinearMap.uncurryMid 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G) : ContinuousMultilinearMap 𝕜 Ei G
• ContinuousMultilinearMap.curryMid 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G) : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G
• ContinuousMultilinearMap.norm_curryMid 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G) : ‖ContinuousMultilinearMap.curryMid p f‖ = ‖f‖
• ContinuousLinearMap.curryMid_uncurryMid 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G) : ContinuousMultilinearMap.curryMid p (ContinuousLinearMap.uncurryMid p f) = f
• ContinuousLinearMap.norm_uncurryMid 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G) : ‖ContinuousLinearMap.uncurryMid p f‖ = ‖f‖
• ContinuousMultilinearMap.curryMid_apply 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei p) (m : (i : Fin n) → Ei (p.succAbove i)) : ((ContinuousMultilinearMap.curryMid p f) x) m = f (p.insertNth x m)
• ContinuousLinearMap.uncurryMid_apply 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G) (m : (i : Fin n.succ) → Ei i) : (ContinuousLinearMap.uncurryMid p f) m = (f (m p)) (p.removeNth m)
• ContinuousLinearMap.norm_map_removeNth_le 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {i : Fin (n + 1)} (f : Ei i →L[𝕜] ContinuousMultilinearMap 𝕜 (fun j => Ei (i.succAbove j)) G) (m : (i : Fin n.succ) → Ei i) : ‖(f (m i)) (i.removeNth m)‖ ≤ ‖f‖ * ∏ j, ‖m j‖
• ContinuousMultilinearMap.curryMidEquiv 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) : ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G
• ContinuousMultilinearMap.curryMidEquiv_apply 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G) : (ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p) f = ContinuousMultilinearMap.curryMid p f
• ContinuousMultilinearMap.curryMidEquiv_symm_apply 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G) : (ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p).symm f = ContinuousLinearMap.uncurryMid p f
• MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable' 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ) (hle : a ≤ b) (f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E) (f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable) (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) (Hi : MeasureTheory.IntegrableOn (fun x => ∑ i, (f' i x) (Pi.single i 1)) (Set.Icc a b) MeasureTheory.volume) : ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' i x) (Pi.single i 1) = ∑ i, ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (b i) x)) - ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (a i) x))
• MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable' 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ) (hle : a ≤ b) (f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E) (f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable) (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) (Hi : MeasureTheory.IntegrableOn (fun x => ∑ i, (f' i x) (Pi.single i 1)) (Set.Icc a b) MeasureTheory.volume) : ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' i x) (Pi.single i 1) = ∑ i, ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (b i) x)) - ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (a i) x))
• MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ) (hle : a ≤ b) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable) (Hc : ContinuousOn f (Set.Icc a b)) (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (Set.Icc a b) MeasureTheory.volume) : ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (Pi.single i 1) i = ∑ i, ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) - ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
• MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ) (hle : a ≤ b) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable) (Hc : ContinuousOn f (Set.Icc a b)) (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (Set.Icc a b) MeasureTheory.volume) : ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (Pi.single i 1) i = ∑ i, ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) - ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08