ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>x : StateCpsT σ m α<VAR>s : σ<GOAL>x.run s = x.runK s fun a s => pure { fst := a, snd := s }
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>x : StateCpsT σ m α<VAR>s : σ<GOAL>x.run' s = x.runK s fun a x => pure a
<VAR>m : Type u_1 → Type u_2<VAR>ε α : Type u_1<VAR>x : α<VAR>Monad m<GOAL>(pure x).run = pure (Except.ok x)
<VAR>m : Type u → Type u_1<VAR>α ε : Type u<VAR>Monad m<VAR>x : m α<GOAL>(ExceptCpsT.lift x).run = do let a ← x pure (Except.ok a)
<VAR>m : Type u_1 → Type u_2<VAR>ε β : Type u_1<VAR>e : ε<VAR>Monad m<GOAL>(throw e).run = pure (Except.error e)
<VAR>m : Type u_1 → Type u_2<VAR>α ε β : Type u_1<VAR>Monad m<VAR>x : m α<VAR>f : α → ExceptCpsT ε m β<GOAL>(ExceptCpsT.lift x >>= f).run = do let a ← x (f a).run
<VAR>m : Type u_1 → Type u_2<VAR>ε α β : Type u_1<VAR>Monad m<VAR>e : ε<VAR>f : α → ExceptCpsT ε m β<GOAL>(throw e >>= f).run = (throw e).run
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>x : α<VAR>Monad m<GOAL>(pure x).runCatch = pure x
<VAR>m : Type u → Type u_1<VAR>α : Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<GOAL>(ExceptCpsT.lift x).runCatch = x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>a : α<VAR>Monad m<GOAL>(throw a).runCatch = pure a
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>Monad m<VAR>x : m α<VAR>f : α → ExceptCpsT β m β<GOAL>(ExceptCpsT.lift x >>= f).runCatch = do let a ← x (f a).runCatch
<VAR>m : Type u_1 → Type u_2<VAR>β α : Type u_1<VAR>Monad m<VAR>e : β<VAR>f : α → ExceptCpsT β m β<GOAL>(throw e >>= f).runCatch = pure e
<VAR>ε : Type u_1<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>x y : ExceptT ε m α<VAR>h : x.run = y.run<GOAL>x = y
<VAR>m : Type u_1 → Type u_2<VAR>α ε : Type u_1<VAR>Monad m<VAR>x : α<GOAL>(pure x).run = pure (Except.ok x)
<VAR>m : Type u → Type v<VAR>α ε : Type u<VAR>Monad m<VAR>x : m α<GOAL>(ExceptT.lift x).run = Except.ok <$> x
<VAR>m : Type u_1 → Type u_2<VAR>α ε β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<VAR>f : α → ExceptT ε m β<GOAL>(ExceptT.lift x >>= f).run = do let a ← x (f a).run
<VAR>m : Type u_1 → Type u_2<VAR>α ε β : Type u_1<VAR>e : ε<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → ExceptT ε m β<GOAL>throw e >>= f = throw e
<VAR>m : Type u_1 → Type u_2<VAR>ε α β : Type u_1<VAR>f : α → ExceptT ε m β<VAR>Monad m<VAR>x : ExceptT ε m α<GOAL>(x >>= f).run = do let x ← x.run match x with | Except.ok x => (f x).run | Except.error e => pure (Except.error e)
<VAR>m : Type u_1 → Type u_2<VAR>α ε : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>a : α<GOAL>ExceptT.lift (pure a) = pure a
<VAR>m : Type u_1 → Type u_2<VAR>α β ε : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β<VAR>x : ExceptT ε m α<GOAL>(f <$> x).run = Except.map f <$> x.run
<VAR>m : Type u → Type u_1<VAR>α β ε : Type u<VAR>Monad m<VAR>mf : ExceptT ε m (α → β)<VAR>x : ExceptT ε m α<GOAL>(Seq.seq mf fun x_1 => x) = do let f ← mf f <$> x
<VAR>m : Type u_1 → Type u_2<VAR>α β ε : Type u_1<VAR>Monad m<VAR>f : α → β<VAR>x : ExceptT ε m α<GOAL>x >>= pure ∘ f = f <$> x
<VAR>α β ε : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>x : ExceptT ε m α<VAR>y : ExceptT ε m β<GOAL>(SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
<VAR>m : Type u_1 → Type u_2<VAR>ε α β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : ExceptT ε m α<VAR>y : ExceptT ε m β<GOAL>(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
<VAR>ρ : Type u_1<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>x y : ReaderT ρ m α<VAR>h : ∀ (ctx : ρ), x.run ctx = y.run ctx<GOAL>x = y
<VAR>m : Type u_1 → Type u_2<VAR>α ρ : Type u_1<VAR>Monad m<VAR>a : α<VAR>ctx : ρ<GOAL>(pure a).run ctx = pure a
<VAR>m : Type u_1 → Type u_2<VAR>ρ α β : Type u_1<VAR>Monad m<VAR>x : ReaderT ρ m α<VAR>f : α → ReaderT ρ m β<VAR>ctx : ρ<GOAL>(x >>= f).run ctx = do let a ← x.run ctx (f a).run ctx
<VAR>m : Type u_1 → Type u_2<VAR>α ρ β : Type u_1<VAR>Monad m<VAR>a : α<VAR>x : ReaderT ρ m β<VAR>ctx : ρ<GOAL>(Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx)
<VAR>m : Type u_1 → Type u_2<VAR>α β ρ : Type u_1<VAR>Monad m<VAR>f : α → β<VAR>x : ReaderT ρ m α<VAR>ctx : ρ<GOAL>(f <$> x).run ctx = f <$> x.run ctx
<VAR>n : Type u_1 → Type u_2<VAR>m : Type u_1 → Type u_3<VAR>α ρ : Type u_1<VAR>MonadLiftT n m<VAR>x : n α<VAR>ctx : ρ<GOAL>(monadLift x).run ctx = monadLift x
<VAR>n : Type u → Type u_1<VAR>m : Type u → Type u_2<VAR>ρ α : Type u<VAR>MonadFunctor n m<VAR>f : {β : Type u} → n β → n β<VAR>x : ReaderT ρ m α<VAR>ctx : ρ<GOAL>(monadMap f x).run ctx = monadMap f (x.run ctx)
<VAR>m : Type u_1 → Type u_2<VAR>ρ : Type u_1<VAR>Monad m<VAR>ctx : ρ<GOAL>ReaderT.read.run ctx = pure ctx
<VAR>m : Type u → Type u_1<VAR>ρ α β : Type u<VAR>Monad m<VAR>f : ReaderT ρ m (α → β)<VAR>x : ReaderT ρ m α<VAR>ctx : ρ<GOAL>(Seq.seq f fun x_1 => x).run ctx = Seq.seq (f.run ctx) fun x_1 => x.run ctx
<VAR>m : Type u_1 → Type u_2<VAR>ρ α β : Type u_1<VAR>Monad m<VAR>x : ReaderT ρ m α<VAR>y : ReaderT ρ m β<VAR>ctx : ρ<GOAL>(SeqRight.seqRight x fun x => y).run ctx = SeqRight.seqRight (x.run ctx) fun x => y.run ctx
<VAR>m : Type u_1 → Type u_2<VAR>ρ α β : Type u_1<VAR>Monad m<VAR>x : ReaderT ρ m α<VAR>y : ReaderT ρ m β<VAR>ctx : ρ<GOAL>(SeqLeft.seqLeft x fun x => y).run ctx = SeqLeft.seqLeft (x.run ctx) fun x => y.run ctx
<VAR>σ : Type u_1<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>x y : StateT σ m α<VAR>h : ∀ (s : σ), x.run s = y.run s<GOAL>x = y
<VAR>m : Type u_1 → Type u_2<VAR>σ α : Type u_1<VAR>Monad m<VAR>x : StateT σ m α<VAR>s : σ<GOAL>x.run' s = (fun x => x.fst) <$> x.run s
<VAR>m : Type u_1 → Type u_2<VAR>α σ : Type u_1<VAR>Monad m<VAR>a : α<VAR>s : σ<GOAL>(pure a).run s = pure (a, s)
<VAR>m : Type u_1 → Type u_2<VAR>σ α β : Type u_1<VAR>Monad m<VAR>x : StateT σ m α<VAR>f : α → StateT σ m β<VAR>s : σ<GOAL>(x >>= f).run s = do let p ← x.run s (f p.fst).run p.snd
<VAR>m : Type u → Type u_1<VAR>α β σ : Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β<VAR>x : StateT σ m α<VAR>s : σ<GOAL>(f <$> x).run s = (fun p => (f p.fst, p.snd)) <$> x.run s
<VAR>m : Type u_1 → Type u_2<VAR>σ : Type u_1<VAR>Monad m<VAR>s : σ<GOAL>get.run s = pure (s, s)
<VAR>m : Type u_1 → Type u_2<VAR>σ : Type u_1<VAR>Monad m<VAR>s s' : σ<GOAL>(set s').run s = pure (PUnit.unit, s')
<VAR>m : Type u_1 → Type u_2<VAR>σ : Type u_1<VAR>Monad m<VAR>f : σ → σ<VAR>s : σ<GOAL>(modify f).run s = pure (PUnit.unit, f s)
<VAR>m : Type u_1 → Type u_2<VAR>σ α : Type u_1<VAR>Monad m<VAR>f : σ → α × σ<VAR>s : σ<GOAL>(modifyGet f).run s = pure ((f s).fst, (f s).snd)
<VAR>m : Type u → Type u_1<VAR>α σ : Type u<VAR>Monad m<VAR>x : m α<VAR>s : σ<GOAL>(StateT.lift x).run s = do let a ← x pure (a, s)
<VAR>m : Type u → Type u_1<VAR>β α σ : Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<VAR>f : α → StateT σ m β<VAR>s : σ<GOAL>(StateT.lift x >>= f).run s = do let a ← x (f a).run s
<VAR>m : Type u → Type u_1<VAR>n : Type u → Type u_2<VAR>α σ : Type u<VAR>Monad m<VAR>MonadLiftT n m<VAR>x : n α<VAR>s : σ<GOAL>(monadLift x).run s = do let a ← monadLift x pure (a, s)
<VAR>m : Type u → Type u_1<VAR>n : Type u → Type u_2<VAR>σ α : Type u<VAR>Monad m<VAR>MonadFunctor n m<VAR>f : {β : Type u} → n β → n β<VAR>x : StateT σ m α<VAR>s : σ<GOAL>(monadMap f x).run s = monadMap f (x.run s)
<VAR>m : Type u → Type u_1<VAR>α β σ : Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : StateT σ m (α → β)<VAR>x : StateT σ m α<VAR>s : σ<GOAL>(Seq.seq f fun x_1 => x).run s = do let fs ← f.run s (fun p => (fs.fst p.fst, p.snd)) <$> x.run fs.snd
<VAR>m : Type u_1 → Type u_2<VAR>σ α β : Type u_1<VAR>Monad m<VAR>x : StateT σ m α<VAR>y : StateT σ m β<VAR>s : σ<GOAL>(SeqRight.seqRight x fun x => y).run s = do let p ← x.run s y.run p.snd
<VAR>m : Type u → Type u_1<VAR>α β σ : Type u<VAR>Monad m<VAR>x : StateT σ m α<VAR>y : StateT σ m β<VAR>s : σ<GOAL>(SeqLeft.seqLeft x fun x => y).run s = do let p ← x.run s let p' ← y.run p.snd pure (p.fst, p'.snd)
<VAR>m : Type u_1 → Type u_2<VAR>σ α β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : StateT σ m α<VAR>y : StateT σ m β<GOAL>(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
<VAR>m : Type u_1 → Type u_2<VAR>σ α β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : StateT σ m α<VAR>y : StateT σ m β<GOAL>(SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
<VAR>α : Sort u_1<VAR>n : α<GOAL>sizeOf n = 0
<VAR>α : Sort u_1<VAR>SizeOf α<VAR>f : Unit → α<GOAL>sizeOf f = sizeOf (f Unit.unit)
<VAR>p : Lean.Name<VAR>s : String<GOAL>sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
<VAR>p : Lean.Name<VAR>n : Nat<GOAL>sizeOf (p.num n) = 1 + sizeOf p + sizeOf n
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>x y : α<VAR>h₁ : Acc r x<VAR>h₂ : r y x<GOAL>Acc r y
<VAR>α : Sort u<VAR>self : WellFoundedRelation α<GOAL>WellFounded WellFoundedRelation.rel
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>wf : WellFounded r<VAR>a : α<GOAL>Acc r a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>hwf : WellFounded r<VAR>C : α → Prop<VAR>a : α<VAR>h : ∀ (x : α), (∀ (y : α), r y x → C y) → C x<GOAL>C a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>C : α → Sort v<VAR>F : (x : α) → ((y : α) → r y x → C y) → C x<VAR>x : α<VAR>acx : Acc r x<GOAL>WellFounded.fixF F x acx = F x fun y p => WellFounded.fixF F y ⋯
<VAR>α : Sort u<VAR>C : α → Sort v<VAR>r : α → α → Prop<VAR>hwf : WellFounded r<VAR>F : (x : α) → ((y : α) → r y x → C y) → C x<VAR>x : α<GOAL>hwf.fix F x = F x fun y x => hwf.fix F y
<VAR>α : Sort u<VAR>r q : α → α → Prop<VAR>a : α<VAR>h₁ : Subrelation q r<VAR>ac : Acc r a<GOAL>Acc q a
<VAR>α : Sort u<VAR>r q : α → α → Prop<VAR>h₁ : Subrelation q r<VAR>h₂ : WellFounded r<GOAL>WellFounded q
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>a : α<VAR>f : α → β<VAR>ac : Acc r (f a)<GOAL>Acc (InvImage r f) a
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>f : α → β<VAR>h : WellFounded r<GOAL>WellFounded (InvImage r f)
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>z : α<VAR>ac : Acc r z<GOAL>Acc (TC r) z
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>h : WellFounded r<GOAL>WellFounded (TC r)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>p q : α × β<GOAL>Prod.Lex r s p q ↔ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
<VAR>β : Type v<VAR>rb : β → β → Prop<VAR>a₂ : Nat<VAR>b₂ : β<VAR>a₁ : Nat<VAR>b₁ : β<VAR>h₁ : a₁ ≤ a₂<VAR>h₂ : rb b₁ b₂<GOAL>Prod.Lex Nat.lt rb { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
<VAR>α : Type u<VAR>β : Type v<VAR>ra : α → α → Prop<VAR>rb : β → β → Prop<VAR>a : α<VAR>aca : Acc ra a<VAR>acb : ∀ (b : β), Acc rb b<VAR>b : β<GOAL>Acc (Prod.Lex ra rb) { fst := a, snd := b }
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>ha : WellFounded r<VAR>hb : WellFounded s<GOAL>WellFounded (PSigma.lexNdep r s)
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>b : β<VAR>acb : Acc s b<VAR>aca : ∀ (a : α), Acc r a<VAR>a : α<GOAL>Acc (PSigma.RevLex r s) ⟨a, b⟩
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>ha : WellFounded r<VAR>hb : WellFounded s<GOAL>WellFounded (PSigma.RevLex r s)
<VAR>α : Type u<VAR>β : Type v<VAR>b₁ b₂ : β<VAR>s : β → β → Prop<VAR>a₁ a₂ : α<VAR>h : s b₁ b₂<GOAL>PSigma.SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>x : m α<GOAL>monadLift x = x
<VAR>f : Type u → Type v<VAR>Functor f<VAR>self : LawfulFunctor f<VAR>α : Type u<VAR>x : f α<GOAL>id <$> x = x
<VAR>f : Type u → Type v<VAR>Functor f<VAR>self : LawfulFunctor f<VAR>α β : Type u<GOAL>Functor.mapConst = Functor.map ∘ Function.const β
<VAR>f : Type u → Type v<VAR>Functor f<VAR>self : LawfulFunctor f<VAR>α β γ : Type u<VAR>g : α → β<VAR>h : β → γ<VAR>x : f α<GOAL>(h ∘ g) <$> x = h <$> g <$> x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Functor m<VAR>LawfulFunctor m<VAR>x : m α<GOAL>(fun a => a) <$> x = x
<VAR>f : Type u → Type v<VAR>Applicative f<VAR>self : LawfulApplicative f<VAR>α β : Type u<VAR>x : f α<VAR>y : f β<GOAL>(SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
<VAR>f : Type u → Type v<VAR>Applicative f<VAR>self : LawfulApplicative f<VAR>α β : Type u<VAR>g : f (α → β)<VAR>x : α<GOAL>(Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
<VAR>f : Type u → Type v<VAR>Applicative f<VAR>self : LawfulApplicative f<VAR>α β γ : Type u<VAR>x : f α<VAR>g : f (α → β)<VAR>h : f (β → γ)<GOAL>(Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
<VAR>f : Type u → Type v<VAR>Applicative f<VAR>self : LawfulApplicative f<VAR>α β : Type u<VAR>g : α → β<VAR>x : α<GOAL>g <$> pure x = pure (g x)
<VAR>f : Type u → Type v<VAR>Applicative f<VAR>self : LawfulApplicative f<VAR>α β : Type u<VAR>g : α → β<VAR>x : f α<GOAL>(Seq.seq (pure g) fun x_1 => x) = g <$> x
<VAR>f : Type u → Type v<VAR>Applicative f<VAR>self : LawfulApplicative f<VAR>α β : Type u<VAR>x : f α<VAR>y : f β<GOAL>(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
<VAR>f : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Applicative f<VAR>LawfulApplicative f<VAR>x : f α<GOAL>(Seq.seq (pure id) fun x_1 => x) = x
<VAR>m : Type u → Type v<VAR>Monad m<VAR>self : LawfulMonad m<VAR>α β : Type u<VAR>f : m (α → β)<VAR>x : m α<GOAL>(do let x_1 ← f x_1 <$> x) = Seq.seq f fun x_1 => x
<VAR>m : Type u → Type v<VAR>Monad m<VAR>self : LawfulMonad m<VAR>α β : Type u<VAR>x : α<VAR>f : α → m β<GOAL>pure x >>= f = f x
<VAR>m : Type u → Type v<VAR>Monad m<VAR>self : LawfulMonad m<VAR>α β : Type u<VAR>f : α → β<VAR>x : m α<GOAL>(do let a ← x pure (f a)) = f <$> x
<VAR>m : Type u → Type v<VAR>Monad m<VAR>self : LawfulMonad m<VAR>α β γ : Type u<VAR>x : m α<VAR>f : α → m β<VAR>g : β → m γ<GOAL>x >>= f >>= g = x >>= fun x => f x >>= g
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<GOAL>x >>= pure = x
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β<VAR>x : m α<GOAL>f <$> x = do let a ← x pure (f a)
<VAR>m : Type u → Type u_1<VAR>α β : Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : m (α → β)<VAR>x : m α<GOAL>(Seq.seq f fun x_1 => x) = do let x_1 ← f x_1 <$> x
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>Bind m<VAR>x : m α<VAR>f g : α → m β<VAR>h : ∀ (a : α), f a = g a<GOAL>x >>= f = x >>= g
<VAR>m : Type u_1 → Type u_2<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m PUnit<GOAL>(do x pure PUnit.unit) = x
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>Functor m<VAR>x : m α<VAR>f g : α → β<VAR>h : ∀ (a : α), f a = g a<GOAL>f <$> x = g <$> x
<VAR>m : Type u → Type u_1<VAR>α β : Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>mf : m (α → β)<VAR>x : m α<GOAL>(Seq.seq mf fun x_1 => x) = do let f ← mf f <$> x
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<VAR>y : m β<GOAL>(SeqRight.seqRight x fun x => y) = do let _ ← x y
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<VAR>y : m β<GOAL>(SeqLeft.seqLeft x fun x => y) = do let a ← x let _ ← y pure a
<VAR>m : Type u → Type v<VAR>Monad m<VAR>id_map : ∀ {α : Type u} (x : m α), id <$> x = x<VAR>pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x<VAR>bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g<VAR>map_const : ∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y := by intros; rfl<VAR>seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun x => y) = do let a ← x let _ ← y pure a := by intros; rfl<VAR>seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun x => y) = do let _ ← x y := by intros; rfl<VAR>bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let y ← x pure (f y)) = f <$> x := by intros; rfl<VAR>bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun x_1 => x := by intros; rfl<GOAL>LawfulMonad m
<VAR>α β : Type u_1<VAR>x : Id α<VAR>f : α → β<GOAL>f <$> x = f x
<VAR>α β : Type u_1<VAR>x : Id α<VAR>f : α → id β<GOAL>x >>= f = f x
<VAR>α : Type u_1<VAR>a : α<GOAL>pure a = a
<VAR>p q : Prop<VAR>h : ¬(p ∨ q)<GOAL>¬p ∧ ¬q
<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>h : ¬(p ∧ q)<GOAL>¬p ∨ ¬q
<VAR>p q : Prop<VAR>Decidable q<VAR>h : p ↔ q<GOAL>p ∧ q ∨ ¬p ∧ ¬q
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>¬(a ↔ b) ↔ a ∧ ¬b ∨ ¬a ∧ b
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<VAR>h : ¬(a ↔ b)<GOAL>a ∧ ¬b ∨ ¬a ∧ b
<VAR>a b : Prop<VAR>Decidable a<VAR>h : ¬(a → b)<GOAL>a ∧ ¬b
<VAR>α : Type u<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<GOAL>P ∧ (if P then a else b) = a ∨ ¬P ∧ (if P then a else b) = b
<VAR>x : Lean.Omega.Coeffs<VAR>m : Nat<GOAL>(x.bmod m).length ≤ x.length
<VAR>m : Nat<VAR>xs ys : Lean.Omega.Coeffs<GOAL>↑m ∣ Lean.Omega.Coeffs.bmod_dot_sub_dot_bmod m xs ys
<VAR>i : Nat<VAR>xs : Lean.Omega.Coeffs<VAR>h : xs.length ≤ i<GOAL>xs.get i = 0
<VAR>xs ys : Lean.Omega.Coeffs<VAR>i : Nat<VAR>z : Int<GOAL>(xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i
<VAR>xs ys : Lean.Omega.Coeffs<VAR>d : Int<VAR>h : d ∣ ↑xs.gcd<GOAL>(xs.sdiv d).dot ys = xs.dot ys / d
<VAR>xs ys : Lean.Omega.Coeffs<VAR>i : Int<GOAL>Lean.Omega.Coeffs.dot (i * xs) ys = i * xs.dot ys
<VAR>xs ys zs : Lean.Omega.Coeffs<GOAL>(xs + ys).dot zs = xs.dot zs + ys.dot zs
<VAR>xs ys : Lean.Omega.Coeffs<GOAL>xs - ys = xs + -ys
<VAR>a : Int<VAR>xs : Lean.Omega.Coeffs<VAR>b : Int<VAR>ys : Lean.Omega.Coeffs<GOAL>Lean.Omega.Coeffs.combo a xs b ys = a * xs + b * ys
<VAR>xs ys : Lean.Omega.Coeffs<GOAL>↑xs.gcd ∣ xs.dot ys
<VAR>f : Int → Int<VAR>xs : Lean.Omega.Coeffs<GOAL>(Lean.Omega.Coeffs.map f xs).length ≤ xs.length
<VAR>xs : Lean.Omega.Coeffs<GOAL>xs.dot [] = 0
<VAR>i : Nat<GOAL>Lean.Omega.Coeffs.get [] i = 0
<VAR>xs ys : Lean.Omega.IntList<GOAL>Lean.Omega.Coeffs.dot (-xs) ys = -Lean.Omega.Coeffs.dot xs ys
<VAR>a b : Nat<GOAL>↑(a ^ b) = ↑a ^ b
<VAR>a : Int<VAR>b : Nat<VAR>h : 0 < a<GOAL>0 < a ^ b
<VAR>a : Nat<GOAL>0 < ↑a ↔ 0 < a
<VAR>a : Nat<VAR>h : 0 < a<GOAL>0 < ↑a
<VAR>x : Nat<GOAL>↑(OfNat.ofNat x) = OfNat.ofNat x
<VAR>x y : Nat<VAR>h : x < y<GOAL>↑x < ↑y
<VAR>x y : Nat<VAR>h : x ≤ y<GOAL>↑x ≤ ↑y
<VAR>x y : Nat<GOAL>↑(x <<< y) = ↑x * ↑(2 ^ y)
<VAR>x y : Nat<GOAL>↑(x >>> y) = ↑x / ↑(2 ^ y)
<VAR>x : Nat<VAR>y : Int<GOAL>0 ≤ ↑x % y
<VAR>x y : Int<VAR>h : ¬x ≤ y<GOAL>y < x
<VAR>x y : Int<VAR>h : y < x<GOAL>¬x ≤ y
<VAR>x y : Int<VAR>h₁ : y < x<VAR>h₂ : x ≤ y<GOAL>False
<VAR>x y : Int<VAR>h₁ : y ≤ x<VAR>h₂ : x < y<GOAL>False
<VAR>x y : Int<VAR>h : ¬y > x<GOAL>y ≤ x
<VAR>x y : Int<VAR>h : y ≥ x<GOAL>¬y < x
<VAR>x y : Int<VAR>h : ¬x < y<GOAL>y ≤ x
<VAR>x y : Int<VAR>h : y ≤ x<GOAL>¬x < y
<VAR>a b c d : Int<VAR>h₁ : a = b<VAR>h₂ : c = d<GOAL>a + c = b + d
<VAR>a b c d : Int<VAR>h₁ : a = b<VAR>h₂ : c = d<GOAL>a * c = b * d
<VAR>a b : Int<VAR>h₁ : a = b<VAR>c : Int<GOAL>a * c = b * c
<VAR>a b c d : Int<VAR>h₁ : a = b<VAR>h₂ : c = d<GOAL>a - c = b - d
<VAR>a b : Int<VAR>h₁ : a = b<GOAL>-a = -b
<VAR>x y : Int<VAR>h : x > y<GOAL>y < x
<VAR>x y : Int<VAR>h : x ≥ y<GOAL>y ≤ x
<VAR>b a : Nat<VAR>h : ¬b ≤ a<GOAL>↑(a - b) = 0
<VAR>a b : Nat<GOAL>b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0
<VAR>a b : Nat<VAR>h : a = b<GOAL>↑a = ↑b
<VAR>a b c : Nat<GOAL>↑(a - b - c) = ↑(a - (b + c))
<VAR>a b : Nat<GOAL>↑(min a b) = min ↑a ↑b
<VAR>a b : Nat<GOAL>↑(max a b) = max ↑a ↑b
<VAR>a : Int<GOAL>↑a.natAbs = if 0 ≤ a then a else -a
<VAR>a : Int<GOAL>0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a
<VAR>a : Int<GOAL>-a ≤ ↑a.natAbs
<VAR>a b c : Int<GOAL>a + b ≤ c ↔ a ≤ c - b
<VAR>a b c : Int<GOAL>a ≤ b + c ↔ a - c ≤ b
<VAR>a b : Int<GOAL>a + b ≤ 0 ↔ a ≤ -b
<VAR>a b : Int<GOAL>a + b ≤ 0 ↔ b ≤ -a
<VAR>a b : Int<GOAL>0 ≤ a + b ↔ -b ≤ a
<VAR>a b : Int<GOAL>0 ≤ a + b ↔ -a ≤ b
<VAR>β : Type u_1<VAR>x : Nat<VAR>y : β<GOAL>↑(x, y).fst = ↑x
<VAR>α : Type u_1<VAR>x : α<VAR>y : Nat<GOAL>↑(x, y).snd = ↑y
<VAR>x y : Nat<VAR>h : x > y<GOAL>y < x
<VAR>x y : Nat<VAR>h : x ≥ y<GOAL>y ≤ x
<VAR>n : Nat<VAR>i j : Fin n<GOAL>i ≠ j ↔ i < j ∨ i > j
<VAR>n : Nat<VAR>i j : Fin n<VAR>h : i ≠ j<GOAL>i < j ∨ i > j
<VAR>n : Nat<VAR>i j : Fin n<GOAL>¬i ≤ j ↔ j < i
<VAR>n : Nat<VAR>i j : Fin n<GOAL>¬i < j ↔ j ≤ i
<VAR>n : Nat<VAR>i j : Fin n<VAR>h : ¬i ≤ j<GOAL>j < i
<VAR>n : Nat<VAR>i j : Fin n<VAR>h : ¬i < j<GOAL>j ≤ i
<VAR>n : Nat<VAR>x y : Fin n<GOAL>↑↑(x + y) = (↑↑x + ↑↑y) % ↑n
<VAR>n : Nat<VAR>x y : Fin n<GOAL>↑↑(x - y) = (↑(n - ↑y) + ↑↑x) % ↑n
<VAR>n : Nat<VAR>x y : Fin n<GOAL>↑↑(x * y) = ↑↑x * ↑↑y % ↑n
<VAR>n x y : Nat<VAR>h : y = x % (n + 1)<GOAL>↑↑(OfNat.ofNat x) = OfNat.ofNat y
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {p q : α × β}, Prod.Lex r s p q → r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableEq α<VAR>β : Type u_2<VAR>s : β → β → Prop<VAR>p q : α × β<VAR>w : ¬Prod.Lex r s p q<GOAL>¬r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬s p.snd q.snd)
<GOAL>∀ {α : Type u_1} {x : α} {β : Type u_2} {y : β}, (x, y).fst = x
<GOAL>∀ {α : Type u_1} {x : α} {α_1 : Type u_2} {y : α_1}, (x, y).snd = y
<VAR>α : Sort u<VAR>p : α → Prop<VAR>h : ∃ x, p x<GOAL>p (Classical.choose h)
<VAR>p : Prop<GOAL>p ∨ ¬p
<VAR>α : Sort u<GOAL>Nonempty α → ∃ x, True
<VAR>α : Sort u<VAR>h : Nonempty α<VAR>p : α → Prop<GOAL>(∃ y, p y) → p (Classical.epsilon p)
<VAR>α : Sort u<VAR>p : α → Prop<VAR>hex : ∃ y, p y<GOAL>p (Classical.epsilon p)
<VAR>α : Sort u<VAR>x : α<GOAL>(Classical.epsilon fun y => y = x) = x
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>r : (x : α) → β x → Prop<VAR>h : ∀ (x : α), ∃ y, r x y<GOAL>∃ f, ∀ (x : α), r x (f x)
<VAR>α : Sort u<VAR>b : α → Sort v<VAR>p : (x : α) → b x → Prop<GOAL>(∀ (x : α), ∃ y, p x y) ↔ ∃ f, ∀ (x : α), p x (f x)
<VAR>a : Prop<GOAL>a = True ∨ a = False
<VAR>p q : Prop<VAR>hpq : p → q<VAR>hnpq : ¬p → q<GOAL>q
<VAR>p : Prop<VAR>h : ¬p → False<GOAL>p
<VAR>a : Prop<GOAL>¬¬a ↔ a
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(¬∀ (x : α), p x) ↔ ∃ x, ¬p x
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(¬∀ (x : α), ¬p x) ↔ ∃ x, p x
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(¬∃ x, ¬p x) ↔ ∀ (x : α), p x
<VAR>α : Sort u_1<VAR>P : α → Prop<GOAL>(∀ (a : α), P a) ∨ ∃ a, ¬P a
<VAR>α : Sort u_1<VAR>P : α → Prop<GOAL>(∃ a, P a) ∨ ∀ (a : α), ¬P a
<VAR>a b : Prop<GOAL>a ∨ b ↔ ¬a → b
<VAR>a b : Prop<GOAL>a ∨ b ↔ ¬b → a
<VAR>a b : Prop<GOAL>¬(a → b) ↔ a ∧ ¬b
<VAR>a b : Prop<GOAL>¬(a ∧ b) ↔ ¬a ∨ ¬b
<VAR>a b : Prop<GOAL>¬(a ↔ b) ↔ (¬a ↔ b)
<VAR>b a : Prop<GOAL>(b ↔ a → b) ↔ a ∨ b
<VAR>a b : Prop<GOAL>(a → b ↔ b) ↔ a ∨ b
<VAR>a b c : Prop<GOAL>a ∧ b ∨ (a → c) ↔ a → b ∨ c
<VAR>p q : Prop<GOAL>(p → q) ∧ (¬p → q) ↔ q
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : ∃ a, p a<GOAL>p P.choose
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x y : α × β<GOAL>x.fst = y.fst → x.snd = y.snd → x = y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>x y : PProd α β<GOAL>x.fst = y.fst → x.snd = y.snd → x = y
<GOAL>∀ {α : Type u_1} {β : α → Type u_2} {x y : Sigma β}, x.fst = y.fst → HEq x.snd y.snd → x = y
<GOAL>∀ {α : Sort u_1} {β : α → Sort u_2} {x y : PSigma β}, x.fst = y.fst → HEq x.snd y.snd → x = y
<VAR>a b : Lean.Omega.LinearCombo<VAR>w₁ : a.const = b.const<VAR>w₂ : a.coeffs = b.coeffs<GOAL>a = b
<VAR>lc : Lean.Omega.LinearCombo<GOAL>lc.eval [] = lc.const
<VAR>i : Nat<VAR>v : Lean.Omega.Coeffs<GOAL>(Lean.Omega.LinearCombo.coordinate i).eval v = v.get i
<VAR>a0 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 0).eval (Lean.Omega.Coeffs.ofList (a0 :: t)) = a0
<VAR>a0 a1 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 1).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1
<VAR>a0 a1 a2 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 2).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2
<VAR>a0 a1 a2 a3 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 3).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3
<VAR>a0 a1 a2 a3 a4 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 4).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4
<VAR>a0 a1 a2 a3 a4 a5 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 5).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5
<VAR>a0 a1 a2 a3 a4 a5 a6 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 6).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6
<VAR>a0 a1 a2 a3 a4 a5 a6 a7 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 7).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7