ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<GOAL>Nat.rec (some (z a)) (fun n_1 n_ih => Nat.rec (some (s a)) (fun n_2 n_ih => Nat.rec (some (l a)) (fun n_3 n_ih => Nat.rec (some (r a)) (fun n_4 n_ih => G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))), n_4, n_4.div2.div2)) n_3) n_2) n_1) (List.map (fun n => F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))).length = some (F a (ofNat Code (n + 1 + 1 + 1 + 1)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<GOAL>Nat.rec (some (z a)) (fun n_1 n_ih => Nat.rec (some (s a)) (fun n_2 n_ih => Nat.rec (some (l a)) (fun n_3 n_ih => Nat.rec (some (r a)) (fun n_4 n_ih => G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))), n_4, n_4.div2.div2)) n_3) n_2) n_1) (n + 1 + 1 + 1 + 1) = some (F a (ofNat Code (n + 1 + 1 + 1 + 1)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<VAR>m2 : (unpair m).2 < n + 4<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<VAR>m2 : (unpair m).2 < n + 4<GOAL>((Option.map (fun n => F a (ofNat Code n)) (List.range (n + 4))[m]?).bind fun a_1 => (Option.map (fun n => F a (ofNat Code n)) (List.range (n + 4))[(unpair m).1]?).bind fun a_2 => Option.map ((fun s₂ => bif n.bodd then bif n.div2.bodd then rf a (ofNat Code m, a_1) else pc a (ofNat Code (unpair m).1, ofNat Code (unpair m).2, a_2, s₂) else bif n.div2.bodd then co a (ofNat Code (unpair m).1, ofNat Code (unpair m).2, a_2, s₂) else pr a (ofNat Code (unpair m).1, ofNat Code (unpair m).2, a_2, s₂)) ∘ fun n => F a (ofNat Code n)) (List.range (n + 4))[(unpair m).2]?) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<VAR>m2 : (unpair m).2 < n + 4<GOAL>(bif n.bodd then bif n.div2.bodd then rf a (ofNat Code n.div2.div2, F a (ofNat Code n.div2.div2)) else pc a (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2)) else bif n.div2.bodd then co a (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2)) else pr a (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2))) = F a (ofNat Code (n + 4))
<VAR>a b c : ℕ<GOAL>Ioc b (b + 1) = {b + 1}
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < c.length<GOAL>c.sizeUpTo i < c.sizeUpTo (i + 1)
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < c.length<GOAL>c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<GOAL>∃ σ, σ x = y
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<VAR>hx : IsAlgebraic K x<GOAL>∃ σ, σ x = y
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<VAR>hx : IsAlgebraic K x<VAR>f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯<GOAL>∃ σ, σ x = y
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<VAR>hx : IsAlgebraic K x<VAR>f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯<VAR>hxy : (f.liftNormal L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y<GOAL>∃ σ, σ x = y
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J✝ K L : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, J i ⊔ I = ⊤<GOAL>(∏ i ∈ s, J i) ⊔ I = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Group G<VAR>g h : G<GOAL>g ∈ orbit (ConjAct G) h ↔ IsConj g h
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Group G<VAR>g h : G<GOAL>(∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0∞<VAR>h : ∑' (i : α), f i ≠ ⊤<GOAL>(support f).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>h : ∑' (i : α), (fun i => ↑(f i)) i ≠ ⊤<GOAL>(support fun i => ↑(f i)).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>P : α → Prop<VAR>s : Set α<GOAL>{x | ↑x ∈ s}.ncard = (s ∩ setOf P).ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>P : α → Prop<VAR>s : Set α<GOAL>s ∩ setOf P = (fun a => ↑a) '' {x | ↑x ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>P : α → Prop<VAR>s : Set α<VAR>x : α<GOAL>x ∈ s ∩ setOf P ↔ x ∈ (fun a => ↑a) '' {x | ↑x ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → σ<GOAL>(Primrec₂ fun a n => Option.map (f a) (decode n)) ↔ Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → σ<GOAL>(Primrec₂ fun a n => (decode n).bind (some ∘ f a)) ↔ Primrec₂ f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>Set.InjOn ⇑f ↑p ↔ Set.SurjOn ⇑f ↑p ↑p
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>Injective ((↑p).restrict ⇑f) ↔ Surjective (Set.MapsTo.restrict (⇑f) (↑p) (↑p) h)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>Injective ⇑(f.domRestrict p) ↔ Surjective ⇑(f.restrict h)
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd' C a 0 a ⋯).hom.app X = (shiftFunctorZero C A).inv.app ((shiftFunctor C a).obj X)
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f : K[X]<VAR>hf : f.natDegree ≠ 0<GOAL>(X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f : K[X]<VAR>hf : f.natDegree ≠ 0<VAR>g : K[X]<VAR>hg : f = f.factor * g<GOAL>(X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f : K[X]<VAR>hf : f.natDegree ≠ 0<VAR>g : K[X]<VAR>hg : f = f.factor * g<GOAL>(map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>W X Y Z : C<GOAL>(α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom = (𝟙 W ⊗ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv