ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>R S : α → α → Prop<VAR>H : ∀ (a b : α), R a b ↔ S a b<VAR>a : α<VAR>l : List α<GOAL>List.Chain R a l ↔ List.Chain S a l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Chain R a l ↔ List.Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a b : α<GOAL>List.Chain R a [b] ↔ R a b
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a b : α<VAR>l₁ l₂ : List α<GOAL>List.Chain R a (l₁ ++ b :: l₂) ↔ List.Chain R a (l₁ ++ [b]) ∧ List.Chain R b l₂
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a b c : α<VAR>l₁ l₂ : List α<GOAL>List.Chain R a (l₁ ++ b :: c :: l₂) ↔ List.Chain R a (l₁ ++ [b]) ∧ R b c ∧ List.Chain R c l₂
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Chain R a l ↔ l = [] ∨ List.Forall₂ R (a :: l.dropLast) l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<VAR>a b : α<GOAL>List.Chain R a (l ++ [b]) ↔ List.Forall₂ R (a :: l) (l ++ [b])
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>f : β → α<VAR>b : β<VAR>l : List β<GOAL>List.Chain R (f b) (List.map f l) ↔ List.Chain (fun a b => R (f a) (f b)) b l
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>f : α → β<VAR>H : ∀ (a b : α), S (f a) (f b) → R a b<VAR>a : α<VAR>l : List α<VAR>p : List.Chain S (f a) (List.map f l)<GOAL>List.Chain R a l
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>f : α → β<VAR>H : ∀ (a b : α), R a b → S (f a) (f b)<VAR>a : α<VAR>l : List α<VAR>p : List.Chain R a l<GOAL>List.Chain S (f a) (List.map f l)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)<VAR>a : α<VAR>l : List α<VAR>hl₁ : List.Chain R a l<VAR>ha : p a<VAR>hl₂ : ∀ (a : α), a ∈ l → p a<GOAL>List.Chain S (f a ha) (List.pmap f l hl₂)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>hl₁ : ∀ (a : α), a ∈ l → p a<VAR>a : α<VAR>ha : p a<VAR>hl₂ : List.Chain S (f a ha) (List.pmap f l hl₁)<VAR>H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b<GOAL>List.Chain R a l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>IsTrans α R<VAR>a : α<VAR>l : List α<GOAL>List.Chain R a l → List.Pairwise R (a :: l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>IsTrans α R<VAR>a : α<VAR>l : List α<GOAL>List.Chain R a l ↔ List.Pairwise R (a :: l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<VAR>a : α<VAR>IsTrans α R<VAR>hl : List.Chain R a l₂<VAR>h : l₁.Sublist l₂<GOAL>List.Chain R a l₁
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<VAR>a b : α<VAR>IsTrans α R<VAR>hl : List.Chain R a l<VAR>hb : b ∈ l<GOAL>R a b
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Chain R a l ↔ (∀ (h : 0 < l.length), R a (l.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)
<VAR>α : Type u<VAR>R S : α → α → Prop<VAR>H : ∀ (a b : α), R a b → S a b<VAR>l : List α<VAR>p : List.Chain' R l<GOAL>List.Chain' S l
<VAR>α : Type u<VAR>R S : α → α → Prop<VAR>H : ∀ (a b : α), R a b ↔ S a b<VAR>l : List α<GOAL>List.Chain' R l ↔ List.Chain' S l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Chain' R l ↔ List.Chain' (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l
<VAR>α : Type u<VAR>R : α → α → Prop<GOAL>List.Chain' R []
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a : α<GOAL>List.Chain' R [a]
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x y : α<VAR>l : List α<GOAL>List.Chain' R (x :: y :: l) ↔ R x y ∧ List.Chain' R (y :: l)
<VAR>α : Type u<VAR>l : List α<GOAL>List.Chain' (fun x y => [x, y] <:+: l) l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>List.Chain' R (l₁ ++ a :: l₂) ↔ List.Chain' R (l₁ ++ [a]) ∧ List.Chain' R (a :: l₂)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>b c : α<VAR>l₁ l₂ : List α<GOAL>List.Chain' R (l₁ ++ b :: c :: l₂) ↔ List.Chain' R (l₁ ++ [b]) ∧ R b c ∧ List.Chain' R (c :: l₂)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>f : β → α<VAR>l : List β<GOAL>List.Chain' R (List.map f l) ↔ List.Chain' (fun a b => R (f a) (f b)) l
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>f : α → β<VAR>H : ∀ (a b : α), S (f a) (f b) → R a b<VAR>l : List α<VAR>p : List.Chain' S (List.map f l)<GOAL>List.Chain' R l
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>f : α → β<VAR>H : ∀ (a b : α), R a b → S (f a) (f b)<VAR>l : List α<VAR>p : List.Chain' R l<GOAL>List.Chain' S (List.map f l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Pairwise R l → List.Chain' R l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>IsTrans α R<VAR>l : List α<GOAL>List.Chain' R l ↔ List.Pairwise R l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<VAR>IsTrans α R<VAR>hl : List.Chain' R l₂<VAR>h : l₁.Sublist l₂<GOAL>List.Chain' R l₁
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x y : α<VAR>l : List α<VAR>h₁ : R x y<VAR>h₂ : List.Chain' R (y :: l)<GOAL>List.Chain' R (x :: y :: l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Chain' R l → List.Chain' R l.tail
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x y : α<VAR>l : List α<VAR>h : List.Chain' R (x :: y :: l)<GOAL>R x y
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x : α<VAR>l : List α<VAR>h : List.Chain' R (x :: l)<VAR>y : α<VAR>hy : y ∈ l.head?<GOAL>R x y
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x : α<VAR>l : List α<GOAL>List.Chain' R l → (∀ (y : α), y ∈ l.head? → R x y) → List.Chain' R (x :: l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x : α<VAR>l : List α<GOAL>List.Chain' R (x :: l) ↔ (∀ (y : α), y ∈ l.head? → R x y) ∧ List.Chain' R l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<GOAL>List.Chain' R (l₁ ++ l₂) ↔ List.Chain' R l₁ ∧ List.Chain' R l₂ ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<VAR>h₁ : List.Chain' R l₁<VAR>h₂ : List.Chain' R l₂<VAR>h : ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y<GOAL>List.Chain' R (l₁ ++ l₂)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<VAR>h : List.Chain' R (l₁ ++ l₂)<GOAL>List.Chain' R l₁
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<VAR>h : List.Chain' R (l₁ ++ l₂)<GOAL>List.Chain' R l₂
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l l₁ : List α<VAR>h : List.Chain' R l<VAR>h' : l₁ <:+: l<GOAL>List.Chain' R l₁
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l l₁ : List α<VAR>h : List.Chain' R l<VAR>h' : l₁ <:+ l<GOAL>List.Chain' R l₁
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l l₁ : List α<VAR>h : List.Chain' R l<VAR>h' : l₁ <+: l<GOAL>List.Chain' R l₁
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<VAR>h : List.Chain' R l<VAR>n : ℕ<GOAL>List.Chain' R (List.drop n l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<VAR>h : List.Chain' R l<GOAL>List.Chain' R l.dropLast
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<VAR>h : List.Chain' R l<VAR>n : ℕ<GOAL>List.Chain' R (List.take n l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x y : α<GOAL>List.Chain' R [x, y] ↔ R x y
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>x y : α<VAR>h : ∀ {z : α}, R x z → R y z<VAR>l : List α<VAR>hl : List.Chain' R (x :: l)<GOAL>List.Chain' R (y :: l)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Chain' R l.reverse ↔ List.Chain' (flip R) l
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Chain' R l ↔ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l₁ l₂ l₃ : List α<VAR>h₁ : List.Chain' R (l₁ ++ l₂)<VAR>h₂ : List.Chain' R (l₂ ++ l₃)<VAR>hn : l₂ ≠ []<GOAL>List.Chain' R (l₁ ++ l₂ ++ l₃)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>L : List (List α)<GOAL>¬[] ∈ L → (List.Chain' R L.join ↔ (∀ (l : List α), l ∈ L → List.Chain' R l) ∧ List.Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) L)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Relation.ReflTransGen r a b<GOAL>∃ l, List.Chain r a l ∧ (a :: l).getLast ⋯ = b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → Prop<VAR>l : List α<VAR>h : List.Chain r a l<VAR>hb : (a :: l).getLast ⋯ = b<VAR>carries : ∀ ⦃x y : α⦄, r x y → p y → p x<VAR>final : p b<VAR>i : α<GOAL>i ∈ a :: l → p i
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → Prop<VAR>l : List α<VAR>h : List.Chain r a l<VAR>hb : (a :: l).getLast ⋯ = b<VAR>carries : ∀ ⦃x y : α⦄, r x y → p y → p x<VAR>final : p b<GOAL>p a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>hl₁ : List.Chain r a l<VAR>hl₂ : (a :: l).getLast ⋯ = b<GOAL>Relation.ReflTransGen r a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a : α<VAR>as m : List α<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>hm : List.Chain' (fun x x_1 => x > x_1) m<VAR>hmas : m ≤ as<GOAL>List.Chain' (fun x x_1 => x > x_1) (a :: m)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>l : List.chains r<VAR>acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a<GOAL>Acc (List.lex_chains r) l
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hwf : WellFounded r<GOAL>WellFounded (List.lex_chains r)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>i : ι<VAR>l : List ι<VAR>a : α i<VAR>f : (j : ι) → j ∈ l → α j<GOAL>List.Pi.cons i l a f = fun j hj => if h : j = i then ⋯ ▸ a else f j ⋯
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>i : ι<VAR>l : List ι<VAR>a : α i<VAR>f : (j : ι) → j ∈ l → α j<GOAL>Multiset.Pi.cons (↑l) i a f = List.Pi.cons i l a f
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>i : ι<VAR>l : List ι<VAR>f : (j : ι) → j ∈ i :: l → α j<GOAL>List.Pi.cons i l (List.Pi.head f) (List.Pi.tail f) = f
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>i : ι<VAR>l : List ι<VAR>a : α i<VAR>f : (j : ι) → j ∈ l → α j<VAR>α' : ι → Sort u_3<VAR>φ : ⦃j : ι⦄ → α j → α' j<GOAL>(List.Pi.cons i l (φ a) fun j hj => φ (f j hj)) = fun j hj => φ (List.Pi.cons i l a f j hj)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>i : ι<VAR>l : List ι<VAR>r : ⦃i : ι⦄ → α i → α i → Prop<VAR>a₁ a₂ : α i<VAR>f₁ f₂ : (j : ι) → j ∈ l → α j<VAR>ha : r a₁ a₂<VAR>hf : ∀ (i : ι) (hi : i ∈ l), r (f₁ i hi) (f₂ i hi)<VAR>j : ι<VAR>hj : j ∈ i :: l<GOAL>r (List.Pi.cons i l a₁ f₁ j hj) (List.Pi.cons i l a₂ f₂ j hj)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>t : (i : ι) → List (α i)<GOAL>[].pi t = [List.Pi.nil α]
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>i : ι<VAR>l : List ι<VAR>t : (j : ι) → List (α j)<GOAL>(i :: l).pi t = (t i).bind fun b => List.map (List.Pi.cons i l b) (l.pi t)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>l : List ι<VAR>fs : (i : ι) → List (α i)<GOAL>((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>l : List ι<VAR>fs : (i : ι) → List (α i)<VAR>f : (i : ι) → i ∈ l → α i<GOAL>f ∈ l.pi fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
<VAR>n : ℕ<GOAL>(List.Nat.antidiagonal n).length = n + 1
<GOAL>List.Nat.antidiagonal 0 = [(0, 0)]
<VAR>n : ℕ<GOAL>(List.Nat.antidiagonal n).Nodup
<VAR>n : ℕ<GOAL>List.Nat.antidiagonal (n + 1) = (0, n + 1) :: List.map (Prod.map Nat.succ id) (List.Nat.antidiagonal n)
<VAR>n : ℕ<GOAL>List.Nat.antidiagonal (n + 1) = List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]
<VAR>n : ℕ<GOAL>List.Nat.antidiagonal (n + 2) = (0, n + 2) :: List.map (Prod.map Nat.succ Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 2, 0)]
<VAR>n : ℕ<GOAL>List.map Prod.swap (List.Nat.antidiagonal n) = (List.Nat.antidiagonal n).reverse
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<VAR>m : ℕ<GOAL>(List.enumFrom n l)[m]? = Option.map (fun a => (n + m, a)) l[m]?
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<VAR>m : ℕ<GOAL>(List.enumFrom n l).get? m = Option.map (fun a => (n + m, a)) (l.get? m)
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<GOAL>l.enum[n]? = Option.map (fun a => (n, a)) l[n]?
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<GOAL>l.enum.get? n = Option.map (fun a => (n, a)) (l.get? n)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<GOAL>List.map Prod.snd (List.enumFrom n l) = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map Prod.snd l.enum = l
<VAR>α : Type u_1<VAR>l : List α<VAR>n i : ℕ<VAR>h : i < (List.enumFrom n l).length<GOAL>(List.enumFrom n l)[i] = (n + i, l[i])
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>i : Fin (List.enumFrom n l).length<GOAL>(List.enumFrom n l).get i = (n + ↑i, l.get (Fin.cast ⋯ i))
<VAR>α : Type u_1<VAR>l : List α<VAR>i : ℕ<VAR>h : i < l.enum.length<GOAL>l.enum[i] = (i, l[i])
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Fin l.enum.length<GOAL>l.enum.get i = (↑i, l.get (Fin.cast ⋯ i))
<VAR>α : Type u_1<VAR>n i : ℕ<VAR>x : α<VAR>l : List α<GOAL>(n + i, x) ∈ List.enumFrom n l ↔ l.get? i = some x
<VAR>α : Type u_1<VAR>n i : ℕ<VAR>x : α<VAR>l : List α<GOAL>(i, x) ∈ List.enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = some x
<VAR>α : Type u_1<VAR>i : ℕ<VAR>x : α<VAR>l : List α<GOAL>(i, x) ∈ l.enum ↔ l.get? i = some x
<VAR>α : Type u_1<VAR>x : ℕ × α<VAR>l : List α<GOAL>x ∈ l.enum ↔ l.get? x.1 = some x.2
<VAR>α : Type u_1<VAR>x : ℕ × α<VAR>n : ℕ<VAR>l : List α<VAR>h : x ∈ List.enumFrom n l<GOAL>n ≤ x.1
<VAR>α : Type u_1<VAR>x : ℕ × α<VAR>n : ℕ<VAR>l : List α<VAR>h : x ∈ List.enumFrom n l<GOAL>x.1 < n + l.length
<VAR>α : Type u_1<VAR>x : ℕ × α<VAR>l : List α<VAR>h : x ∈ l.enum<GOAL>x.1 < l.length
<VAR>α : Type u_1<VAR>x : ℕ × α<VAR>n : ℕ<VAR>l : List α<VAR>h : x ∈ List.enumFrom n l<GOAL>x.2 ∈ l
<VAR>α : Type u_1<VAR>x : ℕ × α<VAR>l : List α<VAR>h : x ∈ l.enum<GOAL>x.2 ∈ l
<VAR>α : Type u_1<VAR>x : α<VAR>i j : ℕ<VAR>xs : List α<VAR>h : (i, x) ∈ List.enumFrom j xs<GOAL>j ≤ i ∧ i < j + xs.length ∧ x ∈ xs
<VAR>α : Type u_1<VAR>x : α<VAR>n : ℕ<GOAL>List.enumFrom n [x] = [(n, x)]
<VAR>α : Type u_1<VAR>x : α<GOAL>[x].enum = [(0, x)]
<VAR>α : Type u_1<VAR>xs ys : List α<VAR>n : ℕ<GOAL>List.enumFrom n (xs ++ ys) = List.enumFrom n xs ++ List.enumFrom (n + xs.length) ys
<VAR>α : Type u_1<VAR>xs ys : List α<GOAL>(xs ++ ys).enum = xs.enum ++ List.enumFrom xs.length ys
<VAR>α : Type u_1<VAR>l : List α<VAR>n k : ℕ<GOAL>List.map (Prod.map (fun x => x + n) id) (List.enumFrom k l) = List.enumFrom (n + k) l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<GOAL>List.map (Prod.map (fun x => x + n) id) l.enum = List.enumFrom n l
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>List.enumFrom n (x :: xs) = (n, x) :: List.map (Prod.map Nat.succ id) (List.enumFrom n xs)
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).enum = (0, x) :: List.map (Prod.map Nat.succ id) xs.enum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>l : List α<VAR>f : α → β<GOAL>List.enumFrom n (List.map f l) = List.map (Prod.map id f) (List.enumFrom n l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β<GOAL>(List.map f l).enum = List.map (Prod.map id f) l.enum
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<GOAL>List.enumFrom n l = [] ↔ l = []
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.enum = [] ↔ l = []
<VAR>α : Type u_1<VAR>l : List α<VAR>nd : l.Nodup<VAR>h : ∀ (x : α), x ∈ l<VAR>i : Fin l.length<GOAL>↑(List.Nodup.getBijectionOfForallMemList l nd h) i = l.get i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>H : l.Nodup<VAR>i : Fin l.length<GOAL>↑((List.Nodup.getEquiv l H) i) = l.get i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>H : l.Nodup<VAR>x : { x // x ∈ l }<GOAL>↑((List.Nodup.getEquiv l H).symm x) = List.indexOf (↑x) l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>nd : l.Nodup<VAR>h : ∀ (x : α), x ∈ l<VAR>i : Fin l.length<GOAL>(List.Nodup.getEquivOfForallMemList l nd h) i = l.get i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>nd : l.Nodup<VAR>h : ∀ (x : α), x ∈ l<VAR>a : α<GOAL>↑((List.Nodup.getEquivOfForallMemList l nd h).symm a) = List.indexOf a l
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : List α<VAR>h : List.Sorted (fun x x_1 => x ≤ x_1) l<GOAL>Monotone l.get
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : List α<VAR>h : List.Sorted (fun x x_1 => x < x_1) l<GOAL>StrictMono l.get
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : List α<VAR>DecidableEq α<VAR>H : List.Sorted (fun x x_1 => x < x_1) l<VAR>i : Fin l.length<GOAL>↑((List.Sorted.getIso l H) i) = l.get i
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : List α<VAR>DecidableEq α<VAR>H : List.Sorted (fun x x_1 => x < x_1) l<VAR>x : { x // x ∈ l }<GOAL>↑((List.Sorted.getIso l H).symm x) = List.indexOf (↑x) l
<VAR>α : Type u_1<VAR>l l' : List α<VAR>f : ℕ ↪o ℕ<VAR>hf : ∀ (ix : ℕ), l.get? ix = l'.get? (f ix)<GOAL>l.Sublist l'
<VAR>α : Type u_1<VAR>l l' : List α<GOAL>l.Sublist l' ↔ ∃ f, ∀ (ix : ℕ), l.get? ix = l'.get? (f ix)
<VAR>α : Type u_1<VAR>l l' : List α<GOAL>l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<GOAL>List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<GOAL>List.Duplicate x l ↔ ∃ n, ∃ (hn : n < l.length), ∃ m, ∃ (hm : m < l.length) (_ : n < m), x = l.nthLe n hn ∧ x = l.nthLe m hm
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map j ≫ f) g = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i i = 𝟙 (AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i i)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map j ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map j ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g