ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Fintype α<GOAL>⇑Fintype.finsetOrderIsoSet.symm = ⇑Fintype.finsetEquivSet.symm
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>b : β<GOAL>b ∈ Finset.image f Finset.univ ↔ b ∈ Set.range f
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∃! a, p a<GOAL>p (Fintype.choose p hp)
<VAR>α : Type u_4<VAR>p : α → Prop<VAR>Fintype { a // p a }<VAR>DecidableEq α<VAR>x : { a // p a }<VAR>h : ∃! a, ↑a = ↑x := ⋯<GOAL>Fintype.choose (fun y => ↑y = ↑x) h = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>f_bij : Function.Bijective f<GOAL>Function.LeftInverse (Fintype.bijInv f_bij) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>f_bij : Function.Bijective f<GOAL>Function.RightInverse (Fintype.bijInv f_bij) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>f_bij : Function.Bijective f<GOAL>Function.Bijective (Fintype.bijInv f_bij)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.count a Finset.univ.val = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>e : α ≃ β<GOAL>Multiset.map (⇑e) Finset.univ.val = Finset.univ.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<GOAL>Function.Bijective f ↔ Multiset.map f Finset.univ.val = Finset.univ.val
<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<GOAL>∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>IsSymm α r<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<GOAL>∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise fun m n => r (f m) (f n)
<VAR>α : Type u_1<VAR>x : LazyList α<GOAL>x.bind LazyList.singleton = x
<GOAL>⇑Equiv.pnatEquivNat = PNat.natPred
<GOAL>⇑Equiv.pnatEquivNat.symm = Nat.succPNat
<VAR>α : Type u_1<GOAL>(fun a => some a) = some
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>y : β<VAR>o : Option α<GOAL>y ∈ Option.map f o ↔ ∃ x, x ∈ o ∧ f x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>H : Function.Injective f<VAR>a : α<VAR>o : Option α<GOAL>f a ∈ Option.map f o ↔ a ∈ o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Option α<VAR>p : β → Prop<GOAL>(∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Option α<VAR>p : β → Prop<GOAL>(∃ y, y ∈ Option.map f o ∧ p y) ↔ ∃ x, x ∈ o ∧ p (f x)
<VAR>α : Type u_1<VAR>o : Option α<VAR>h : o.isSome = true<GOAL>some (o.get h) = o
<VAR>α : Type u_1<VAR>a : α<VAR>o1 o2 : Option α<VAR>h1 : a ∈ o1<VAR>h2 : a ∈ o2<GOAL>o1 = o2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Hf : Function.Injective f<GOAL>Function.Injective (Option.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Option.map f ∘ some = some ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : Option α<VAR>f : α → Option β<VAR>b : β<GOAL>x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → Option β<VAR>x : Option α<VAR>h : ∀ (a : α), a ∈ x → f a = g a<GOAL>x.bind f = x.bind g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → Option β<VAR>x y : Option α<VAR>hx : x = y<VAR>hf : ∀ (a : α), a ∈ y → f a = g a<GOAL>x.bind f = y.bind g
<VAR>α β : Type u<VAR>f : α → Option β<VAR>x : Option α<GOAL>x >>= f = x.bind f
<VAR>α β : Type u_5<VAR>a : α<VAR>f : α → β<GOAL>f <$> some a = some (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Injective Option.map
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<GOAL>Option.map f = Option.map g ↔ f = g
<VAR>α : Type u_1<VAR>f : α → α<GOAL>Option.map f = id ↔ f = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>x : Option α<GOAL>(x.pbind fun a x => f a) = x.bind f
<VAR>α β γ : Type u_5<VAR>f : β → γ<VAR>x : Option α<VAR>g : α → Option β<GOAL>Option.map f (x >>= g) = do let a ← x Option.map f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → γ<VAR>x : Option α<VAR>g : α → Option β<GOAL>Option.map f (x.bind g) = x.bind fun a => Option.map f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → γ<VAR>x : Option α<VAR>g : (a : α) → a ∈ x → Option β<GOAL>Option.map f (x.pbind g) = x.pbind fun a H => Option.map f (g a H)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>x : Option α<VAR>g : (b : β) → b ∈ Option.map f x → Option γ<GOAL>(Option.map f x).pbind g = x.pbind fun a h => g (f a) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>H : ∀ (a : α), a ∈ none → p a<GOAL>Option.pmap f none H = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : α<VAR>h : p x<GOAL>Option.pmap f (some x) = fun x_1 => some (f x h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>a : α<VAR>h : ∀ (a : α), a ∈ x → p a<VAR>ha : a ∈ x<GOAL>f a ⋯ ∈ Option.pmap f x h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>g : γ → α<VAR>x : Option γ<VAR>H : ∀ (a : α), a ∈ Option.map g x → p a<GOAL>Option.pmap f (Option.map g x) H = Option.pmap (fun a h => f (g a) h) x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>g : β → γ<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>H : ∀ (a : α), a ∈ x → p a<GOAL>Option.map g (Option.pmap f x H) = Option.pmap (fun a h => g (f a h)) x H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : α → β<VAR>x : Option α<VAR>H : ∀ (a : α), a ∈ x → p a<GOAL>Option.pmap (fun a x => f a) x H = Option.map f x
<VAR>α β γ : Type u_5<VAR>x : Option α<VAR>g : α → Option β<VAR>p : β → Prop<VAR>f : (b : β) → p b → γ<VAR>H : ∀ (a : β), a ∈ x >>= g → p a<VAR>H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g<GOAL>Option.pmap f (x >>= g) H = do let a ← x Option.pmap f (g a) ⋯
<VAR>α : Type u_5<VAR>β γ : Type u_6<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>g : β → Option γ<VAR>H : ∀ (a : α), a ∈ x → p a<GOAL>Option.pmap f x H >>= g = x.pbind fun a h => g (f a ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : Option α<VAR>f : (a : α) → a ∈ x → Option β<VAR>h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none<GOAL>x.pbind f = none ↔ x = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : Option α<VAR>f : (a : α) → a ∈ x → Option β<VAR>y : β<GOAL>x.pbind f = some y ↔ ∃ z H, f z H = some y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>h : ∀ (a : α), a ∈ x → p a<GOAL>Option.pmap f x h = none ↔ x = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>hf : ∀ (a : α), a ∈ x → p a<VAR>y : β<GOAL>Option.pmap f x hf = some y ↔ ∃ a H, f a ⋯ = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option (Option α)<VAR>H : ∀ (a : Option α), a ∈ x → ∀ (a_2 : α), a_2 ∈ a → p a_2<GOAL>(Option.pmap (Option.pmap f) x H).join = Option.pmap f x.join ⋯
<VAR>α β : Type u_5<VAR>a : α<VAR>f : α → β<GOAL>(Seq.seq (some f) fun x => some a) = some (f a)
<VAR>α : Type u_1<VAR>a : α<VAR>x : Option α<GOAL>((some a).orElse fun x_1 => x) = some a
<VAR>α : Type u_1<VAR>x : Option α<GOAL>(none.orElse fun x_1 => x) = x
<VAR>α : Type u_1<VAR>x : Option α<GOAL>(x.orElse fun x => none) = x
<VAR>α : Type u_1<VAR>p : Option α → Prop<GOAL>(∃ x, x ≠ none ∧ p x) ↔ ∃ x, p (some x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Option α<GOAL>(Option.map f o).isSome = o.isSome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Option α<VAR>h : (Option.map f o).isSome = true<GOAL>(Option.map f o).get h = f (o.get ⋯)
<VAR>α : Type u_1<VAR>Inhabited α<VAR>o : Option α<GOAL>o.isSome = true → o.iget ∈ o
<VAR>α : Type u_1<VAR>Inhabited α<VAR>a : α<VAR>o : Option α<GOAL>a ∈ o → o.iget = a
<VAR>α : Type u_1<VAR>Inhabited α<VAR>o : Option α<GOAL>o.getD default = o.iget
<VAR>p : Prop<VAR>Decidable p<VAR>u : Unit<GOAL>guard p = some u ↔ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<VAR>f : α → β<GOAL>none.casesOn' x f = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<VAR>f : α → β<VAR>a : α<GOAL>(some a).casesOn' x f = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<VAR>o : Option α<GOAL>o.casesOn' (f none) (f ∘ fun a => some a) = f o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>f : α → β<VAR>a : Option α<GOAL>a.casesOn' b f = a.elim b f
<VAR>α : Type u_1<VAR>o o' : Option α<VAR>x : α<GOAL>(HOrElse.hOrElse o fun x => o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
<VAR>α : Type u_1<VAR>o o' : Option α<VAR>x : α<GOAL>(o.orElse fun x => o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
<VAR>α : Type u_1<VAR>o o' : Option α<GOAL>(HOrElse.hOrElse o fun x => o') = none ↔ o = none ∧ o' = none
<VAR>α : Type u_1<VAR>o o' : Option α<GOAL>(o.orElse fun x => o') = none ↔ o = none ∧ o' = none
<VAR>α : Type u_5<VAR>IsEmpty α<GOAL>Option.choice α = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<GOAL>(fun x => x.elim (f none) (f ∘ some)) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>h : α → β<VAR>f : γ → α<VAR>x : α<VAR>i : Option γ<GOAL>(i.elim (h x) fun j => h (f j)) = h (i.elim x f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>h : α → β → γ<VAR>f : γ → α<VAR>x : α<VAR>g : γ → β<VAR>y : β<VAR>i : Option γ<GOAL>(i.elim (h x y) fun j => h (f j) (g j)) = h (i.elim x f) (i.elim y g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : γ → α → β<VAR>x : α → β<VAR>i : Option γ<VAR>y : α<GOAL>i.elim x f y = i.elim (x y) fun j => f j y
<VAR>α : Type u_1<VAR>Inhabited α<VAR>a : α<GOAL>(some a).get! = a
<VAR>α : Type u_1<VAR>Inhabited α<GOAL>none.get! = default
<VAR>α : Type u_1<VAR>a : Option α<GOAL>(!a.isSome) = a.isNone
<VAR>α : Type u_1<GOAL>(fun x => !x) ∘ Option.isSome = Option.isNone
<VAR>α : Type u_1<VAR>a : Option α<GOAL>(!a.isNone) = a.isSome
<VAR>α : Type u_1<GOAL>(fun x => !x) ∘ Option.isNone = Option.isSome
<VAR>α : Type u_1<VAR>a : Option α<GOAL>a.isNone = false ↔ a.isSome = true
<VAR>α : Type u_1<VAR>a : Option α<GOAL>a = none ∨ ∃ x, a = some x
<VAR>α : Type u_1<VAR>o : Option α<GOAL>(∀ (x : α), some x ≠ o) ↔ o = none
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>(permsOfList l).length = l.length !
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>f : Equiv.Perm α<VAR>h : ∀ (x : α), f x ≠ x → x ∈ l<GOAL>f ∈ permsOfList l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>f : Equiv.Perm α<GOAL>f ∈ permsOfList l → ∀ (x : α), f x ≠ x → x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>f : Equiv.Perm α<GOAL>f ∈ permsOfList l ↔ ∀ {x : α}, f x ≠ x → x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.Nodup → (permsOfList l).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : Equiv.Perm α<GOAL>f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(permsOfFinset s).card = s.card !
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Fintype.card (Equiv.Perm α) = (Fintype.card α)!
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>e : α ≃ β<GOAL>Fintype.card (α ≃ β) = (Fintype.card α)!
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>κ : ι → Type u_5<VAR>(i : ι) → Fintype (κ i)<VAR>s : Finset ι<VAR>f : Sigma κ → Set α<GOAL>⋃ ij ∈ s.sigma fun x => Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>κ : ι → Type u_5<VAR>(i : ι) → Fintype (κ i)<VAR>s : Finset ι<VAR>f : (i : ι) → κ i → Set α<GOAL>⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>κ : ι → Type u_5<VAR>(i : ι) → Fintype (κ i)<VAR>s : Finset ι<VAR>f : Sigma κ → Set α<GOAL>⋂ ij ∈ s.sigma fun x => Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>κ : ι → Type u_5<VAR>(i : ι) → Fintype (κ i)<VAR>s : Finset ι<VAR>f : (i : ι) → κ i → Set α<GOAL>⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>κ : ι → Type u_5<VAR>(i : ι) → Fintype (κ i)<VAR>Fintype ι<GOAL>(Finset.univ.sigma fun x => Finset.univ) = Finset.univ
<VAR>a b : ℕ+<GOAL>Finset.Icc a b = Finset.subtype (fun n => 0 < n) (Finset.Icc ↑a ↑b)
<VAR>a b : ℕ+<GOAL>Finset.Ico a b = Finset.subtype (fun n => 0 < n) (Finset.Ico ↑a ↑b)
<VAR>a b : ℕ+<GOAL>Finset.Ioc a b = Finset.subtype (fun n => 0 < n) (Finset.Ioc ↑a ↑b)
<VAR>a b : ℕ+<GOAL>Finset.Ioo a b = Finset.subtype (fun n => 0 < n) (Finset.Ioo ↑a ↑b)
<VAR>a b : ℕ+<GOAL>Finset.uIcc a b = Finset.subtype (fun n => 0 < n) (Finset.uIcc ↑a ↑b)
<VAR>a b : ℕ+<GOAL>Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Icc a b) = Finset.Icc ↑a ↑b
<VAR>a b : ℕ+<GOAL>Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ico a b) = Finset.Ico ↑a ↑b
<VAR>a b : ℕ+<GOAL>Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
<VAR>a b : ℕ+<GOAL>Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
<VAR>a b : ℕ+<GOAL>Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
<VAR>a b : ℕ+<GOAL>(Finset.Icc a b).card = ↑b + 1 - ↑a
<VAR>a b : ℕ+<GOAL>(Finset.Ico a b).card = ↑b - ↑a
<VAR>a b : ℕ+<GOAL>(Finset.Ioc a b).card = ↑b - ↑a
<VAR>a b : ℕ+<GOAL>(Finset.Ioo a b).card = ↑b - ↑a - 1
<VAR>a b : ℕ+<GOAL>(Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
<VAR>n : ℕ<GOAL>SuccOrder.succ = fun a => if a < Fin.last n then a + 1 else a
<VAR>n : ℕ<VAR>a : Fin (n + 1)<GOAL>SuccOrder.succ a = if a < Fin.last n then a + 1 else a
<VAR>n : ℕ<GOAL>PredOrder.pred = fun a => if a = 0 then 0 else a - 1
<VAR>n : ℕ<VAR>a : Fin (n + 1)<GOAL>PredOrder.pred a = if a = 0 then 0 else a - 1
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>↑⟨n, h⟩ = n
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>PNat.natPred ⟨n, h⟩ = n.pred
<VAR>n : ℕ<GOAL>↑n.succPNat = n.succ
<VAR>n : ℕ<GOAL>n.succPNat.natPred = n
<VAR>n : ℕ+<GOAL>n.natPred.succPNat = n
<VAR>n : ℕ<GOAL>↑n.toPNat' = if 0 < n then n else 1
<VAR>n k : ℕ<VAR>hn : 0 < n<VAR>hk : 0 < k<GOAL>⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k
<VAR>n k : ℕ<VAR>hn : 0 < n<VAR>hk : 0 < k<GOAL>⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k
<VAR>n k : ℕ+<GOAL>↑n ≤ ↑k ↔ n ≤ k
<VAR>n k : ℕ+<GOAL>↑n < ↑k ↔ n < k
<VAR>n : ℕ+<GOAL>0 < ↑n
<VAR>m n : ℕ+<GOAL>↑m = ↑n → m = n
<VAR>n : ℕ+<GOAL>↑n ≠ 0
<VAR>n : ℕ<GOAL>0 < n → ↑n.toPNat' = n
<VAR>n : ℕ+<GOAL>(↑n).toPNat' = n
<VAR>n : ℕ+<GOAL>1 ≤ n
<VAR>n : ℕ+<GOAL>¬n < 1
<VAR>h : 0 < 1<GOAL>⟨1, h⟩ = 1
<VAR>m : ℕ+<GOAL>↑m = 1 ↔ m = 1
<VAR>m k : ℕ+<GOAL>↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
<VAR>m k : ℕ+<GOAL>m.div k = if ↑m % ↑k = 0 then (↑m / ↑k).pred else ↑m / ↑k
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>p (PNat.find h)
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>m : ℕ+<GOAL>m < PNat.find h → ¬p m
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>m : ℕ+<VAR>hm : p m<GOAL>PNat.find h ≤ m
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>m : ℕ+<GOAL>PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ+<GOAL>PNat.find h < n ↔ ∃ m < n, p m
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ+<GOAL>PNat.find h ≤ n ↔ ∃ m ≤ n, p m
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ+<GOAL>n ≤ PNat.find h ↔ ∀ m < n, ¬p m
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ+<GOAL>n < PNat.find h ↔ ∀ m ≤ n, ¬p m
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>PNat.find h = 1 ↔ p 1
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>1 < PNat.find h ↔ ¬p 1
<VAR>p q : ℕ+ → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>h : ∀ (n : ℕ+), q n → p n<VAR>hp : ∃ n, p n<VAR>hq : ∃ n, q n<GOAL>PNat.find hp ≤ PNat.find hq
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>n : ℕ+<VAR>h : ∃ n, p n<VAR>hn : p n<GOAL>PNat.find h ≤ n
<VAR>p : ℕ+ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h1 : ¬p 1<GOAL>PNat.find h = PNat.find h₂ + 1
<VAR>F : Type u → Type u<VAR>self : QPF F<VAR>α β : Type u<VAR>f : α → β<VAR>p : ↑(QPF.P F) α<GOAL>QPF.abs ((QPF.P F).map f p) = f <$> QPF.abs p
<VAR>F : Type u → Type u<VAR>self : QPF F<VAR>α : Type u<VAR>x : F α<GOAL>QPF.abs (QPF.repr x) = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α β γ : Type u<VAR>f : α → β<VAR>g : β → γ<VAR>x : F α<GOAL>(g ∘ f) <$> x = g <$> f <$> x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : ∀ (α β : Type u), Functor.mapConst = Functor.map ∘ Function.const β<GOAL>LawfulFunctor F
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<GOAL>Functor.Liftp p x ↔ ∃ a f, x = QPF.abs ⟨a, f⟩ ∧ ∀ (i : (QPF.P F).B a), p (f i)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<GOAL>Functor.Liftp p x ↔ ∃ u, QPF.abs u = x ∧ ∀ (i : (QPF.P F).B u.fst), p (u.snd i)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : F α<GOAL>Functor.Liftr r x y ↔ ∃ a f₀ f₁, x = QPF.abs ⟨a, f₀⟩ ∧ y = QPF.abs ⟨a, f₁⟩ ∧ ∀ (i : (QPF.P F).B a), r (f₀ i) (f₁ i)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>x : (QPF.P F).W<GOAL>QPF.recF g x = g (QPF.abs ((QPF.P F).map (QPF.recF g) x.dest))
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>a : (QPF.P F).A<VAR>f : (QPF.P F).B a → (QPF.P F).W<GOAL>QPF.recF g (WType.mk a f) = g (QPF.abs ((QPF.P F).map (QPF.recF g) ⟨a, f⟩))
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>u : F α → α<VAR>x y : (QPF.P F).W<GOAL>QPF.Wequiv x y → QPF.recF u x = QPF.recF u y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x y : (QPF.P F).W<VAR>h : QPF.abs x.dest = QPF.abs y.dest<GOAL>QPF.Wequiv x y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : (QPF.P F).W<GOAL>QPF.Wequiv x x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x y : (QPF.P F).W<GOAL>QPF.Wequiv x y → QPF.Wequiv y x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : (QPF.P F).W<GOAL>QPF.Wequiv (QPF.Wrepr x) x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>x : F (QPF.Fix F)<GOAL>QPF.Fix.rec g (QPF.Fix.mk x) = g (QPF.Fix.rec g <$> x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>a : (QPF.P F).A<VAR>f : (QPF.P F).B a → (QPF.P F).W<GOAL>QPF.Fix.mk (QPF.abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g₁ g₂ : QPF.Fix F → α<VAR>h : ∀ (x : F (QPF.Fix F)), g₁ <$> x = g₂ <$> x → g₁ (QPF.Fix.mk x) = g₂ (QPF.Fix.mk x)<VAR>x : QPF.Fix F<GOAL>g₁ x = g₂ x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>h : QPF.Fix F → α<VAR>hyp : ∀ (x : F (QPF.Fix F)), h (QPF.Fix.mk x) = g (h <$> x)<GOAL>QPF.Fix.rec g = h
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : QPF.Fix F<GOAL>QPF.Fix.mk x.dest = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : F (QPF.Fix F)<GOAL>(QPF.Fix.mk x).dest = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>p : QPF.Fix F → Prop<VAR>h : ∀ (x : F (QPF.Fix F)), Functor.Liftp p x → p (QPF.Fix.mk x)<VAR>x : QPF.Fix F<GOAL>p x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : α → F α<VAR>x : α<GOAL>(QPF.corecF g x).dest = (QPF.P F).map (QPF.corecF g) (QPF.repr (g x))
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : α → F α<VAR>x : α<GOAL>(QPF.Cofix.corec g x).dest = QPF.Cofix.corec g <$> g x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : QPF.Cofix F → QPF.Cofix F → Prop<VAR>h' : ∀ (x : QPF.Cofix F), r x x<VAR>h : ∀ (x y : QPF.Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>x y : QPF.Cofix F<GOAL>r x y → x = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : QPF.Cofix F → QPF.Cofix F → Prop<VAR>h : ∀ (x y : QPF.Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>x y : QPF.Cofix F<GOAL>r x y → x = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : QPF.Cofix F → QPF.Cofix F → Prop<VAR>h : ∀ (x y : QPF.Cofix F), r x y → Functor.Liftr r x.dest y.dest<VAR>x y : QPF.Cofix F<GOAL>r x y → x = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u_1<VAR>Q : α → Prop<VAR>u v : α → QPF.Cofix F<VAR>h : ∀ (x : α), Q x → ∃ a f f', (u x).dest = QPF.abs ⟨a, f⟩ ∧ (v x).dest = QPF.abs ⟨a, f'⟩ ∧ ∀ (i : (QPF.P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'<VAR>x : α<GOAL>Q x → u x = v x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>u : α<GOAL>u ∈ Functor.supp x ↔ ∀ (a : (QPF.P F).A) (f : (QPF.P F).B a → α), QPF.abs ⟨a, f⟩ = x → u ∈ f '' Set.univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<GOAL>Functor.supp x = {u | ∀ (a : (QPF.P F).A) (f : (QPF.P F).B a → α), QPF.abs ⟨a, f⟩ = x → u ∈ f '' Set.univ}
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<GOAL>(∀ (p : α → Prop), Functor.Liftp p x ↔ ∀ u ∈ Functor.supp x, p u) ↔ ∃ a f, QPF.abs ⟨a, f⟩ = x ∧ ∀ (a' : (QPF.P F).A) (f' : (QPF.P F).B a' → α), QPF.abs ⟨a', f'⟩ = x → f '' Set.univ ⊆ f' '' Set.univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : QPF.IsUniform<VAR>α : Type u<VAR>a : (QPF.P F).A<VAR>f : (QPF.P F).B a → α<GOAL>Functor.supp (QPF.abs ⟨a, f⟩) = f '' Set.univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : QPF.IsUniform<VAR>α : Type u<VAR>x : F α<VAR>p : α → Prop<GOAL>Functor.Liftp p x ↔ ∀ u ∈ Functor.supp x, p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : QPF.IsUniform<VAR>α β : Type u<VAR>g : α → β<VAR>x : F α<GOAL>Functor.supp (g <$> x) = g '' Functor.supp x
<VAR>F : Type u → Type u<VAR>q : QPF F<GOAL>QPF.SuppPreservation ↔ QPF.IsUniform
<VAR>F : Type u → Type u<VAR>q : QPF F<GOAL>QPF.SuppPreservation ↔ QPF.LiftpPreservation
<VAR>F : Type u → Type u<VAR>q : QPF F<GOAL>QPF.LiftpPreservation ↔ QPF.IsUniform
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<GOAL>IsMaxChain (fun x x_1 => x ≤ x_1) (Set.range f)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<GOAL>↑(Flag.rangeFin f h0 hlast hcovBy) = Set.range f
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>x : α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<GOAL>x ∈ Flag.rangeFin f h0 hlast hcovBy ↔ ∃ k, f k = x
<VAR>p : Nat.Primes<GOAL>↑↑p = ↑p
<VAR>p q : Nat.Primes<GOAL>↑p = ↑q ↔ p = q
<VAR>n m : ℕ+<GOAL>↑(n.gcd m) = (↑n).gcd ↑m
<VAR>n m : ℕ+<GOAL>↑(n.lcm m) = (↑n).lcm ↑m
<VAR>n m : ℕ+<GOAL>n.gcd m ∣ n
<VAR>n m : ℕ+<GOAL>n.gcd m ∣ m
<VAR>m n k : ℕ+<VAR>hm : k ∣ m<VAR>hn : k ∣ n<GOAL>k ∣ m.gcd n
<VAR>n m : ℕ+<GOAL>n ∣ n.lcm m
<VAR>n m : ℕ+<GOAL>m ∣ n.lcm m
<VAR>m n k : ℕ+<VAR>hm : m ∣ k<VAR>hn : n ∣ k<GOAL>m.lcm n ∣ k
<VAR>n m : ℕ+<GOAL>n.gcd m * n.lcm m = n * m
<VAR>n : ℕ+<GOAL>n < 2 → n = 1
<VAR>p : ℕ+<GOAL>p.Prime → 1 < p
<VAR>p : ℕ+<GOAL>p.Prime → p ≠ 1
<VAR>p : ℕ+<GOAL>p.Prime → ¬p ∣ 1
<VAR>m n : ℕ+<GOAL>(↑m).Coprime ↑n ↔ m.Coprime n
<VAR>m : ℕ+<VAR>n k : ℕ+<GOAL>k.Coprime n → (k * m).gcd n = m.gcd n
<VAR>m : ℕ+<VAR>n k : ℕ+<GOAL>k.Coprime n → (m * k).gcd n = m.gcd n
<VAR>m : ℕ+<VAR>n k : ℕ+<GOAL>k.Coprime m → m.gcd (k * n) = m.gcd n
<VAR>m : ℕ+<VAR>n k : ℕ+<GOAL>k.Coprime m → m.gcd (n * k) = m.gcd n
<VAR>n : ℕ+<GOAL>PNat.gcd 1 n = 1
<VAR>m n : ℕ+<GOAL>m.Coprime n → n.Coprime m
<VAR>n : ℕ+<GOAL>PNat.Coprime 1 n
<VAR>n : ℕ+<GOAL>n.Coprime 1
<VAR>k : ℕ+<VAR>m n : ℕ+<VAR>h : m.Coprime n<GOAL>k.gcd (m * n) = k.gcd m * k.gcd n
<VAR>n : ℕ+<GOAL>n.natPred + 1 = ↑n
<VAR>m n : ℕ+<GOAL>m.natPred < n.natPred ↔ m < n
<VAR>m n : ℕ+<GOAL>m.natPred ≤ n.natPred ↔ m ≤ n
<VAR>m n : ℕ+<GOAL>m.natPred = n.natPred ↔ m = n
<VAR>n : ℕ<VAR>NeZero n<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>⟨OfNat.ofNat n, h⟩ = OfNat.ofNat n
<VAR>m n : ℕ<GOAL>m.succPNat < n.succPNat ↔ m < n
<VAR>m n : ℕ<GOAL>m.succPNat ≤ n.succPNat ↔ m ≤ n
<VAR>n m : ℕ<GOAL>n.succPNat = m.succPNat ↔ n = m
<VAR>m n : ℕ+<GOAL>↑m = ↑n ↔ m = n
<VAR>m n : ℕ+<GOAL>↑(m + n) = ↑m + ↑n
<GOAL>⇑OrderIso.pnatIsoNat = PNat.natPred
<GOAL>⇑OrderIso.pnatIsoNat.symm = Nat.succPNat
<VAR>a b : ℕ+<GOAL>a < b + 1 ↔ a ≤ b
<VAR>a b : ℕ+<GOAL>a + 1 ≤ b ↔ a < b
<VAR>p : ℕ+ → Sort u_1<VAR>p1 : p 1<VAR>hp : (n : ℕ+) → p n → p (n + 1)<GOAL>PNat.recOn 1 p1 hp = p1