ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : UInt16<GOAL>x.toUInt32.toNat = x.toNat
<VAR>x : UInt16<GOAL>x.toUInt64.toNat = x.toNat
<VAR>x y : UInt16<GOAL>(x + y).toNat = (x.toNat + y.toNat) % UInt16.size
<VAR>x y : UInt16<GOAL>(x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size
<VAR>x y : UInt16<GOAL>(x * y).toNat = x.toNat * y.toNat % UInt16.size
<VAR>x y : UInt16<GOAL>(x / y).toNat = x.toNat / y.toNat
<VAR>x y : UInt16<GOAL>(x % y).toNat = x.toNat % y.toNat
<VAR>x : UInt16<VAR>n : Nat<GOAL>(x.modn n).toNat = x.toNat % n
<VAR>x y : UInt16<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : UInt16<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>x y : UInt32<GOAL>x.toNat = y.toNat → x = y
<VAR>x y : UInt32<GOAL>x = y ↔ x.toNat = y.toNat
<VAR>x : UInt32<GOAL>↑x.val = x.toNat
<VAR>n : Nat<GOAL>(OfNat.ofNat n).toNat = n % UInt32.size
<VAR>x : UInt32<GOAL>x.toNat < 2 ^ 32
<VAR>x : UInt32<GOAL>x.toUInt8.toNat = x.toNat % 2 ^ 8
<VAR>x : UInt32<GOAL>x.toUInt16.toNat = x.toNat % 2 ^ 16
<VAR>x : UInt32<GOAL>x.toUInt64.toNat = x.toNat
<VAR>x y : UInt32<GOAL>(x + y).toNat = (x.toNat + y.toNat) % UInt32.size
<VAR>x y : UInt32<GOAL>(x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size
<VAR>x y : UInt32<GOAL>(x * y).toNat = x.toNat * y.toNat % UInt32.size
<VAR>x y : UInt32<GOAL>(x / y).toNat = x.toNat / y.toNat
<VAR>x y : UInt32<GOAL>(x % y).toNat = x.toNat % y.toNat
<VAR>x : UInt32<VAR>n : Nat<GOAL>(x.modn n).toNat = x.toNat % n
<VAR>x y : UInt32<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : UInt32<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>x y : UInt64<GOAL>x.toNat = y.toNat → x = y
<VAR>x y : UInt64<GOAL>x = y ↔ x.toNat = y.toNat
<VAR>x : UInt64<GOAL>↑x.val = x.toNat
<VAR>n : Nat<GOAL>(OfNat.ofNat n).toNat = n % UInt64.size
<VAR>x : UInt64<GOAL>x.toNat < 2 ^ 64
<VAR>x : UInt64<GOAL>x.toUInt8.toNat = x.toNat % 2 ^ 8
<VAR>x : UInt64<GOAL>x.toUInt16.toNat = x.toNat % 2 ^ 16
<VAR>x : UInt64<GOAL>x.toUInt32.toNat = x.toNat % 2 ^ 32
<VAR>x y : UInt64<GOAL>(x + y).toNat = (x.toNat + y.toNat) % UInt64.size
<VAR>x y : UInt64<GOAL>(x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size
<VAR>x y : UInt64<GOAL>(x * y).toNat = x.toNat * y.toNat % UInt64.size
<VAR>x y : UInt64<GOAL>(x / y).toNat = x.toNat / y.toNat
<VAR>x y : UInt64<GOAL>(x % y).toNat = x.toNat % y.toNat
<VAR>x : UInt64<VAR>n : Nat<GOAL>(x.modn n).toNat = x.toNat % n
<VAR>x y : UInt64<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : UInt64<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>x y : USize<GOAL>x.toNat = y.toNat → x = y
<VAR>x y : USize<GOAL>x = y ↔ x.toNat = y.toNat
<VAR>x : USize<GOAL>↑x.val = x.toNat
<VAR>n : Nat<GOAL>(OfNat.ofNat n).toNat = n % USize.size
<VAR>x : USize<GOAL>x.toUInt64.toNat = x.toNat
<VAR>x : UInt32<GOAL>x.toUSize.toNat = x.toNat
<VAR>x y : USize<GOAL>(x + y).toNat = (x.toNat + y.toNat) % USize.size
<VAR>x y : USize<GOAL>(x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size
<VAR>x y : USize<GOAL>(x * y).toNat = x.toNat * y.toNat % USize.size
<VAR>x y : USize<GOAL>(x / y).toNat = x.toNat / y.toNat
<VAR>x y : USize<GOAL>(x % y).toNat = x.toNat % y.toNat
<VAR>x : USize<VAR>n : Nat<GOAL>(x.modn n).toNat = x.toNat % n
<VAR>x y : USize<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : USize<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>motive : Nat → Sort u_1<VAR>zero : motive 0<VAR>succ : (n : Nat) → motive n → motive (n + 1)<GOAL>Nat.recAux zero succ 0 = zero
<VAR>motive : Nat → Sort u_1<VAR>zero : motive 0<VAR>succ : (n : Nat) → motive n → motive (n + 1)<VAR>n : Nat<GOAL>Nat.recAux zero succ (n + 1) = succ n (Nat.recAux zero succ n)
<VAR>motive : Nat → Sort u_1<VAR>zero : motive 0<VAR>succ : (n : Nat) → motive n → motive (n + 1)<GOAL>Nat.recAuxOn 0 zero succ = zero
<VAR>motive : Nat → Sort u_1<VAR>zero : motive 0<VAR>succ : (n : Nat) → motive n → motive (n + 1)<VAR>n : Nat<GOAL>Nat.recAuxOn (n + 1) zero succ = succ n (Nat.recAuxOn n zero succ)
<VAR>motive : Nat → Sort u_1<VAR>zero : motive 0<VAR>succ : (n : Nat) → motive (n + 1)<GOAL>Nat.casesAuxOn 0 zero succ = zero
<VAR>motive : Nat → Sort u_1<VAR>zero : motive 0<VAR>succ : (n : Nat) → motive (n + 1)<VAR>n : Nat<GOAL>Nat.casesAuxOn (n + 1) zero succ = succ n
<VAR>motive : Nat → Sort u_1<VAR>ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n<VAR>t : Nat<GOAL>Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m
<VAR>motive : Nat → Sort u_1<VAR>ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n<VAR>t : Nat<GOAL>t.strongRecOn ind = ind t fun m x => m.strongRecOn ind
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_left : (n : Nat) → motive 0 n<VAR>zero_right : (m : Nat) → motive m 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>n : Nat<GOAL>Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_left : (n : Nat) → motive 0 n<VAR>zero_right : (m : Nat) → motive m 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>m : Nat<VAR>h : zero_left 0 = zero_right 0 := by first | assumption | trivial<GOAL>Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_left : (n : Nat) → motive 0 n<VAR>zero_right : (m : Nat) → motive m 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>m n : Nat<GOAL>Nat.recDiagAux zero_left zero_right succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiagAux zero_left zero_right succ_succ m n)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<GOAL>Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>n : Nat<GOAL>Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n + 1) = zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>m : Nat<GOAL>Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) 0 = succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>m n : Nat<GOAL>Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<GOAL>Nat.recDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>n : Nat<GOAL>Nat.recDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n (Nat.recDiagOn 0 n zero_zero zero_succ succ_zero succ_succ)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>m : Nat<GOAL>Nat.recDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m (Nat.recDiagOn m 0 zero_zero zero_succ succ_zero succ_succ)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)<VAR>m n : Nat<GOAL>Nat.recDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n (Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ)
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive (m + 1) (n + 1)<GOAL>Nat.casesDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive (m + 1) (n + 1)<VAR>n : Nat<GOAL>Nat.casesDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive (m + 1) (n + 1)<VAR>m : Nat<GOAL>Nat.casesDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m
<VAR>motive : Nat → Nat → Sort u_1<VAR>zero_zero : motive 0 0<VAR>zero_succ : (n : Nat) → motive 0 (n + 1)<VAR>succ_zero : (m : Nat) → motive (m + 1) 0<VAR>succ_succ : (m n : Nat) → motive (m + 1) (n + 1)<VAR>m n : Nat<GOAL>Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n
<VAR>a : Nat<VAR>l : List Nat<GOAL>Nat.sum (a :: l) = a + Nat.sum l
<VAR>α : Type u_1<VAR>self : Array.PrefixTable α<VAR>i : Nat<VAR>h : i < self.size<GOAL>self.toArray[i].snd ≤ i
<VAR>α : Type u_1<VAR>p : α → Bool<GOAL>List.countP p [] = 0
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>n : Nat<VAR>l : List α<GOAL>List.countP.go p l n = n + List.countP.go p l 0
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : p a = true<GOAL>List.countP p (a :: l) = List.countP p l + 1
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : ¬p a = true<GOAL>List.countP p (a :: l) = List.countP p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<GOAL>List.countP p (a :: l) = List.countP p l + if p a = true then 1 else 0
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>l.length = List.countP p l + List.countP (fun a => decide ¬p a = true) l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.countP p l = (List.filter p l).length
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.countP p l ≤ l.length
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<GOAL>List.countP p (l₁ ++ l₂) = List.countP p l₁ + List.countP p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>0 < List.countP p l ↔ ∃ a, a ∈ l ∧ p a = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.countP p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.countP p l = l.length ↔ ∀ (a : α), a ∈ l → p a = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ <+ l₂<GOAL>List.countP p l₁ ≤ List.countP p l₂
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>List.countP p (List.filter q l) = List.countP (fun a => decide (p a = true ∧ q a = true)) l
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.countP (fun x => true) l = l.length
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.countP (fun x => false) l = 0
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>p : β → Bool<VAR>f : α → β<VAR>l : List α<GOAL>List.countP p (List.map f l) = List.countP (p ∘ f) l
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<VAR>h : ∀ (x : α), x ∈ l → p x = true → q x = true<GOAL>List.countP p l ≤ List.countP q l
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<VAR>h : ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)<GOAL>List.countP p l = List.countP q l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>List.count a [] = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>List.count a (b :: l) = List.count a l + if a = b then 1 else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.count a (a :: l) = List.count a l + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<VAR>l : List α<GOAL>List.count a (b :: l) = List.count a l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<VAR>h : l ≠ []<GOAL>List.count a l.tail = List.count a l - if a = l.head h then 1 else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.count a l ≤ l.length
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+ l₂<VAR>a : α<GOAL>List.count a l₁ ≤ List.count a l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>List.count a l ≤ List.count a (b :: l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>List.count a [a] = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>List.count a [b] = if a = b then 1 else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.count a (l.concat a) = (List.count a l).succ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>0 < List.count a l ↔ a ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : ¬a ∈ l<GOAL>List.count a l = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : List.count a l = 0<GOAL>¬a ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.count a l = 0 ↔ ¬a ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.count a l = l.length ↔ ∀ (b : α), b ∈ l → a = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : Nat<GOAL>List.count a (List.replicate n a) = n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>n : Nat<GOAL>List.count a (List.replicate n b) = if a = b then n else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>List.filter (fun x => x == a) l = List.replicate (List.count a l) a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>List.filter (fun x => decide (x = a)) l = List.replicate (List.count a l) a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>List.filter (fun x => decide (a = x)) l = List.replicate (List.count a l) a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>List.filter (fun x => a == x) l = List.replicate (List.count a l) a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>n ≤ List.count a l ↔ List.replicate n a <+ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : List.count a l = l.length<GOAL>List.replicate (List.count a l) a = l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : p a = true<GOAL>List.count a (List.filter p l) = List.count a l
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>β : Type u_1<VAR>DecidableEq β<VAR>l : List α<VAR>f : α → β<VAR>x : α<GOAL>List.count x l ≤ List.count (f x) (List.map f l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>List.count a (l.erase b) = List.count a l - if a = b then 1 else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.count a (l.erase a) = List.count a l - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>ab : a ≠ b<VAR>l : List α<GOAL>List.count a (l.erase b) = List.count a l
<VAR>m n : Nat<GOAL>m.Coprime n ↔ m.gcd n = 1
<VAR>m n : Nat<GOAL>m.Coprime n → m.gcd n = 1
<VAR>n m : Nat<GOAL>n.Coprime m → m.Coprime n
<VAR>n m : Nat<GOAL>n.Coprime m ↔ m.Coprime n
<VAR>k m n : Nat<VAR>H1 : k.Coprime m<VAR>H2 : k ∣ m * n<GOAL>k ∣ n
<VAR>k n : Nat<VAR>m : Nat<VAR>H : k.Coprime n<GOAL>(k * m).gcd n = m.gcd n
<VAR>k n : Nat<VAR>m : Nat<VAR>H : k.Coprime n<GOAL>(m * k).gcd n = m.gcd n
<VAR>k m : Nat<VAR>n : Nat<VAR>H : k.Coprime m<GOAL>m.gcd (k * n) = m.gcd n
<VAR>k m : Nat<VAR>n : Nat<VAR>H : k.Coprime m<GOAL>m.gcd (n * k) = m.gcd n
<VAR>d m n : Nat<VAR>dgt1 : 1 < d<VAR>Hm : d ∣ m<VAR>Hn : d ∣ n<GOAL>¬m.Coprime n
<VAR>m n : Nat<VAR>H : 0 < m.gcd n<GOAL>∃ g m' n', 0 < g ∧ m'.Coprime n' ∧ m = m' * g ∧ n = n' * g
<VAR>m k n : Nat<VAR>H1 : m.Coprime k<VAR>H2 : n.Coprime k<GOAL>(m * n).Coprime k
<VAR>k m n : Nat<VAR>H1 : k.Coprime m<VAR>H2 : k.Coprime n<GOAL>k.Coprime (m * n)
<VAR>n m k : Nat<VAR>H1 : n ∣ m<VAR>H2 : k.Coprime m<GOAL>k.Coprime n
<VAR>k m n : Nat<VAR>H : (k * m).Coprime n<GOAL>m.Coprime n
<VAR>m k n : Nat<VAR>H : (m * k).Coprime n<GOAL>m.Coprime n
<VAR>m k n : Nat<VAR>H : m.Coprime (k * n)<GOAL>m.Coprime n
<VAR>m n k : Nat<VAR>H : m.Coprime (n * k)<GOAL>m.Coprime n
<VAR>m n a : Nat<VAR>cmn : m.Coprime n<VAR>dvd : a ∣ n<GOAL>m.Coprime (n / a)
<VAR>m n k : Nat<GOAL>(m * n).Coprime k ↔ m.Coprime k ∧ n.Coprime k
<VAR>m n : Nat<VAR>k : Nat<VAR>hmn : m.Coprime n<GOAL>(k.gcd m).Coprime n
<VAR>m n : Nat<VAR>k : Nat<VAR>hmn : m.Coprime n<GOAL>m.Coprime (k.gcd n)
<VAR>m n : Nat<VAR>k l : Nat<VAR>hmn : m.Coprime n<GOAL>(k.gcd m).Coprime (l.gcd n)
<VAR>m n a : Nat<VAR>hmn : m.Coprime n<VAR>hm : m ∣ a<VAR>hn : n ∣ a<GOAL>m * n ∣ a
<VAR>n : Nat<GOAL>Nat.Coprime 0 n ↔ n = 1
<VAR>n : Nat<GOAL>n.Coprime 0 ↔ n = 1
<VAR>n : Nat<GOAL>Nat.Coprime 1 n
<VAR>n : Nat<GOAL>Nat.Coprime 1 n = True
<VAR>n : Nat<GOAL>n.Coprime 1 = True
<VAR>n : Nat<GOAL>n.Coprime n ↔ n = 1
<VAR>m k : Nat<VAR>n : Nat<VAR>H1 : m.Coprime k<GOAL>(m ^ n).Coprime k
<VAR>k m : Nat<VAR>n : Nat<VAR>H1 : k.Coprime m<GOAL>k.Coprime (m ^ n)
<VAR>k l : Nat<VAR>m n : Nat<VAR>H1 : k.Coprime l<GOAL>(k ^ m).Coprime (l ^ n)
<VAR>m n : Nat<VAR>k : Nat<VAR>h : m.Coprime n<GOAL>k.gcd (m * n) = k.gcd m * k.gcd n
<VAR>α : Type u_1<VAR>a b : Thunk α<GOAL>a.get = b.get → a = b
<VAR>a b : String.Pos<GOAL>a < b → b ≠ 0
<VAR>α : Type u_1<VAR>BEq α<VAR>Hashable α<VAR>self : Batteries.HashMap.LawfulHashable α<VAR>a b : α<GOAL>(a == b) = true → hash a = hash b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Batteries.HashMap.Imp.Buckets α β<VAR>i : USize<VAR>d : Batteries.AssocList α β<VAR>h : i.toNat < self.val.size<GOAL>(self.update i d h).val.size = self.val.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>buckets : Batteries.HashMap.Imp.Buckets α β<VAR>self : buckets.WF<VAR>Batteries.HashMap.LawfulHashable α<VAR>PartialEquivBEq α<VAR>bucket : Batteries.AssocList α β<GOAL>bucket ∈ buckets.val.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) bucket.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>buckets : Batteries.HashMap.Imp.Buckets α β<VAR>self : buckets.WF<VAR>i : Nat<VAR>h : i < buckets.val.size<GOAL>Batteries.AssocList.All (fun k x => ((hash k).toUSize % buckets.val.size).toNat = i) buckets.val[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>BEq α<VAR>Hashable α<GOAL>(Batteries.HashMap.Imp.empty n).WF
<VAR>a b : Char<GOAL>a.val = b.val → a = b
<VAR>x y : Char<GOAL>x = y ↔ x.val = y.val
<VAR>x y : Char<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : Char<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>n : Nat<VAR>x y : Fin n<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>n : Nat<VAR>x y : Fin n<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>n m : Nat<GOAL>↑(Fin.clamp n m) = min n m
<VAR>n : Nat<GOAL>(Fin.enum n).size = n
<VAR>n : Nat<VAR>i : Nat<VAR>h : i < (Fin.enum n).size<GOAL>(Fin.enum n)[i] = ⟨i, ⋯⟩
<VAR>n : Nat<GOAL>(Fin.list n).length = n
<VAR>n : Nat<VAR>i : Nat<VAR>h : i < (Fin.list n).length<GOAL>(Fin.list n)[i] = Fin.cast ⋯ ⟨i, h⟩
<VAR>n : Nat<VAR>i : Fin (Fin.list n).length<GOAL>(Fin.list n).get i = Fin.cast ⋯ i
<VAR>n : Nat<GOAL>Fin.list (n + 1) = 0 :: List.map Fin.succ (Fin.list n)
<VAR>n : Nat<GOAL>Fin.list (n + 1) = List.map Fin.castSucc (Fin.list n) ++ [Fin.last n]
<VAR>n : Nat<GOAL>(Fin.list n).reverse = List.map Fin.rev (Fin.list n)
<VAR>α : Sort u_1<VAR>n m : Nat<VAR>f : α → Fin n → α<VAR>x : α<VAR>h : m < n<GOAL>Fin.foldl.loop n f x m = Fin.foldl.loop n f (f x ⟨m, h⟩) (m + 1)
<VAR>α : Sort u_1<VAR>n : Nat<VAR>f : α → Fin n → α<VAR>x : α<GOAL>Fin.foldl.loop n f x n = x
<VAR>α : Sort u_1<VAR>n m : Nat<VAR>f : α → Fin (n + 1) → α<VAR>x : α<VAR>h : m < n + 1<GOAL>Fin.foldl.loop (n + 1) f x m = Fin.foldl.loop n (fun x i => f x i.succ) (f x ⟨m, h⟩) m
<VAR>α : Sort u_1<VAR>f : α → Fin 0 → α<VAR>x : α<GOAL>Fin.foldl 0 f x = x
<VAR>α : Sort u_1<VAR>n : Nat<VAR>f : α → Fin (n + 1) → α<VAR>x : α<GOAL>Fin.foldl (n + 1) f x = Fin.foldl n (fun x i => f x i.succ) (f x 0)
<VAR>α : Sort u_1<VAR>n : Nat<VAR>f : α → Fin (n + 1) → α<VAR>x : α<GOAL>Fin.foldl (n + 1) f x = f (Fin.foldl n (fun x x_1 => f x x_1.castSucc) x) (Fin.last n)
<VAR>α : Type u_1<VAR>n : Nat<VAR>f : α → Fin n → α<VAR>x : α<GOAL>Fin.foldl n f x = List.foldl f x (Fin.list n)
<VAR>n : Nat<VAR>α : Sort u_1<VAR>f : Fin n → α → α<VAR>x : α<GOAL>Fin.foldr.loop n f ⟨0, ⋯⟩ x = x
<VAR>n : Nat<VAR>α : Sort u_1<VAR>m : Nat<VAR>f : Fin n → α → α<VAR>x : α<VAR>h : m < n<GOAL>Fin.foldr.loop n f ⟨m + 1, h⟩ x = Fin.foldr.loop n f ⟨m, ⋯⟩ (f ⟨m, h⟩ x)
<VAR>n : Nat<VAR>α : Sort u_1<VAR>m : Nat<VAR>f : Fin (n + 1) → α → α<VAR>x : α<VAR>h : m + 1 ≤ n + 1<GOAL>Fin.foldr.loop (n + 1) f ⟨m + 1, h⟩ x = f 0 (Fin.foldr.loop n (fun i => f i.succ) ⟨m, ⋯⟩ x)
<VAR>α : Sort u_1<VAR>f : Fin 0 → α → α<VAR>x : α<GOAL>Fin.foldr 0 f x = x
<VAR>n : Nat<VAR>α : Sort u_1<VAR>f : Fin (n + 1) → α → α<VAR>x : α<GOAL>Fin.foldr (n + 1) f x = f 0 (Fin.foldr n (fun i => f i.succ) x)
<VAR>n : Nat<VAR>α : Sort u_1<VAR>f : Fin (n + 1) → α → α<VAR>x : α<GOAL>Fin.foldr (n + 1) f x = Fin.foldr n (fun x => f x.castSucc) (f (Fin.last n) x)
<VAR>n : Nat<VAR>α : Type u_1<VAR>f : Fin n → α → α<VAR>x : α<GOAL>Fin.foldr n f x = List.foldr f x (Fin.list n)
<VAR>n : Nat<VAR>α : Sort u_1<VAR>f : Fin n → α → α<VAR>x : α<GOAL>Fin.foldl n (fun x i => f i.rev x) x = Fin.foldr n f x
<VAR>α : Sort u_1<VAR>n : Nat<VAR>f : α → Fin n → α<VAR>x : α<GOAL>Fin.foldr n (fun i x => f x i.rev) x = Fin.foldl n f x
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>H : ∀ {x : α}, p x → q x<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.All p t → Batteries.RBNode.All q t
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.all p t = true ↔ Batteries.RBNode.All (fun x => p x = true) t
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.any p t = true ↔ Batteries.RBNode.Any (fun x => p x = true) t
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Batteries.TransCmp cmp], Batteries.RBNode.cmpLT cmp x y ↔ cmp x y = Ordering.lt
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Batteries.TransCmp cmp], Batteries.RBNode.cmpEq cmp x y ↔ cmp x y = Ordering.eq
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBSet α cmp<VAR>cut : α → Ordering<VAR>f : α → α<VAR>self : t.ModifyWF cut f<GOAL>Batteries.RBNode.WF cmp (Batteries.RBNode.modify cut f t.val)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBSet α cmp<VAR>cut : α → Ordering<VAR>f : Option α → Option α<VAR>self : t.AlterWF cut f<GOAL>Batteries.RBNode.WF cmp (Batteries.RBNode.alter cut f t.val)
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<VAR>path : Batteries.RBNode.Path α<GOAL>Batteries.RBNode.Path.fill' (Batteries.RBNode.zoom cut t path) = path.fill t
<GOAL>∀ {α : Type u_1} {cut : α → Ordering} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α}, Batteries.RBNode.zoom cut t path = (t', path') → path.fill t = path'.fill t'
<VAR>α : Type u_1<VAR>c₀ : Batteries.RBColor<VAR>n₀ : Nat<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>path : Batteries.RBNode.Path α<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Path.Balanced c₀ n₀ path c n → t.Balanced c n → (path.fill t).Balanced c₀ n₀
<GOAL>∀ {α : Type u_1} {cut : α → Ordering} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat}, t.Balanced c n → Batteries.RBNode.Path.Balanced c₀ n₀ path c n → Batteries.RBNode.zoom cut t path = (t', path') → ∃ c n, t'.Balanced c n ∧ Batteries.RBNode.Path.Balanced c₀ n₀ path' c n