ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : β<GOAL>Sum.inr a ≤ Sum.inr b ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : α<GOAL>Sum.inl a < Sum.inl b ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : β<GOAL>Sum.inr a < Sum.inr b ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<VAR>b : β<GOAL>¬Sum.inl b ≤ Sum.inr a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a : α<VAR>b : β<GOAL>¬Sum.inl b < Sum.inr a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<VAR>b : β<GOAL>¬Sum.inr b ≤ Sum.inl a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a : α<VAR>b : β<GOAL>¬Sum.inr b < Sum.inl a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone Sum.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone Sum.inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>StrictMono Sum.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>StrictMono Sum.inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<GOAL>NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<GOAL>NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<GOAL>DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : α ⊕ β<GOAL>a.swap ≤ b.swap ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : α ⊕ β<GOAL>a.swap < b.swap ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : α ⊕ β<GOAL>toLex a ≤ toLex b ↔ Sum.Lex (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : α ⊕ β<GOAL>toLex a < toLex b ↔ Sum.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : Lex (α ⊕ β)<GOAL>a ≤ b ↔ Sum.Lex (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) (ofLex a) (ofLex b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : Lex (α ⊕ β)<GOAL>a < b ↔ Sum.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (ofLex a) (ofLex b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : α<GOAL>toLex (Sum.inl a) ≤ toLex (Sum.inl b) ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : β<GOAL>toLex (Sum.inr a) ≤ toLex (Sum.inr b) ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : α<GOAL>toLex (Sum.inl a) < toLex (Sum.inl b) ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : β<GOAL>toLex (Sum.inr a) < toLex (Sum.inr b) ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<VAR>b : β<GOAL>toLex (Sum.inl a) ≤ toLex (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a : α<VAR>b : β<GOAL>toLex (Sum.inl a) < toLex (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<VAR>b : β<GOAL>¬toLex (Sum.inr b) ≤ toLex (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a : α<VAR>b : β<GOAL>¬toLex (Sum.inr b) < toLex (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone ⇑toLex
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>StrictMono ⇑toLex
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone (⇑toLex ∘ Sum.inl)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone (⇑toLex ∘ Sum.inr)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>StrictMono (⇑toLex ∘ Sum.inl)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>StrictMono (⇑toLex ∘ Sum.inr)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>OrderBot α<VAR>LE β<GOAL>toLex (Sum.inl ⊥) = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>OrderTop β<GOAL>toLex (Sum.inr ⊤) = ⊤
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>LE α<VAR>LE β<GOAL>∀ (a : α ⊕ β), (OrderIso.sumComm α β) a = a.swap
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>LE α<VAR>LE β<GOAL>(OrderIso.sumComm α β).symm = OrderIso.sumComm β α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>a : α<GOAL>(OrderIso.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>b : β<GOAL>(OrderIso.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>c : γ<GOAL>(OrderIso.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>a : α<GOAL>(OrderIso.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>b : β<GOAL>(OrderIso.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>c : γ<GOAL>(OrderIso.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<GOAL>(OrderIso.sumDualDistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inl (OrderDual.toDual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>b : β<GOAL>(OrderIso.sumDualDistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inr (OrderDual.toDual b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<GOAL>(OrderIso.sumDualDistrib α β).symm (Sum.inl (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>b : β<GOAL>(OrderIso.sumDualDistrib α β).symm (Sum.inr (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>a : α<GOAL>(OrderIso.sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inl a)))) = toLex (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>b : β<GOAL>(OrderIso.sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inr b)))) = toLex (Sum.inr (toLex (Sum.inl b)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>c : γ<GOAL>(OrderIso.sumLexAssoc α β γ) (toLex (Sum.inr c)) = toLex (Sum.inr (toLex (Sum.inr c)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>a : α<GOAL>(OrderIso.sumLexAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>b : β<GOAL>(OrderIso.sumLexAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>c : γ<GOAL>(OrderIso.sumLexAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<GOAL>(OrderIso.sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inr (OrderDual.toDual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>b : β<GOAL>(OrderIso.sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inl (OrderDual.toDual b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>b : β<GOAL>(OrderIso.sumLexDualAntidistrib α β).symm (Sum.inl (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a : α<GOAL>(OrderIso.sumLexDualAntidistrib α β).symm (Sum.inr (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)
<VAR>α : Type u_1<VAR>LE α<GOAL>WithBot.orderIsoPUnitSumLex ⊥ = toLex (Sum.inl PUnit.unit)
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>WithBot.orderIsoPUnitSumLex ↑a = toLex (Sum.inr a)
<VAR>α : Type u_1<VAR>LE α<VAR>x : PUnit.{u_5 + 1}<GOAL>WithBot.orderIsoPUnitSumLex.symm (toLex (Sum.inl x)) = ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>WithBot.orderIsoPUnitSumLex.symm (toLex (Sum.inr a)) = ↑a
<VAR>α : Type u_1<VAR>LE α<GOAL>WithTop.orderIsoSumLexPUnit ⊤ = toLex (Sum.inr PUnit.unit)
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>WithTop.orderIsoSumLexPUnit ↑a = toLex (Sum.inl a)
<VAR>α : Type u_1<VAR>LE α<VAR>x : PUnit.{u_5 + 1}<GOAL>WithTop.orderIsoSumLexPUnit.symm (toLex (Sum.inr x)) = ⊤
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>WithTop.orderIsoSumLexPUnit.symm (toLex (Sum.inl a)) = ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroupWithOne α<VAR>AddGroupWithOne β<VAR>n : ℤ<GOAL>(↑n).1 = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroupWithOne α<VAR>AddGroupWithOne β<VAR>n : ℤ<GOAL>(↑n).2 = ↑n
<VAR>n : ℕ<GOAL>(-1) ^ n ≠ 0
<VAR>x : ℤ<VAR>h1 : x ^ 2 < 4<VAR>h2 : x ≠ 0<GOAL>x ^ 2 = 1
<VAR>x : ℤ<VAR>h1 : x ^ 2 ≤ 3<VAR>h2 : x ≠ 0<GOAL>x ^ 2 = 1
<VAR>a b : ℤ<GOAL>a.natAbs = b.natAbs ↔ a * a = b * b
<VAR>a b : ℤ<GOAL>a.natAbs < b.natAbs ↔ a * a < b * b
<VAR>a b : ℤ<GOAL>a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
<VAR>m x : ℤ<VAR>h1 : m ∣ x<VAR>h2 : |x| < m<GOAL>x = 0
<VAR>F : PFunctor.{u}<VAR>x y : PFunctor.Approx.CofixA F 0<GOAL>x = y
<VAR>F : PFunctor.{u}<VAR>n : ℕ<VAR>x : PFunctor.Approx.CofixA F (n + 1)<GOAL>x = PFunctor.Approx.CofixA.intro (PFunctor.Approx.head' x) (PFunctor.Approx.children' x)
<VAR>F : PFunctor.{u}<VAR>x : PFunctor.Approx.CofixA F 0<VAR>y : PFunctor.Approx.CofixA F 1<GOAL>PFunctor.Approx.Agree x y
<VAR>F : PFunctor.{u}<VAR>n : ℕ<VAR>x : PFunctor.Approx.CofixA F n.succ<VAR>y : PFunctor.Approx.CofixA F (n.succ + 1)<VAR>i : F.B (PFunctor.Approx.head' x)<VAR>j : F.B (PFunctor.Approx.head' y)<VAR>h₀ : HEq i j<VAR>h₁ : PFunctor.Approx.Agree x y<GOAL>PFunctor.Approx.Agree (PFunctor.Approx.children' x i) (PFunctor.Approx.children' y j)
<VAR>F : PFunctor.{u}<VAR>n : ℕ<VAR>x : PFunctor.Approx.CofixA F n<VAR>y : PFunctor.Approx.CofixA F n.succ<VAR>h : PFunctor.Approx.Agree x y<GOAL>PFunctor.Approx.truncate y = x
<VAR>F : PFunctor.{u}<VAR>X : Type w<VAR>f : X → ↑F X<VAR>i : X<VAR>n : ℕ<GOAL>PFunctor.Approx.Agree (PFunctor.Approx.sCorec f i n) (PFunctor.Approx.sCorec f i n.succ)
<VAR>F : PFunctor.{u}<VAR>n m : ℕ<VAR>x : (n : ℕ) → PFunctor.Approx.CofixA F n<VAR>Hconsistent : PFunctor.Approx.AllAgree x<GOAL>PFunctor.Approx.head' (x n.succ) = PFunctor.Approx.head' (x m.succ)
<VAR>F : PFunctor.{u}<VAR>self : F.MIntl<GOAL>PFunctor.Approx.AllAgree self.approx
<VAR>F : PFunctor.{u}<VAR>Inhabited F.A<VAR>n : ℕ<GOAL>PFunctor.Approx.Agree default default
<VAR>F : PFunctor.{u}<VAR>x y : F.M<VAR>H : ∀ (i : ℕ), x.approx i = y.approx i<GOAL>x = y
<VAR>F : PFunctor.{u}<VAR>n m : ℕ<VAR>x : F.M<GOAL>PFunctor.Approx.head' (x.approx n.succ) = PFunctor.Approx.head' (x.approx m.succ)
<VAR>F : PFunctor.{u}<VAR>x : F.M<VAR>n : ℕ<GOAL>x.head = PFunctor.Approx.head' (x.approx (n + 1))
<VAR>F : PFunctor.{u}<VAR>x : F.M<VAR>n : ℕ<GOAL>PFunctor.Approx.head' (x.approx (n + 1)) = x.head
<VAR>F : PFunctor.{u}<VAR>x : F.M<VAR>n : ℕ<GOAL>PFunctor.Approx.truncate (x.approx (n + 1)) = x.approx n
<VAR>F : PFunctor.{u}<VAR>x : ↑F F.M<GOAL>PFunctor.Approx.AllAgree (PFunctor.M.Approx.sMk x)
<VAR>F : PFunctor.{u}<VAR>x : ↑F F.M<GOAL>(PFunctor.M.mk x).dest = x
<VAR>F : PFunctor.{u}<VAR>x : F.M<GOAL>PFunctor.M.mk x.dest = x
<VAR>F : PFunctor.{u}<VAR>x y : ↑F F.M<VAR>h : PFunctor.M.mk x = PFunctor.M.mk y<GOAL>x = y
<VAR>F : PFunctor.{u}<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : ℕ<GOAL>(PFunctor.M.mk ⟨a, f⟩).approx i.succ = PFunctor.Approx.CofixA.intro a fun j => (f j).approx i
<VAR>F : PFunctor.{u}<VAR>n : ℕ<VAR>x : F.M<GOAL>PFunctor.M.Agree' n x x
<VAR>F : PFunctor.{u}<VAR>n : ℕ<VAR>x y : F.M<GOAL>PFunctor.Approx.Agree (x.approx n) (y.approx (n + 1)) ↔ PFunctor.M.Agree' n x y
<VAR>F : PFunctor.{u}<VAR>r : F.M → Sort u_2<VAR>x : ↑F F.M<VAR>f : (x : ↑F F.M) → r (PFunctor.M.mk x)<GOAL>PFunctor.M.cases f (PFunctor.M.mk x) = f x
<VAR>F : PFunctor.{u}<VAR>r : F.M → Sort u_2<VAR>x : ↑F F.M<VAR>f : (x : ↑F F.M) → r (PFunctor.M.mk x)<GOAL>(PFunctor.M.mk x).casesOn f = f x
<VAR>F : PFunctor.{u}<VAR>r : F.M → Sort u_2<VAR>a : F.A<VAR>x : F.B a → F.M<VAR>f : (a : F.A) → (f : F.B a → F.M) → r (PFunctor.M.mk ⟨a, f⟩)<GOAL>(PFunctor.M.mk ⟨a, x⟩).casesOn' f = f a x
<VAR>F : PFunctor.{u}<VAR>xs : PFunctor.Approx.Path F<VAR>a a' : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a'<GOAL>PFunctor.M.IsPath (⟨a', i⟩ :: xs) (PFunctor.M.mk ⟨a, f⟩) → a = a'
<VAR>F : PFunctor.{u}<VAR>xs : PFunctor.Approx.Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<GOAL>PFunctor.M.IsPath (⟨a, i⟩ :: xs) (PFunctor.M.mk ⟨a, f⟩) → PFunctor.M.IsPath xs (f i)
<VAR>F : PFunctor.{u}<VAR>DecidableEq F.A<VAR>Inhabited F.M<VAR>ps : PFunctor.Approx.Path F<VAR>x : F.M<VAR>h : ¬PFunctor.M.IsPath ps x<GOAL>PFunctor.M.iselect ps x = default.head
<VAR>F : PFunctor.{u}<VAR>x : ↑F F.M<GOAL>(PFunctor.M.mk x).head = x.fst
<VAR>F : PFunctor.{u}<VAR>a : F.A<VAR>x : F.B a → F.M<VAR>i : F.B (PFunctor.M.mk ⟨a, x⟩).head<GOAL>(PFunctor.M.mk ⟨a, x⟩).children i = x (cast ⋯ i)
<VAR>F : PFunctor.{u}<VAR>DecidableEq F.A<VAR>Inhabited F.M<VAR>x : ↑F F.M<VAR>i : F.Idx<GOAL>PFunctor.M.ichildren i (PFunctor.M.mk x) = x.iget i
<VAR>F : PFunctor.{u}<VAR>DecidableEq F.A<VAR>Inhabited F.M<VAR>ps : PFunctor.Approx.Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<GOAL>PFunctor.M.isubtree (⟨a, i⟩ :: ps) (PFunctor.M.mk ⟨a, f⟩) = PFunctor.M.isubtree ps (f i)
<VAR>F : PFunctor.{u}<VAR>DecidableEq F.A<VAR>Inhabited F.M<VAR>a : F.A<VAR>f : F.B a → F.M<GOAL>PFunctor.M.iselect [] (PFunctor.M.mk ⟨a, f⟩) = a
<VAR>F : PFunctor.{u}<VAR>DecidableEq F.A<VAR>Inhabited F.M<VAR>ps : PFunctor.Approx.Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<GOAL>PFunctor.M.iselect (⟨a, i⟩ :: ps) (PFunctor.M.mk ⟨a, f⟩) = PFunctor.M.iselect ps (f i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_2<VAR>f : X → ↑F X<VAR>x₀ : X<GOAL>PFunctor.M.corec f x₀ = PFunctor.M.mk (F.map (PFunctor.M.corec f) (f x₀))
<VAR>F : PFunctor.{u}<VAR>Inhabited F.M<VAR>DecidableEq F.A<VAR>n : ℕ<VAR>x y z : F.M<VAR>hx : PFunctor.M.Agree' n z x<VAR>hy : PFunctor.M.Agree' n z y<VAR>hrec : ∀ (ps : PFunctor.Approx.Path F), n = List.length ps → PFunctor.M.iselect ps x = PFunctor.M.iselect ps y<GOAL>x.approx (n + 1) = y.approx (n + 1)
<VAR>F : PFunctor.{u}<VAR>Inhabited F.M<VAR>x y : F.M<VAR>H : ∀ (ps : PFunctor.Approx.Path F), PFunctor.M.iselect ps x = PFunctor.M.iselect ps y<GOAL>x = y
<VAR>F : PFunctor.{u}<VAR>R : F.M → F.M → Prop<VAR>self : PFunctor.M.IsBisimulation R<VAR>a : F.A<VAR>f f' : F.B a → F.M<GOAL>R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)
<VAR>F : PFunctor.{u}<VAR>R : F.M → F.M → Prop<VAR>self : PFunctor.M.IsBisimulation R<VAR>a a' : F.A<VAR>f : F.B a → F.M<VAR>f' : F.B a' → F.M<GOAL>R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a', f'⟩) → a = a'
<VAR>F : PFunctor.{u}<VAR>R : F.M → F.M → Prop<VAR>Inhabited F.M<VAR>bisim : PFunctor.M.IsBisimulation R<VAR>s₁ s₂ : F.M<VAR>ps : PFunctor.Approx.Path F<GOAL>R s₁ s₂ → PFunctor.M.IsPath ps s₁ ∨ PFunctor.M.IsPath ps s₂ → PFunctor.M.iselect ps s₁ = PFunctor.M.iselect ps s₂ ∧ ∃ a f f', PFunctor.M.isubtree ps s₁ = PFunctor.M.mk ⟨a, f⟩ ∧ PFunctor.M.isubtree ps s₂ = PFunctor.M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
<VAR>F : PFunctor.{u}<VAR>R : F.M → F.M → Prop<VAR>Nonempty F.M<VAR>bisim : PFunctor.M.IsBisimulation R<VAR>s₁ s₂ : F.M<GOAL>R s₁ s₂ → s₁ = s₂
<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>x : α<GOAL>(PFunctor.M.corec g x).dest = P.map (PFunctor.M.corec g) (g x)
<VAR>P : PFunctor.{u}<VAR>R : P.M → P.M → Prop<VAR>h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)<VAR>x y : P.M<GOAL>R x y → x = y
<VAR>P : PFunctor.{u}<VAR>α : Type u_3<VAR>Q : α → Prop<VAR>u v : α → P.M<VAR>h : ∀ (x : α), Q x → ∃ a f f', (u x).dest = ⟨a, f⟩ ∧ (v x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'<VAR>x : α<GOAL>Q x → u x = v x
<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<GOAL>f = PFunctor.M.corec g
<VAR>a b : ℤ<VAR>c : ℕ<VAR>ha : a.natAbs ≠ 1<VAR>hb : b.natAbs ≠ 1<VAR>hc : a * b = ↑c<GOAL>¬Nat.Prime c
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<GOAL>↑(p ^ (k + 1)) ∣ m ∨ ↑(p ^ (l + 1)) ∣ n
<VAR>s : Set ℤ<VAR>DecidablePred fun x => x ∈ s<VAR>b : ℤ<VAR>Hb : ∀ z ∈ s, z ≤ b<VAR>Hinh : ∃ z, z ∈ s<GOAL>sSup s = ↑(b.greatestOfBdd Hb Hinh)
<VAR>s : Set ℤ<VAR>h : ¬BddAbove s<GOAL>sSup s = 0
<VAR>s : Set ℤ<VAR>DecidablePred fun x => x ∈ s<VAR>b : ℤ<VAR>Hb : ∀ z ∈ s, b ≤ z<VAR>Hinh : ∃ z, z ∈ s<GOAL>sInf s = ↑(b.leastOfBdd Hb Hinh)
<VAR>s : Set ℤ<VAR>h : ¬BddBelow s<GOAL>sInf s = 0
<VAR>s : Set ℤ<VAR>h1 : s.Nonempty<VAR>h2 : BddBelow s<GOAL>sInf s ∈ s
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>P : Prop<VAR>Decidable P<VAR>m n : ℤ<GOAL>↑(if P then m else n) = if P then ↑m else ↑n
<VAR>α : Type u_3<VAR>AddGroupWithOne α<GOAL>⇑(Int.castAddHom α) = fun x => ↑x
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>n : ℤ<VAR>h : Even n<GOAL>Even ↑n
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>CharZero α<VAR>n : ℤ<GOAL>↑n = 0 ↔ n = 0
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>CharZero α<VAR>m n : ℤ<GOAL>↑m = ↑n ↔ m = n
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>CharZero α<GOAL>Function.Injective Int.cast
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>CharZero α<VAR>n : ℤ<GOAL>↑n ≠ 0 ↔ n ≠ 0
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>CharZero α<VAR>n : ℤ<GOAL>↑n = 1 ↔ n = 1
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>CharZero α<VAR>n : ℤ<GOAL>↑n ≠ 1 ↔ n ≠ 1
<VAR>α : Type u_3<VAR>NonAssocRing α<GOAL>⇑(Int.castRingHom α) = fun x => ↑x
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>n : ℤ<VAR>a : α<GOAL>Commute (↑n) a
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>n : ℤ<VAR>x : α<GOAL>↑n * x = x * ↑n
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>a : α<VAR>n : ℤ<GOAL>Commute a ↑n
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>a : α<VAR>n : ℤ<GOAL>n • a = ↑n * a
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>a : α<VAR>n : ℤ<GOAL>n • a = a * ↑n
<VAR>α : Type u_3<VAR>Ring α<VAR>n : ℤ<VAR>hn : Odd n<GOAL>Odd ↑n
<VAR>α : Type u_3<VAR>CommRing α<VAR>m n : ℤ<VAR>h : m ∣ n<GOAL>↑m ∣ ↑n
<VAR>α : Type u_3<VAR>Ring α<VAR>a x y : α<VAR>h : SemiconjBy a x y<VAR>n : ℤ<GOAL>SemiconjBy a (↑n * x) (↑n * y)
<VAR>α : Type u_3<VAR>Ring α<VAR>a x y : α<VAR>h : SemiconjBy a x y<VAR>n : ℤ<GOAL>SemiconjBy (↑n * a) x y
<VAR>α : Type u_3<VAR>Ring α<VAR>a x y : α<VAR>h : SemiconjBy a x y<VAR>m n : ℤ<GOAL>SemiconjBy (↑m * a) (↑n * x) (↑n * y)
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>a : α<VAR>n : ℤ<GOAL>Commute (↑n) a
<VAR>α : Type u_3<VAR>Ring α<VAR>a b : α<VAR>h : Commute a b<VAR>m : ℤ<GOAL>Commute a (↑m * b)
<VAR>α : Type u_3<VAR>Ring α<VAR>a b : α<VAR>h : Commute a b<VAR>m : ℤ<GOAL>Commute (↑m * a) b
<VAR>α : Type u_3<VAR>Ring α<VAR>a b : α<VAR>h : Commute a b<VAR>m n : ℤ<GOAL>Commute (↑m * a) (↑n * b)
<VAR>α : Type u_3<VAR>Ring α<VAR>a : α<VAR>n : ℤ<GOAL>Commute a (↑n * a)
<VAR>α : Type u_3<VAR>Ring α<VAR>a : α<VAR>n : ℤ<GOAL>Commute (↑n * a) a
<VAR>α : Type u_3<VAR>Ring α<VAR>a : α<VAR>m n : ℤ<GOAL>Commute (↑m * a) (↑n * a)
<VAR>A : Type u_5<VAR>AddMonoid A<VAR>f g : ℤ →+ A<VAR>h1 : f 1 = g 1<GOAL>f = g
<VAR>A : Type u_5<VAR>AddGroupWithOne A<VAR>f : ℤ →+ A<VAR>h1 : f 1 = 1<GOAL>f = Int.castAddHom A
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>FunLike F ℤ α<VAR>AddMonoidHomClass F ℤ α<VAR>f : F<VAR>h₁ : f 1 = 1<VAR>n : ℤ<GOAL>f n = ↑n
<VAR>α : Type u_3<VAR>AddGroupWithOne α<VAR>n : ℤ<GOAL>n • 1 = ↑n
<GOAL>Int.castAddHom ℤ = AddMonoidHom.id ℤ
<VAR>M : Type u_5<VAR>Monoid M<VAR>f g : Multiplicative ℤ →* M<VAR>h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)<GOAL>f = g
<VAR>M : Type u_5<VAR>Monoid M<VAR>f g : ℤ →* M<VAR>h_neg_one : f (-1) = g (-1)<VAR>h_nat : f.comp ↑Int.ofNatHom = g.comp ↑Int.ofNatHom<GOAL>f = g
<VAR>M : Type u_5<VAR>MonoidWithZero M<VAR>f g : ℤ →*₀ M<VAR>h_neg_one : f (-1) = g (-1)<VAR>h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom<GOAL>f = g
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>MonoidWithZero α<VAR>FunLike F ℤ α<VAR>MonoidWithZeroHomClass F ℤ α<VAR>f g : F<VAR>h_neg_one : f (-1) = g (-1)<VAR>h_pos : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n<GOAL>f = g
<VAR>β : Type u_4<VAR>AddGroup β<VAR>x : β<VAR>n : ℤ<GOAL>((zmultiplesHom β) x) n = n • x
<VAR>β : Type u_4<VAR>AddGroup β<VAR>f : ℤ →+ β<GOAL>(zmultiplesHom β).symm f = f 1
<VAR>α : Type u_3<VAR>Group α<VAR>x : α<VAR>n : Multiplicative ℤ<GOAL>((zpowersHom α) x) n = x ^ Multiplicative.toAdd n
<VAR>α : Type u_3<VAR>Group α<VAR>f : Multiplicative ℤ →* α<GOAL>(zpowersHom α).symm f = f (Multiplicative.ofAdd 1)
<VAR>α : Type u_3<VAR>Group α<VAR>f : Multiplicative ℤ →* α<VAR>n : Multiplicative ℤ<GOAL>f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
<VAR>β : Type u_4<VAR>AddGroup β<VAR>f : ℤ →+ β<VAR>n : ℤ<GOAL>f n = n • f 1
<VAR>α : Type u_3<VAR>CommGroup α<VAR>x : α<VAR>n : Multiplicative ℤ<GOAL>((zpowersMulHom α) x) n = x ^ Multiplicative.toAdd n
<VAR>α : Type u_3<VAR>CommGroup α<VAR>f : Multiplicative ℤ →* α<GOAL>(zpowersMulHom α).symm f = f (Multiplicative.ofAdd 1)
<VAR>β : Type u_4<VAR>AddCommGroup β<VAR>x : β<VAR>n : ℤ<GOAL>((zmultiplesAddHom β) x) n = n • x
<VAR>β : Type u_4<VAR>AddCommGroup β<VAR>f : ℤ →+ β<GOAL>(zmultiplesAddHom β).symm f = f 1
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>FunLike F ℤ α<VAR>RingHomClass F ℤ α<VAR>f : F<VAR>n : ℤ<GOAL>f n = ↑n
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>NonAssocRing α<VAR>NonAssocRing β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>n : ℤ<GOAL>f ↑n = ↑n
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>f : ℤ →+* α<GOAL>f = Int.castRingHom α
<VAR>R : Type u_5<VAR>NonAssocSemiring R<VAR>f g : ℤ →+* R<GOAL>f = g
<GOAL>Int.castRingHom ℤ = RingHom.id ℤ
<VAR>ι : Type u_2<VAR>π : ι → Type u_5<VAR>(i : ι) → IntCast (π i)<VAR>n : ℤ<VAR>i : ι<GOAL>↑n i = ↑n
<VAR>ι : Type u_2<VAR>π : ι → Type u_5<VAR>(i : ι) → IntCast (π i)<VAR>n : ℤ<GOAL>↑n = fun x => ↑n
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>γ : Type u_7<VAR>IntCast γ<VAR>n : ℤ<GOAL>Sum.elim ↑n ↑n = ↑n
<VAR>s t : ℤ<VAR>r' : ℕ<VAR>s' t' : ℤ<GOAL>Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
<VAR>s : ℕ<GOAL>Nat.gcdA 0 s = 0
<VAR>s : ℕ<GOAL>Nat.gcdB 0 s = 1
<VAR>s : ℕ<VAR>h : s ≠ 0<GOAL>s.gcdA 0 = 1
<VAR>s : ℕ<VAR>h : s ≠ 0<GOAL>s.gcdB 0 = 0
<VAR>x y : ℕ<VAR>s t s' t' : ℤ<GOAL>(x.xgcdAux s t y s' t').1 = x.gcd y
<VAR>x y : ℕ<GOAL>x.xgcd y = (x.gcdA y, x.gcdB y)
<VAR>x y : ℕ<VAR>r r' : ℕ<VAR>s t s' t' : ℤ<GOAL>Nat.P x y (r, s, t) → Nat.P x y (r', s', t') → Nat.P x y (r.xgcdAux s t r' s' t')
<VAR>k n : ℕ<VAR>hkn : n.Coprime k<VAR>hk : 1 < k<GOAL>∃ m, n * m % k = 1
<VAR>i j : ℤ<GOAL>i.gcd j = i.natAbs.gcd j.natAbs
<VAR>m n : ℕ<GOAL>(↑m).gcd ↑n = m.gcd n
<VAR>x y : ℤ<GOAL>↑(x.gcd y) = x * x.gcdA y + y * x.gcdB y
<VAR>i j : ℤ<GOAL>i.lcm j = i.natAbs.lcm j.natAbs
<VAR>m n : ℕ<GOAL>(↑m).lcm ↑n = m.lcm n
<VAR>i j k : ℤ<VAR>h1 : k ∣ i<VAR>h2 : k ∣ j<GOAL>k ∣ ↑(i.gcd j)
<VAR>i j : ℤ<GOAL>i.gcd j = j.gcd i
<VAR>i j k : ℤ<GOAL>(↑(i.gcd j)).gcd k = i.gcd ↑(j.gcd k)
<VAR>i : ℤ<GOAL>i.gcd i = i.natAbs
<VAR>i : ℤ<GOAL>Int.gcd 0 i = i.natAbs
<VAR>i : ℤ<GOAL>i.gcd 0 = i.natAbs
<VAR>i : ℤ<VAR>j : ℤ<VAR>hi : i ≠ 0<GOAL>0 < i.gcd j
<VAR>i : ℤ<VAR>j : ℤ<VAR>hj : j ≠ 0<GOAL>0 < i.gcd j
<VAR>i j : ℤ<GOAL>0 < i.gcd j ↔ i ≠ 0 ∨ j ≠ 0
<VAR>i j : ℤ<VAR>H : 0 < i.gcd j<GOAL>(i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1
<VAR>i k : ℤ<VAR>j : ℤ<VAR>H : i ∣ k<GOAL>i.gcd j ∣ k.gcd j
<VAR>i k : ℤ<VAR>j : ℤ<VAR>H : i ∣ k<GOAL>j.gcd i ∣ j.gcd k
<VAR>i j k : ℤ<GOAL>i.gcd j ∣ (k * i).gcd j
<VAR>i j k : ℤ<GOAL>i.gcd j ∣ (i * k).gcd j
<VAR>i j k : ℤ<GOAL>i.gcd j ∣ i.gcd (k * j)
<VAR>i j k : ℤ<GOAL>i.gcd j ∣ i.gcd (j * k)
<VAR>a : ℤ<VAR>m n : ℕ<VAR>h : a.gcd (↑m * ↑n) = 1<GOAL>a.gcd ↑m = 1
<VAR>a : ℤ<VAR>m n : ℕ<VAR>h : a.gcd (↑m * ↑n) = 1<GOAL>a.gcd ↑n = 1
<VAR>i j : ℤ<VAR>H : i ∣ j<GOAL>i.gcd j = i.natAbs
<VAR>m n : ℤ<VAR>H : 0 < m.gcd n<GOAL>∃ m' n', m'.gcd n' = 1 ∧ m = m' * ↑(m.gcd n) ∧ n = n' * ↑(m.gcd n)
<VAR>m n : ℤ<VAR>H : 0 < m.gcd n<GOAL>∃ g m' n', 0 < g ∧ m'.gcd n' = 1 ∧ m = m' * ↑g ∧ n = n' * ↑g
<VAR>a b : ℤ<VAR>n : ℕ<GOAL>a.gcd b ∣ n ↔ ∃ x y, ↑n = a * x + b * y
<VAR>a b d : ℤ<VAR>hd_pos : 0 ≤ d<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<VAR>hd : ∀ (e : ℤ), e ∣ a → e ∣ b → e ∣ d<GOAL>d = ↑(a.gcd b)
<VAR>a b c : ℤ<VAR>habc : a ∣ b * c<VAR>hab : a.gcd c = 1<GOAL>a ∣ b
<VAR>i j : ℤ<GOAL>i.lcm j = j.lcm i
<VAR>i : ℤ<GOAL>Int.lcm 0 i = 0
<VAR>i : ℤ<GOAL>i.lcm 0 = 0
<VAR>i : ℤ<GOAL>Int.lcm 1 i = i.natAbs
<VAR>i : ℤ<GOAL>i.lcm 1 = i.natAbs
<VAR>i j k : ℤ<GOAL>i ∣ k → j ∣ k → ↑(i.lcm j) ∣ k
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<VAR>m n : ℕ<VAR>hm : x ^ m = 1<VAR>hn : x ^ n = 1<GOAL>x ^ m.gcd n = 1