ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b c : Int<GOAL>a - b < c ↔ a < c + b
<VAR>a b c : Int<VAR>h : a - b < c<GOAL>a - c < b
<VAR>a b : Int<VAR>h : a < b<VAR>c : Int<GOAL>c - b < c - a
<VAR>a b : Int<VAR>h : a < b<VAR>c : Int<GOAL>a - c < b - c
<VAR>a b c d : Int<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a - d < b - c
<VAR>a b c : Int<VAR>h : c - a < c - b<GOAL>b < a
<VAR>a b c : Int<VAR>h : a - c < b - c<GOAL>a < b
<VAR>a b c : Int<GOAL>c - a < c - b ↔ b < a
<VAR>a b c : Int<GOAL>a - c < b - c ↔ a < b
<VAR>a b c d : Int<VAR>hab : a ≤ b<VAR>hcd : c < d<GOAL>a - d < b - c
<VAR>a b c d : Int<VAR>hab : a < b<VAR>hcd : c ≤ d<GOAL>a - d < b - c
<VAR>a b c d e f : Int<VAR>h₁ : a ≤ d<VAR>h₂ : b ≤ e<VAR>h₃ : c ≤ f<GOAL>a + b + c ≤ d + e + f
<VAR>a : Int<VAR>H : a ≤ 0<GOAL>∃ n, a = -↑n
<VAR>a b : Int<VAR>H : a + 1 ≤ b<GOAL>a < b
<VAR>a b : Int<VAR>H : a ≤ b<GOAL>a < b + 1
<VAR>a b : Int<VAR>H : a < b + 1<GOAL>a ≤ b
<VAR>a b : Int<VAR>H : a ≤ b<GOAL>a - 1 < b
<VAR>a b : Int<VAR>H : a - 1 < b<GOAL>a ≤ b
<VAR>a b : Int<VAR>H : a < b<GOAL>a ≤ b - 1
<VAR>a b : Int<VAR>H : a ≤ b - 1<GOAL>a < b
<VAR>a b c d : Int<VAR>h₁ : a < c<VAR>h₂ : b ≤ d<VAR>h₃ : 0 < b<VAR>h₄ : 0 ≤ c<GOAL>a * b < c * d
<VAR>a b c d : Int<VAR>h₁ : a ≤ c<VAR>h₂ : b < d<VAR>h₃ : 0 ≤ b<VAR>h₄ : 0 < c<GOAL>a * b < c * d
<VAR>a b : Int<VAR>ha : 0 < a<VAR>hb : b < 0<GOAL>a * b < 0
<VAR>a b : Int<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>a * b < 0
<VAR>a b : Int<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>0 ≤ a * b
<VAR>a b c : Int<VAR>h : b < a<VAR>hc : c < 0<GOAL>c * a < c * b
<VAR>a b c : Int<VAR>h : b < a<VAR>hc : c < 0<GOAL>a * c < b * c
<VAR>a b : Int<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>0 < a * b
<VAR>a b : Int<VAR>h1 : 0 ≤ a<VAR>h2 : a ≤ b<GOAL>a * a ≤ b * b
<VAR>a b : Int<VAR>h1 : 0 ≤ a<VAR>h2 : a < b<GOAL>a * a < b * b
<VAR>x : Nat<GOAL>(↑x + 1).sign = 1
<VAR>x : Nat<GOAL>(Int.negSucc x).sign = -1
<VAR>z : Int<GOAL>z.sign.natAbs = if z = 0 then 0 else 1
<VAR>z : Int<VAR>hz : z ≠ 0<GOAL>z.sign.natAbs = 1
<VAR>n : Nat<VAR>hn : n ≠ 0<GOAL>(↑n).sign = 1
<VAR>a : Int<GOAL>a.sign * ↑a.natAbs = a
<VAR>a b : Int<GOAL>(a * b).sign = a.sign * b.sign
<VAR>a : Int<VAR>h : 0 < a<GOAL>a.sign = 1
<VAR>a : Int<VAR>h : a < 0<GOAL>a.sign = -1
<VAR>a : Int<GOAL>a.sign = 0 → a = 0
<VAR>a : Int<GOAL>a.sign = 1 → 0 < a
<VAR>a : Int<GOAL>a.sign = -1 → a < 0
<VAR>a : Int<GOAL>a.sign = 1 ↔ 0 < a
<VAR>a : Int<GOAL>a.sign = -1 ↔ a < 0
<VAR>a : Int<GOAL>a.sign = 0 ↔ a = 0
<VAR>x : Int<GOAL>0 ≤ x.sign ↔ 0 ≤ x
<VAR>i : Int<GOAL>i * i.sign = ↑i.natAbs
<VAR>a : Int<GOAL>a.natAbs ≠ 0 ↔ a ≠ 0
<VAR>a : Int<GOAL>↑(a.natAbs * a.natAbs) = a * a
<VAR>a : Int<GOAL>∃ n, a = ↑n ∨ a = -↑n
<VAR>a b : Int<VAR>c : Nat<VAR>h : a * b = ↑c<GOAL>a.natAbs * b.natAbs = c
<VAR>a : Int<GOAL>↑a.natAbs * ↑a.natAbs = a * a
<VAR>a : Int<VAR>n : Nat<GOAL>a.natAbs = n ↔ a = ↑n ∨ a = -↑n
<VAR>a b : Int<GOAL>(a + b).natAbs ≤ a.natAbs + b.natAbs
<VAR>a b : Int<GOAL>(a - b).natAbs ≤ a.natAbs + b.natAbs
<VAR>m : Nat<GOAL>Int.negSucc m = -↑m - 1
<VAR>a b : Int<VAR>w₁ : 0 ≤ a<VAR>w₂ : a < b<GOAL>a.natAbs < b.natAbs
<VAR>a : Int<VAR>n : Nat<GOAL>a.natAbs = n ↔ (a - ↑n) * (a + ↑n) = 0
<VAR>n : Nat<VAR>hNe : n ≠ 0<GOAL>n / 2 < n
<VAR>a b : Nat<GOAL>a <<< b = a * 2 ^ b
<VAR>m n : Nat<GOAL>m >>> (n + 1) = m >>> n / 2
<VAR>m n k : Nat<GOAL>m >>> (n + k) = m >>> n >>> k
<VAR>m n : Nat<GOAL>m >>> n = m / 2 ^ n
<VAR>α : Type u_1<VAR>x : α<GOAL>some x ≠ none
<VAR>α : Type u_1<VAR>p : Option α → Prop<GOAL>(∀ (x : Option α), p x) ↔ p none ∧ ∀ (x : α), p (some x)
<VAR>α : Type u_1<VAR>p : Option α → Prop<GOAL>(∃ x, p x) ↔ p none ∨ ∃ x, p (some x)
<VAR>α : Type u_1<VAR>o : Option α<VAR>h : o.isSome = true<GOAL>o.get h ∈ o
<VAR>α : Type u_1<VAR>a : α<VAR>o : Option α<VAR>h : o.isSome = true<GOAL>a ∈ o → o.get h = a
<VAR>α : Type u_1<VAR>a : α<GOAL>¬a ∈ none
<VAR>α : Type u_1<VAR>x : Option α<VAR>h : x.isSome = true<GOAL>some (x.get h) = x
<VAR>α : Type u_1<VAR>x : α<VAR>h : (some x).isSome = true<GOAL>(some x).get h = x
<VAR>α : Type u_1<VAR>x : Option α<VAR>hx : x ≠ none<VAR>y : α<GOAL>some (x.getD y) = x
<VAR>α : Type u_1<VAR>o : Option α<VAR>a b : α<GOAL>o.getD a = b ↔ o = some b ∨ o = none ∧ a = b
<VAR>α : Type u_1<VAR>o : Option α<VAR>a b : α<VAR>ha : a ∈ o<VAR>hb : b ∈ o<GOAL>a = b
<VAR>α : Type u_1<VAR>o₁ o₂ : Option α<GOAL>(∀ (a : α), a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂
<GOAL>∀ {α : Type u_1} {o : Option α}, o = none ↔ ∀ (a : α), ¬a ∈ o
<VAR>α : Type u_1<GOAL>none.isSome = false
<GOAL>∀ {α : Type u_1} {a : α}, (some a).isSome = true
<GOAL>∀ {α : Type u_1} {x : Option α}, x.isSome = true ↔ ∃ a, x = some a
<VAR>α : Type u_1<GOAL>none.isNone = true
<GOAL>∀ {α : Type u_1} {a : α}, (some a).isNone = false
<GOAL>∀ {α : Type u_1} {a : Option α}, a.isSome = false ↔ a.isNone = true
<GOAL>∀ {α : Type u_1} {o : Option α} {a : α}, o = some a ↔ ∃ h, o.get h = a
<VAR>α : Type u_1<VAR>o : Option α<VAR>h : o.isSome = true<GOAL>o = some (o.get h)
<GOAL>∀ {α : Type u_1} {o : Option α}, ¬o.isSome = true ↔ o = none
<GOAL>∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ o.isSome = true
<GOAL>∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ x, some x = o
<GOAL>∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ x, o = some x
<VAR>α : Type u_1<VAR>p : Option α → Prop<GOAL>(∃ x x_1, p x) ↔ ∃ x, p (some x)
<VAR>α : Type u_1<VAR>p : Option α → Prop<GOAL>(∀ (x : Option α), x ≠ none → p x) ↔ ∀ (x : α), p (some x)
<VAR>α : Type u_1<VAR>x : Option α<GOAL>x.bind some = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : Option α<GOAL>(x.bind fun x => none) = none
<GOAL>∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1 → Option α}, x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>o : Option α<VAR>f : α → Option β<GOAL>o.bind f = none ↔ ∀ (a : α), o = some a → f a = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>o : Option α<VAR>f : α → Option β<GOAL>o.bind f = none ↔ ∀ (b : β) (a : α), a ∈ o → ¬b ∈ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → Option γ<VAR>a : Option α<VAR>b : Option β<GOAL>(a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : Option α<VAR>f : α → Option β<VAR>g : β → Option γ<GOAL>(x.bind f).bind g = x.bind fun y => (f y).bind g
<GOAL>∀ {α : Type u_1} {a : α} {x : Option (Option α)}, x.join = some a ↔ x = some (some a)
<GOAL>∀ {α : Type u_1} {x : Option (Option α)}, x.join ≠ none ↔ ∃ z, x = some (some z)
<GOAL>∀ {α : Type u_1} {x : Option (Option α)}, ¬x.join = none ↔ ∃ z, x = some (some z)
<GOAL>∀ {α : Type u_1} {o : Option (Option α)}, o.join = none ↔ o = none ∨ o = some none
<VAR>α : Type u_1<VAR>x : Option (Option α)<GOAL>x.bind id = x.join
<GOAL>∀ {α α_1 : Type u_1} {f : α → α_1}, Functor.map f = Option.map f
<GOAL>∀ {α α_1 : Type u_1} {f : α → α_1}, f <$> none = none
<GOAL>∀ {α α_1 : Type u_1} {f : α → α_1} {a : α}, f <$> some a = some (f a)
<GOAL>∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1 → α}, Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b
<GOAL>∀ {α α_1 : Type u_1} {f : α → α_1} {x : Option α} {b : α_1}, f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b
<GOAL>∀ {α : Type u_1} {x : Option α} {α_1 : Type u_2} {f : α → α_1}, Option.map f x = none ↔ x = none
<GOAL>∀ {α α_1 : Type u_1} {f : α → α_1} {x : Option α}, f <$> x = none ↔ x = none
<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_2} {f : α → α_1} {x : Option α}, Option.map f x = x.bind (some ∘ f)
<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_2} {f g : α → α_1} {x : Option α}, (∀ (a : α), a ∈ x → f a = g a) → Option.map f x = Option.map g x
<VAR>α : Type u_1<VAR>x : Option α<GOAL>Option.map (fun a => a) x = x
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>h : β → γ<VAR>g : α → β<VAR>x : Option α<GOAL>Option.map h (Option.map g x) = Option.map (h ∘ g) x
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>h : β → γ<VAR>g : α → β<VAR>x : Option α<GOAL>Option.map (h ∘ g) x = Option.map h (Option.map g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<GOAL>Option.map g ∘ Option.map f = Option.map (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>x : Option α<VAR>g : α → β<VAR>h : a ∈ x<GOAL>g a ∈ Option.map g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : Option (Option α)<VAR>f : α → β<GOAL>x.bind (Option.map f) = (Option.map (Option.map f) x).bind id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : Option (Option α)<GOAL>(Option.map (Option.map f) x).join = Option.map f x.join
<VAR>α : Type u_1<VAR>x : Option (Option (Option α))<GOAL>x.join.join = (Option.map Option.join x).join
<VAR>α : Type u_1<VAR>a : α<VAR>x : Option (Option α)<VAR>h : a ∈ x.join<GOAL>some a ∈ x
<VAR>α : Type u_1<VAR>a : α<VAR>x : Option α<GOAL>(HOrElse.hOrElse (some a) fun x_1 => x) = some a
<VAR>α : Type u_1<VAR>x : Option α<GOAL>(HOrElse.hOrElse none fun x_1 => x) = x
<VAR>α : Type u_1<VAR>x : Option α<GOAL>(HOrElse.hOrElse x fun x => none) = x
<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_2} {f : α → α_1} {x y : Option α}, Option.map f (HOrElse.hOrElse x fun x => y) = HOrElse.hOrElse (Option.map f x) fun x => Option.map f y
<GOAL>∀ {α : Type u_1} {p : α → Prop} {a b : α} [inst : DecidablePred p], Option.guard p a = some b ↔ a = b ∧ p a
<VAR>α : Type u_1<VAR>f : α → α → α<VAR>h : ∀ (a b : α), f a b = a ∨ f a b = b<VAR>o₁ o₂ : Option α<GOAL>Option.liftOrGet f o₁ o₂ = o₁ ∨ Option.liftOrGet f o₁ o₂ = o₂
<VAR>α : Type u_1<VAR>f : α → α → α<VAR>b : Option α<GOAL>Option.liftOrGet f none b = b
<VAR>α : Type u_1<VAR>f : α → α → α<VAR>a : Option α<GOAL>Option.liftOrGet f a none = a
<VAR>α : Type u_1<VAR>f : α → α → α<VAR>a b : α<GOAL>Option.liftOrGet f (some a) (some b) = some (f a b)
<VAR>β : Sort u_1<VAR>α : Type u_2<VAR>x : β<VAR>f : α → β<GOAL>none.elim x f = x
<VAR>β : Sort u_1<VAR>α : Type u_2<VAR>x : β<VAR>f : α → β<VAR>a : α<GOAL>(some a).elim x f = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<VAR>o : Option α<GOAL>(Option.map f o).getD (f x) = f (o.getD x)
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>a : α<GOAL>Option.choice α = some a
<VAR>α : Type u_1<GOAL>(Option.choice α).isSome = true ↔ Nonempty α
<VAR>α : Type u_1<VAR>a : α<GOAL>(some a).toList = [a]
<VAR>b : Nat<VAR>a : Nat<GOAL>a.min b = min a b
<VAR>a b : Nat<GOAL>min a b ≤ b
<VAR>a b : Nat<GOAL>min a b ≤ a
<VAR>a b : Nat<VAR>h : a ≤ b<GOAL>min a b = a
<VAR>a b : Nat<VAR>h : b ≤ a<GOAL>min a b = b
<VAR>a b c : Nat<GOAL>a ≤ b → a ≤ c → a ≤ min b c
<VAR>a b c : Nat<GOAL>a ≤ min b c ↔ a ≤ b ∧ a ≤ c
<VAR>a b c : Nat<GOAL>a < min b c ↔ a < b ∧ a < c
<VAR>b : Nat<VAR>a : Nat<GOAL>a.max b = max a b
<VAR>a b : Nat<GOAL>a ≤ max a b
<VAR>a b : Nat<GOAL>b ≤ max a b
<VAR>a b : Nat<GOAL>a ∣ b * a
<VAR>a b : Nat<GOAL>a ∣ a * b
<VAR>a b c : Nat<VAR>h₁ : a ∣ b<VAR>h₂ : b ∣ c<GOAL>a ∣ c
<VAR>a : Nat<VAR>h : 0 ∣ a<GOAL>a = 0
<VAR>n : Nat<GOAL>0 ∣ n ↔ n = 0
<VAR>a b c : Nat<VAR>h₁ : a ∣ b<VAR>h₂ : a ∣ c<GOAL>a ∣ b + c
<VAR>k m n : Nat<VAR>h : k ∣ m<GOAL>k ∣ n ↔ k ∣ m + n
<VAR>k m n : Nat<VAR>h : k ∣ n<GOAL>k ∣ m ↔ k ∣ m + n
<VAR>k m n : Nat<VAR>h : k ∣ n<GOAL>k ∣ m % n ↔ k ∣ m
<VAR>m n : Nat<VAR>h : 0 < n<GOAL>m ∣ n → m ≤ n
<VAR>m n : Nat<GOAL>m ∣ n → n ∣ m → m = n
<VAR>m n : Nat<VAR>H1 : m ∣ n<VAR>H2 : 0 < n<GOAL>0 < m
<VAR>n : Nat<VAR>H : n ∣ 1<GOAL>n = 1
<VAR>m n : Nat<VAR>H : m ∣ n<GOAL>n % m = 0
<VAR>m n : Nat<VAR>H : n % m = 0<GOAL>m ∣ n
<VAR>m n : Nat<GOAL>m ∣ n ↔ n % m = 0
<VAR>a b : Nat<VAR>h : ¬a ∣ b<GOAL>0 < b % a
<VAR>n m : Nat<VAR>H : n ∣ m<GOAL>n * (m / n) = m
<VAR>n m : Nat<VAR>H : n ∣ m<GOAL>m / n * n = m
<VAR>c b : Nat<VAR>a : Nat<VAR>h : c ∣ b<GOAL>a % b % c = a % c
<VAR>k m n : Nat<VAR>kpos : 0 < k<VAR>H : k * m ∣ k * n<GOAL>m ∣ n
<VAR>k m n : Nat<VAR>kpos : 0 < k<VAR>H : m * k ∣ n * k<GOAL>m ∣ n
<VAR>k m n : Nat<VAR>H : n ≤ m<VAR>h₁ : k ∣ m<VAR>h₂ : k ∣ n<GOAL>k ∣ m - n
<VAR>a b c d : Nat<GOAL>a ∣ b → c ∣ d → a * c ∣ b * d
<VAR>b c : Nat<VAR>a : Nat<VAR>h : b ∣ c<GOAL>a * b ∣ a * c
<VAR>a b : Nat<VAR>h : a ∣ b<VAR>c : Nat<GOAL>a * c ∣ b * c
<VAR>n : Nat<GOAL>n ∣ 1 ↔ n = 1
<VAR>k n : Nat<VAR>m : Nat<VAR>H : k ∣ n<GOAL>m * n / k = m * (n / k)
<VAR>n : Nat<GOAL>n ≥ 2 → n / 2 < n
<VAR>n : Nat<GOAL>n.log2 ≤ n
<VAR>a b c : Nat<GOAL>a - (b + c) = a - c - b
<VAR>a c : Nat<VAR>b d : Nat<VAR>h : b ≤ d<GOAL>a + b - (c + d) = a - (c + (d - b))
<VAR>a c : Nat<VAR>b d : Nat<VAR>h : b ≥ d<GOAL>a + b - (c + d) = a + (b - d) - c
<VAR>a : Nat<VAR>b c : Nat<VAR>h : b ≤ c<GOAL>a + b - c = a - (c - b)
<VAR>a : Nat<VAR>b c : Nat<VAR>h : b > c<GOAL>(a + b = c) = False
<VAR>a : Nat<VAR>b c : Nat<VAR>h : c > a<GOAL>(a = b + c) = False
<VAR>a c : Nat<VAR>b d : Nat<VAR>h : b ≤ d<GOAL>(a + b = c + d) = (a = c + (d - b))
<VAR>a c : Nat<VAR>b d : Nat<VAR>h : b ≥ d<GOAL>(a + b = c + d) = (a + (b - d) = c)
<VAR>a : Nat<VAR>b c : Nat<VAR>h : b ≤ c<GOAL>(a + b = c) = (a = c - b)
<VAR>a : Nat<VAR>b : Nat<VAR>c : Nat<VAR>h : c ≤ a<GOAL>(a = b + c) = (b = a - c)
<VAR>a b c d : Nat<VAR>p : (a = b) = (c = d)<GOAL>(a == b) = (c == d)
<VAR>a b : Nat<VAR>p : (a = b) = False<GOAL>(a == b) = false
<VAR>a b c d : Nat<VAR>p : (a = b) = (c = d)<GOAL>(a != b) = (c != d)
<VAR>a b : Nat<VAR>p : (a = b) = False<GOAL>(a != b) = true
<VAR>a c : Nat<VAR>b d : Nat<VAR>h : b ≤ d<GOAL>(a + b ≤ c + d) = (a ≤ c + (d - b))
<VAR>a c : Nat<VAR>b d : Nat<VAR>h : b ≥ d<GOAL>(a + b ≤ c + d) = (a + (b - d) ≤ c)
<VAR>a : Nat<VAR>b c : Nat<VAR>h : b ≤ c<GOAL>(a + b ≤ c) = (a ≤ c - b)
<VAR>a : Nat<VAR>b c : Nat<VAR>h : b > c<GOAL>(a + b ≤ c) = False
<VAR>a : Nat<VAR>b c : Nat<VAR>h : a ≤ c<GOAL>(a ≤ b + c) = True
<VAR>a : Nat<VAR>b c : Nat<VAR>h : a ≥ c<GOAL>(a ≤ b + c) = (a - c ≤ b)
<VAR>a b c : Nat<VAR>a0 : 0 < a<GOAL>a * b < a * c ↔ b < c
<VAR>a b c : Nat<VAR>a0 : 0 < a<GOAL>b * a < c * a ↔ b < c
<VAR>a b c : Nat<VAR>h : a * b < a * c<GOAL>b < c
<VAR>a b c : Nat<VAR>h : b * a < c * a<GOAL>b < c
<VAR>m n k : Nat<VAR>h : m < n * k<GOAL>m / n < k
<VAR>m n k : Nat<GOAL>m % (n * k) / n = m / n % k
<VAR>m n k : Nat<GOAL>m % (k * n) / n = m / n % k
<VAR>a b c : Nat<GOAL>a % (b * c) % b = a % b
<VAR>a b c : Nat<GOAL>a % (b * c) % c = a % c
<VAR>a b x : Nat<GOAL>x % (a * b) = x % a + a * (x / a % b)
<VAR>x b k : Nat<GOAL>x % b ^ (k + 1) = x % b ^ k + b ^ k * (x / b ^ k % b)
<VAR>a b : Nat<GOAL>compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq
<VAR>a b : Nat<GOAL>compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt
<VAR>a b : Nat<GOAL>(compare a b).swap = compare b a
<VAR>a b : Nat<GOAL>compare a b = Ordering.eq ↔ a = b
<VAR>a b : Nat<GOAL>compare a b = Ordering.lt ↔ a < b
<VAR>a b : Nat<GOAL>compare a b = Ordering.gt ↔ b < a
<VAR>a b : Nat<GOAL>compare a b ≠ Ordering.gt ↔ a ≤ b
<VAR>a b : Nat<GOAL>compare a b ≠ Ordering.lt ↔ b ≤ a
<VAR>m n : Nat<GOAL>m.lcm n = n.lcm m
<VAR>m : Nat<GOAL>Nat.lcm 0 m = 0
<VAR>m : Nat<GOAL>m.lcm 0 = 0
<VAR>m : Nat<GOAL>Nat.lcm 1 m = m
<VAR>m : Nat<GOAL>m.lcm 1 = m
<VAR>m n : Nat<GOAL>m ∣ m.lcm n
<VAR>m n : Nat<GOAL>n ∣ m.lcm n
<VAR>m n : Nat<GOAL>m.gcd n * m.lcm n = m * n
<VAR>m n k : Nat<VAR>H1 : m ∣ k<VAR>H2 : n ∣ k<GOAL>m.lcm n ∣ k
<VAR>m n k : Nat<GOAL>(m.lcm n).lcm k = m.lcm (n.lcm k)
<VAR>m n : Nat<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<GOAL>m.lcm n ≠ 0
<VAR>n power : Nat<VAR>h₁ : power > 0<VAR>h₂ : power < n<GOAL>n - power * 2 < n - power
<VAR>n : Nat<VAR>h : n.isPowerOfTwo<GOAL>(n * 2).isPowerOfTwo
<VAR>n : Nat<VAR>h : n.isPowerOfTwo<GOAL>n > 0
<VAR>n power : Nat<VAR>h₁ : power > 0<VAR>h₂ : power.isPowerOfTwo<GOAL>(Nat.nextPowerOfTwo.go n power h₁).isPowerOfTwo
<VAR>n : Nat<GOAL>n.nextPowerOfTwo.isPowerOfTwo
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : Array α<VAR>hsz : a.size = b.size<VAR>i : Nat<VAR>hi : i ≤ a.size<VAR>heqv : a.isEqvAux b hsz (fun x y => decide (x = y)) i = true<VAR>j : Nat<VAR>low : i ≤ j<VAR>high : j < a.size<GOAL>a[j] = b[j]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : Array α<GOAL>(a.isEqv b fun x y => decide (x = y)) = true → a = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : Array α<VAR>i : Nat<GOAL>a.isEqvAux a ⋯ (fun x y => decide (x = y)) i = true
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : Array α<GOAL>(a.isEqv a fun x y => decide (x = y)) = true
<VAR>y : Nat<GOAL>Nat.gcd 0 y = y
<VAR>x y : Nat<GOAL>x.succ.gcd y = (y % x.succ).gcd x.succ
<VAR>x y : Nat<GOAL>(x + 1).gcd y = (y % (x + 1)).gcd (x + 1)
<VAR>n : Nat<GOAL>Nat.gcd 1 n = 1
<VAR>n : Nat<GOAL>n.gcd 0 = n
<VAR>m n : Nat<GOAL>m.gcd n = (n % m).gcd m
<VAR>P : Nat → Nat → Prop<VAR>m n : Nat<VAR>H0 : ∀ (n : Nat), P 0 n<VAR>H1 : ∀ (m n : Nat), 0 < m → P (n % m) m → P m n<GOAL>P m n
<VAR>m n : Nat<GOAL>m.gcd n ∣ m ∧ m.gcd n ∣ n
<VAR>m n : Nat<GOAL>m.gcd n ∣ m
<VAR>m n : Nat<GOAL>m.gcd n ∣ n
<VAR>m : Nat<VAR>n : Nat<VAR>h : 0 < m<GOAL>m.gcd n ≤ m
<VAR>m : Nat<VAR>n : Nat<VAR>h : 0 < n<GOAL>m.gcd n ≤ n
<VAR>k m n : Nat<GOAL>k ∣ m → k ∣ n → k ∣ m.gcd n
<VAR>k : Nat<VAR>m n : Nat<GOAL>k ∣ m.gcd n ↔ k ∣ m ∧ k ∣ n
<VAR>m n : Nat<GOAL>m.gcd n = n.gcd m
<VAR>m n : Nat<GOAL>m ∣ n ↔ m.gcd n = m
<VAR>m n : Nat<GOAL>m ∣ n ↔ n.gcd m = m
<VAR>m n k : Nat<GOAL>(m.gcd n).gcd k = m.gcd (n.gcd k)
<VAR>n : Nat<GOAL>n.gcd 1 = 1
<VAR>m n k : Nat<GOAL>(m * n).gcd (m * k) = m * n.gcd k
<VAR>m n k : Nat<GOAL>(m * n).gcd (k * n) = m.gcd k * n
<VAR>m : Nat<VAR>n : Nat<VAR>mpos : 0 < m<GOAL>0 < m.gcd n
<VAR>m : Nat<VAR>n : Nat<VAR>npos : 0 < n<GOAL>0 < m.gcd n
<VAR>a : Nat<VAR>b : Nat<VAR>h : 0 < a<GOAL>0 < a / a.gcd b
<VAR>b : Nat<VAR>a : Nat<VAR>h : 0 < b<GOAL>0 < b / a.gcd b
<VAR>m n : Nat<VAR>H : m.gcd n = 0<GOAL>m = 0
<VAR>m n : Nat<VAR>H : m.gcd n = 0<GOAL>n = 0
<VAR>m n : Nat<GOAL>m ≠ 0 → m.gcd n ≠ 0
<VAR>n m : Nat<GOAL>n ≠ 0 → m.gcd n ≠ 0
<VAR>m n k : Nat<VAR>H1 : k ∣ m<VAR>H2 : k ∣ n<GOAL>(m / k).gcd (n / k) = m.gcd n / k
<VAR>m k : Nat<VAR>n : Nat<VAR>H : m ∣ k<GOAL>m.gcd n ∣ k.gcd n
<VAR>m k : Nat<VAR>n : Nat<VAR>H : m ∣ k<GOAL>n.gcd m ∣ n.gcd k
<VAR>m n k : Nat<GOAL>m.gcd n ∣ (k * m).gcd n
<VAR>m n k : Nat<GOAL>m.gcd n ∣ (m * k).gcd n
<VAR>m n k : Nat<GOAL>m.gcd n ∣ m.gcd (k * n)
<VAR>m n k : Nat<GOAL>m.gcd n ∣ m.gcd (n * k)
<VAR>m n : Nat<VAR>H : m ∣ n<GOAL>m.gcd n = m
<VAR>m n : Nat<VAR>H : n ∣ m<GOAL>m.gcd n = n
<VAR>m n : Nat<GOAL>(m * n).gcd n = n
<VAR>m n : Nat<GOAL>n.gcd (m * n) = n
<VAR>m n : Nat<GOAL>(n * m).gcd n = n
<VAR>m n : Nat<GOAL>n.gcd (n * m) = n
<VAR>m n : Nat<GOAL>m.gcd (m.gcd n) = m.gcd n
<VAR>m n : Nat<GOAL>m.gcd (n.gcd m) = n.gcd m
<VAR>m n : Nat<GOAL>(n.gcd m).gcd m = n.gcd m
<VAR>m n : Nat<GOAL>(m.gcd n).gcd m = m.gcd n
<VAR>m n k : Nat<GOAL>m.gcd (n + k * m) = m.gcd n
<VAR>i j : Nat<GOAL>i.gcd j = 0 ↔ i = 0 ∧ j = 0
<VAR>g : Nat<VAR>a b : Nat<GOAL>a.gcd b = g ↔ g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
<VAR>k m n : Nat<GOAL>k.gcd (m * n) ∣ k.gcd m * k.gcd n
<VAR>α : Type u_1<VAR>a b : α<VAR>as bs : Array α<VAR>h : as.push a = bs.push b<GOAL>as = bs ∧ a = b
<VAR>α : Type u_1<VAR>as : List α<VAR>bs : Array α<GOAL>(as.toArrayAux bs).size = as.length + bs.size
<VAR>α : Type u_1<VAR>as bs : List α<VAR>cs ds : Array α<VAR>h : as.toArrayAux cs = bs.toArrayAux ds<VAR>hlen : cs.size = ds.size<GOAL>as = bs ∧ cs = ds
<VAR>α : Type u_1<VAR>as bs : List α<GOAL>(List.toArray as = List.toArray bs) = (as = bs)
<VAR>x y : Nat<GOAL>x.add y = x + y
<VAR>x y : Nat<GOAL>x.mul y = x * y
<VAR>x y : Nat<GOAL>x.sub y = x - y
<VAR>x y : Nat<GOAL>x.lt y = (x < y)
<VAR>x y : Nat<GOAL>x.le y = (x ≤ y)
<VAR>x y : Nat<GOAL>(x.beq y = true) = (x = y)
<VAR>x y : Nat<GOAL>(x.ble y = true) = (x ≤ y)
<VAR>x y : Nat<GOAL>(x.blt y = true) = (x < y)
<VAR>a b : Nat<GOAL>((a == b) = true) = (a = b)
<VAR>a b : Nat<GOAL>((!a == b) = true) = ¬a = b
<VAR>n m : Nat<GOAL>n.succ + m = (n + m).succ
<VAR>n m : Nat<GOAL>n + m.succ = (n + m).succ
<VAR>n : Nat<GOAL>n + 1 = n.succ
<VAR>n : Nat<GOAL>n.succ = n + 1
<VAR>n : Nat<GOAL>n + 1 ≠ 0
<VAR>n : Nat<GOAL>0 ≠ n + 1
<VAR>n m k : Nat<GOAL>n + m + k = n + (m + k)
<VAR>n m k : Nat<GOAL>n + (m + k) = m + (n + k)
<VAR>n m k : Nat<GOAL>n + m + k = n + k + m
<VAR>n m k : Nat<GOAL>n + m = n + k → m = k
<VAR>n m k : Nat<VAR>h : n + m = k + m<GOAL>n = k
<VAR>n m : Nat<GOAL>n + m = 0 → n = 0 ∧ m = 0
<VAR>n m : Nat<VAR>h : n + m = 0<GOAL>m = 0
<VAR>n m : Nat<GOAL>n * m.succ = n * m + n
<VAR>n m : Nat<GOAL>n * (m + 1) = n * m + n
<VAR>n m : Nat<GOAL>n.succ * m = n * m + m
<VAR>n m : Nat<GOAL>(n + 1) * m = n * m + m
<VAR>n m k : Nat<GOAL>n * (m + k) = n * m + n * k
<VAR>n m k : Nat<GOAL>(n + m) * k = n * k + m * k
<VAR>n m k : Nat<GOAL>n * m * k = n * (m * k)
<VAR>n m k : Nat<GOAL>n * (m * k) = m * (n * k)
<VAR>n : Nat<GOAL>n * 2 = n + n
<VAR>n m : Nat<GOAL>n < m → n.succ < m.succ
<VAR>n m : Nat<GOAL>n ≤ m → n < m.succ
<VAR>n m : Nat<GOAL>n < m + 1 → n ≤ m
<VAR>n m : Nat<GOAL>n ≤ m → n < m + 1
<VAR>n : Nat<GOAL>¬n + 1 ≤ 0
<VAR>n : Nat<GOAL>¬n + 1 ≤ n
<VAR>n m : Nat<GOAL>n.succ - m.succ = n - m
<VAR>n : Nat<GOAL>n ≠ 0 → n.pred < n
<VAR>n : Nat<GOAL>n ≠ 0 → n - 1 < n
<VAR>n m : Nat<GOAL>n - m ≤ n
<VAR>n m : Nat<GOAL>0 < n → 0 < m → n - m < n
<VAR>n m : Nat<GOAL>n - m.succ = (n - m).pred
<VAR>a b c : Nat<GOAL>a - (b + c) = a - b - c
<VAR>n m k : Nat<GOAL>n < m → m ≤ k → n < k
<VAR>n m k : Nat<GOAL>n < m → m = k → n < k
<VAR>n m : Nat<VAR>p : n = m<GOAL>n ≤ m
<VAR>n m : Nat<GOAL>n < m → n < m.succ
<VAR>n m : Nat<VAR>h : n.succ ≤ m<GOAL>n ≤ m
<VAR>n m : Nat<GOAL>n.succ < m → n < m
<VAR>n m : Nat<GOAL>n < m → n ≤ m
<VAR>n m : Nat<GOAL>n.succ < m.succ → n < m
<VAR>n m : Nat<VAR>h : n.succ ≤ m<GOAL>n < m
<VAR>n m : Nat<VAR>h : n < m<GOAL>n.succ ≤ m
<VAR>n : Nat<GOAL>n = 0 ∨ n > 0
<VAR>n : Nat<GOAL>n ≠ 0 → 0 < n
<VAR>m n : Nat<GOAL>m ≤ n ∨ n ≤ m
<VAR>n : Nat<VAR>h : n ≤ 0<GOAL>n = 0
<VAR>a b : Nat<GOAL>a < b → 0 < b
<VAR>a : Nat<VAR>h : a ≠ 0<GOAL>0 < a
<VAR>a b : Nat<VAR>h : a < b<GOAL>a ≠ b
<VAR>m n : Nat<VAR>h : m ≤ n.succ<GOAL>m ≤ n ∨ m = n.succ
<VAR>m n : Nat<VAR>h : m ≤ n + 1<GOAL>m ≤ n ∨ m = n + 1
<VAR>n k : Nat<GOAL>n ≤ n + k
<VAR>n m : Nat<GOAL>n ≤ m + n
<VAR>n m k : Nat<VAR>h : n + k ≤ m<GOAL>n ≤ m
<VAR>n m k : Nat<VAR>h : n ≤ m<GOAL>n ≤ m + k
<VAR>n m : Nat<VAR>h : n + 1 ≤ m<GOAL>n < m
<VAR>n m : Nat<VAR>h : n < m<GOAL>n + 1 ≤ m
<VAR>a b : Nat<VAR>c : Nat<VAR>h : a < b<GOAL>a < c + b
<VAR>a b : Nat<VAR>c : Nat<VAR>h : a < b<GOAL>a < b + c
<VAR>n m k : Nat<VAR>h : n + k < m<GOAL>n < m
<VAR>n m : Nat<GOAL>n ≤ m → Exists fun k => n + k = m
<VAR>n m k : Nat<VAR>h : n + k = m<GOAL>n ≤ m
<VAR>n m : Nat<VAR>h : n > m<GOAL>¬n ≤ m
<VAR>a b : Nat<GOAL>a < b → ¬b ≤ a
<VAR>a b : Nat<GOAL>b ≥ a → ¬b < a
<VAR>a b : Nat<GOAL>a ≤ b → ¬b < a
<VAR>n m : Nat<VAR>h : ¬n ≤ m<GOAL>n > m
<VAR>a b : Nat<GOAL>¬b ≥ a → b < a
<VAR>a b : Nat<GOAL>¬a ≤ b → b < a
<VAR>n m : Nat<VAR>h : ¬n < m<GOAL>n ≥ m
<VAR>a b : Nat<GOAL>¬b > a → b ≤ a
<VAR>a b : Nat<GOAL>¬a < b → b ≤ a
<VAR>a b : Nat<VAR>h : b < a<GOAL>a ≠ b
<VAR>a b : Nat<GOAL>a < b → b ≠ a
<VAR>a b : Nat<GOAL>¬a ≤ b ↔ b < a
<VAR>a b : Nat<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : Nat<VAR>h : ¬b ≤ a<GOAL>a ≤ b
<VAR>a b : Nat<GOAL>¬a ≥ b → a ≤ b
<VAR>a b : Nat<GOAL>a < b ∨ a = b ∨ b < a
<VAR>a b : Nat<VAR>ne : a ≠ b<GOAL>a < b ∨ a > b
<VAR>a b : Nat<GOAL>a ≠ b → a < b ∨ b < a
<VAR>a b : Nat<GOAL>a = b ↔ a ≤ b ∧ b ≤ a
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>k : Nat<GOAL>k + n ≤ k + m
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>k : Nat<GOAL>n + k ≤ m + k
<VAR>n m : Nat<VAR>h : n < m<VAR>k : Nat<GOAL>k + n < k + m
<VAR>n m : Nat<VAR>h : n < m<VAR>k : Nat<GOAL>n + k < m + k
<VAR>k n : Nat<VAR>h : 0 < k<GOAL>n < n + k
<VAR>n : Nat<GOAL>0 < n ↔ n ≠ 0
<VAR>a b c d : Nat<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a + c ≤ b + d
<VAR>a b c d : Nat<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>a b c : Nat<VAR>h : a + b ≤ a + c<GOAL>b ≤ c
<VAR>a b c : Nat<GOAL>a + b ≤ c + b → a ≤ c
<VAR>m k n : Nat<GOAL>m + n ≤ k + n ↔ m ≤ k
<VAR>a b : Nat<VAR>h : a < b<GOAL>¬b < a
<VAR>m n : Nat<GOAL>m < n ↔ m ≤ n ∧ ¬n ≤ m
<VAR>m n : Nat<GOAL>m < n ↔ m ≤ n ∧ m ≠ n
<VAR>a b : Nat<GOAL>a ≠ b ↔ a < b ∨ b < a
<VAR>a b : Nat<VAR>hnlt : ¬a < b<GOAL>a = b ∨ b < a
<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>n < m ∨ n = m
<VAR>n m : Nat<GOAL>n ≤ m ↔ n < m ∨ n = m
<VAR>m n : Nat<GOAL>m < n.succ ↔ m ≤ n
<VAR>m n : Nat<GOAL>m < n + 1 ↔ m ≤ n
<VAR>m n : Nat<GOAL>m < n.succ ↔ m < n ∨ m = n
<VAR>m n : Nat<GOAL>m < n + 1 ↔ m < n ∨ m = n
<VAR>m n : Nat<VAR>hmn : m < n + 1<VAR>h : ¬m < n<GOAL>m = n
<VAR>n m : Nat<VAR>h₁ : n ≤ m<VAR>h₂ : m < n + 1<GOAL>m = n
<VAR>i : Nat<GOAL>i ≤ 0 ↔ i = 0
<VAR>n : Nat<GOAL>n ≠ 0 ↔ 0 < n
<VAR>n : Nat<VAR>h : ¬0 < n<GOAL>n = 0
<VAR>n : Nat<GOAL>n.succ ≠ n
<VAR>n : Nat<GOAL>n + 1 ≠ n
<VAR>n m : Nat<GOAL>n.succ ≤ m ↔ n < m
<VAR>n m : Nat<GOAL>n + 1 ≤ m ↔ n < m
<VAR>a b : Nat<VAR>h : a < b<GOAL>a < b.succ
<VAR>a b : Nat<VAR>h : a < b<GOAL>a < b + 1
<VAR>n : Nat<GOAL>n ≠ 0 → n.pred.succ = n