ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.toFinsupp {a} = Finsupp.single a 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>Finsupp.toMultiset (Multiset.toFinsupp s) = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>f : α →₀ ℕ<GOAL>Multiset.toFinsupp s = f ↔ s = Finsupp.toMultiset f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toFinsupp (s ∪ t) = Multiset.toFinsupp s ⊔ Multiset.toFinsupp t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toFinsupp (s ∩ t) = Multiset.toFinsupp s ⊓ Multiset.toFinsupp t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>((Multiset.toFinsupp s).sum fun x => id) = Multiset.card s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : α →₀ ℕ<GOAL>Multiset.toFinsupp (Finsupp.toMultiset f) = f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : α →₀ ℕ<VAR>s : Multiset α<GOAL>Finsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s
<VAR>ι : Type u_3<VAR>DecidableEq ι<GOAL>⇑Finsupp.orderIsoMultiset = ⇑Finsupp.toMultiset
<VAR>ι : Type u_3<VAR>DecidableEq ι<GOAL>⇑Finsupp.orderIsoMultiset.symm = ⇑Multiset.toFinsupp
<VAR>ι : Type u_3<GOAL>StrictMono ⇑Finsupp.toMultiset
<VAR>ι : Type u_3<VAR>m n : ι →₀ ℕ<VAR>h : m < n<GOAL>(m.sum fun x => id) < n.sum fun x => id
<VAR>ι : Type u_3<GOAL>WellFounded LT.lt
<VAR>ι : Type u_3<VAR>DecidableEq ι<GOAL>StrictMono ⇑Multiset.toFinsupp
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : ℕ<VAR>s : Sym α n<VAR>a : α<GOAL>↑((Sym.equivNatSum α n) s) a = Multiset.count a ↑s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : ℕ<VAR>P : { P // (P.sum fun x => id) = n }<GOAL>↑((Sym.equivNatSum α n).symm P) = Finsupp.toMultiset ↑P
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : ℕ<VAR>Fintype α<VAR>s : Sym α n<VAR>a : α<GOAL>↑((Sym.equivNatSumOfFintype α n) s) a = Multiset.count a ↑s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : ℕ<VAR>Fintype α<VAR>P : { P // ∑ i : α, P i = n }<GOAL>↑((Sym.equivNatSumOfFintype α n).symm P) = ∑ a : α, ↑P a • {a}
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<GOAL>AddSubmonoid.closure (Set.range fun x => x ^ n) = ⊤
<GOAL>AddSubmonoid.closure (Set.range fun x => x * x) = ⊤
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : Even n<GOAL>AddSubmonoid.closure (Set.range fun x => x ^ n) = AddSubmonoid.nonneg ℚ
<GOAL>AddSubmonoid.closure (Set.range fun x => x * x) = AddSubmonoid.nonneg ℚ
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<GOAL>s.destruct = Sum.inl a → s = Computation.pure a
<VAR>α : Type u<VAR>s s' : Computation α<GOAL>s.destruct = Sum.inr s' → s = s'.think
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.pure a).destruct = Sum.inl a
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.think.destruct = Sum.inr s
<VAR>α : Type u<GOAL>(Computation.empty α).destruct = Sum.inr (Computation.empty α)
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.pure a).head = some a
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.think.head = none
<VAR>α : Type u<GOAL>(Computation.empty α).head = none
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.pure a).tail = Computation.pure a
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.think.tail = s
<VAR>α : Type u<GOAL>(Computation.empty α).tail = Computation.empty α
<VAR>α : Type u<GOAL>Computation.empty α = (Computation.empty α).think
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α ⊕ β<VAR>b : β<GOAL>(Computation.corec f b).destruct = Computation.rmap (Computation.corec f) (f b)
<VAR>α : Type u<VAR>R : Computation α → Computation α → Prop<VAR>bisim : Computation.IsBisimulation R<VAR>s₁ s₂ : Computation α<VAR>r : R s₁ s₂<GOAL>s₁ = s₂
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>↑s m = some a → ↑s n = some a
<VAR>α : Type u<VAR>s : Computation α<VAR>a b : α<GOAL>a ∈ s → b ∈ s → a = b
<VAR>α : Type u<GOAL>Relator.LeftUnique fun x x_1 => x ∈ x_1
<VAR>α : Type u<VAR>s : Computation α<VAR>self : s.Terminates<GOAL>∃ a, a ∈ s
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.Terminates ↔ ∃ a, a ∈ s
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>h : a ∈ s<GOAL>s.Terminates
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.Terminates ↔ ∃ n, (↑s n).isSome = true
<VAR>α : Type u<VAR>a : α<GOAL>a ∈ Computation.pure a
<VAR>α : Type u<VAR>a a' : α<VAR>h : a' ∈ Computation.pure a<GOAL>a' = a
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<GOAL>a ∈ s → a ∈ s.think
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<GOAL>a ∈ s.think → a ∈ s
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.think.Terminates → s.Terminates
<VAR>α : Type u<VAR>a : α<GOAL>¬a ∈ Computation.empty α
<VAR>α : Type u<GOAL>¬(Computation.empty α).Terminates
<VAR>α : Type u<VAR>s : Computation α<VAR>H : ¬s.Terminates<GOAL>s = Computation.empty α
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ s.thinkN n ↔ a ∈ s
<VAR>α : Type u<VAR>s : Computation α<VAR>n : ℕ<GOAL>(s.thinkN n).Terminates → s.Terminates
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<GOAL>a ∈ s → s.Promises a
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.empty α).Promises a
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.get ∈ s
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<VAR>a : α<GOAL>a ∈ s → s.get = a
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<VAR>a : α<GOAL>s.get = a → a ∈ s
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.think.get = s.get
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<VAR>n : ℕ<GOAL>(s.thinkN n).get = s.get
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.Promises s.get
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<VAR>a : α<VAR>p : s.Promises a<GOAL>a ∈ s
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<VAR>a : α<GOAL>s.Promises a → s.get = a
<VAR>α : Type u<VAR>s : Computation α<VAR>_T : s.Terminates<GOAL>s.Results s.get s.length
<VAR>α : Type u<VAR>s : Computation α<VAR>T : s.Terminates<VAR>a : α<VAR>h : a ∈ s<GOAL>s.Results a s.length
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<GOAL>s.Results a n → a ∈ s
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.Results a n<GOAL>s.Terminates
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>_T : s.Terminates<GOAL>s.Results a n → s.length = n
<VAR>α : Type u<VAR>s : Computation α<VAR>a b : α<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : s.Results b n<GOAL>a = b
<VAR>α : Type u<VAR>s : Computation α<VAR>a b : α<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : s.Results b n<GOAL>m = n
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ n, s.Results a n
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.pure a).get = a
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.pure a).length = 0
<VAR>α : Type u<VAR>a : α<GOAL>(Computation.pure a).Results a 0
<VAR>α : Type u<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.think.length = s.length + 1
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.Results a n<GOAL>s.think.Results a (n + 1)
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.think.Results a n<GOAL>∃ m, s.Results a m ∧ n = m + 1
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<GOAL>s.think.Results a (n + 1) ↔ s.Results a n
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>m : ℕ<VAR>n : ℕ<GOAL>s.Results a m → (s.thinkN n).Results a (m + n)
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<GOAL>((Computation.pure a).thinkN n).Results a n
<VAR>α : Type u<VAR>s : Computation α<VAR>_h : s.Terminates<VAR>n : ℕ<GOAL>(s.thinkN n).length = s.length + n
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.Results a n<GOAL>s = (Computation.pure a).thinkN n
<VAR>α : Type u<VAR>s : Computation α<VAR>_h : s.Terminates<GOAL>s = (Computation.pure s.get).thinkN s.length
<VAR>α β : Type u<VAR>c : Computation α<VAR>f : α → Computation β<GOAL>c >>= f = c.bind f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Computation.map f (Computation.pure a) = Computation.pure (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Computation α<GOAL>Computation.map f s.think = (Computation.map f s).think
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Computation α<GOAL>(Computation.map f s).destruct = Computation.lmap f (Computation.rmap (Computation.map f) s.destruct)
<VAR>α : Type u<VAR>s : Computation α<GOAL>Computation.map id s = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Computation α<GOAL>Computation.map (g ∘ f) s = Computation.map g (Computation.map f s)
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : α → Computation β<GOAL>(Computation.pure a).bind f = f a
<VAR>α : Type u<VAR>β : Type v<VAR>c : Computation α<VAR>f : α → Computation β<GOAL>c.think.bind f = (c.bind f).think
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Computation α<GOAL>s.bind (Computation.pure ∘ f) = Computation.map f s
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.bind Computation.pure = s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : (f a).Results b n<GOAL>(s.bind f).Results b (n + m)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>h1 : a ∈ s<VAR>h2 : b ∈ f a<GOAL>b ∈ s.bind f
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>s.Terminates<VAR>(f s.get).Terminates<GOAL>(s.bind f).get = (f s.get).get
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>_T1 : s.Terminates<VAR>_T2 : (f s.get).Terminates<GOAL>(s.bind f).length = (f s.get).length + s.length
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>b : β<VAR>k : ℕ<GOAL>(s.bind f).Results b k → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ k = n + m
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>b : β<VAR>h : b ∈ s.bind f<GOAL>∃ a, a ∈ s ∧ b ∈ f a
<VAR>α : Type u<VAR>β : Type v<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>h1 : s.Promises a<VAR>h2 : (f a).Promises b<GOAL>(s.bind f).Promises b
<VAR>α β : Type u<VAR>f : α → β<VAR>c : Computation α<GOAL>f <$> c = Computation.map f c
<VAR>α : Type u<VAR>a : α<GOAL>pure a = Computation.pure a
<VAR>α β : Type u_1<VAR>f : α → β<VAR>a : α<GOAL>f <$> Computation.pure a = Computation.pure (f a)
<VAR>α β : Type u_1<VAR>f : α → β<VAR>s : Computation α<GOAL>f <$> s.think = (f <$> s).think
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Computation α<VAR>m : a ∈ s<GOAL>f a ∈ Computation.map f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>b : β<VAR>s : Computation α<VAR>h : b ∈ Computation.map f s<GOAL>∃ a, a ∈ s ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Computation α<GOAL>(Computation.map f s).Terminates ↔ s.Terminates
<VAR>α : Type u<VAR>a : α<VAR>c₂ : Computation α<GOAL>(HOrElse.hOrElse (Computation.pure a) fun x => c₂) = Computation.pure a
<VAR>α : Type u<VAR>c₁ : Computation α<VAR>a : α<GOAL>(HOrElse.hOrElse c₁.think fun x => Computation.pure a) = Computation.pure a
<VAR>α : Type u<VAR>c₁ c₂ : Computation α<GOAL>(HOrElse.hOrElse c₁.think fun x => c₂.think) = (HOrElse.hOrElse c₁ fun x => c₂).think
<VAR>α : Type u<VAR>c : Computation α<GOAL>(HOrElse.hOrElse (Computation.empty α) fun x => c) = c
<VAR>α : Type u<VAR>c : Computation α<GOAL>(HOrElse.hOrElse c fun x => Computation.empty α) = c
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.Equiv s
<VAR>α : Type u<VAR>s t : Computation α<GOAL>s.Equiv t → t.Equiv s
<VAR>α : Type u<VAR>s t u : Computation α<GOAL>s.Equiv t → t.Equiv u → s.Equiv u
<VAR>α : Type u<VAR>s t : Computation α<VAR>a : α<VAR>h1 : a ∈ s<VAR>h2 : a ∈ t<GOAL>s.Equiv t
<VAR>α : Type u<VAR>c₁ c₂ : Computation α<VAR>h : c₁.Equiv c₂<GOAL>c₁.Terminates ↔ c₂.Terminates
<VAR>α : Type u<VAR>c₁ c₂ : Computation α<VAR>h : c₁.Equiv c₂<VAR>a : α<GOAL>c₁.Promises a ↔ c₂.Promises a
<VAR>α : Type u<VAR>c₁ c₂ : Computation α<VAR>h : c₁.Equiv c₂<VAR>c₁.Terminates<VAR>c₂.Terminates<GOAL>c₁.get = c₂.get
<VAR>α : Type u<VAR>s : Computation α<GOAL>s.think.Equiv s
<VAR>α : Type u<VAR>s : Computation α<VAR>n : ℕ<GOAL>(s.thinkN n).Equiv s
<VAR>α : Type u<VAR>β : Type v<VAR>s1 s2 : Computation α<VAR>f1 f2 : α → Computation β<VAR>h1 : s1.Equiv s2<VAR>h2 : ∀ (a : α), (f1 a).Equiv (f2 a)<GOAL>(s1.bind f1).Equiv (s2.bind f2)
<VAR>α : Type u<VAR>s : Computation α<VAR>a : α<VAR>h : a ∈ s<GOAL>s.Equiv (Computation.pure a)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>Computation.LiftRel (Function.swap R) cb ca ↔ Computation.LiftRel R ca cb
<VAR>α : Type u<VAR>c₁ c₂ : Computation α<GOAL>Computation.LiftRel (fun x x_1 => x = x_1) c₁ c₂ ↔ c₁.Equiv c₂
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>H : Reflexive R<GOAL>Reflexive (Computation.LiftRel R)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>H : Symmetric R<GOAL>Symmetric (Computation.LiftRel R)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>H : Transitive R<GOAL>Transitive (Computation.LiftRel R)
<VAR>α : Type u<VAR>R : α → α → Prop<GOAL>Equivalence R → Equivalence (Computation.LiftRel R)
<VAR>α : Type u<VAR>β : Type v<VAR>R S : α → β → Prop<VAR>H : ∀ {a : α} {b : β}, R a b → S a b<VAR>s : Computation α<VAR>t : Computation β<GOAL>Computation.LiftRel R s t → Computation.LiftRel S s t
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Computation α<VAR>t : Computation β<GOAL>Computation.LiftRel R s t → (s.Terminates ↔ t.Terminates)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>Computation.LiftRel R ca cb → ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>ca : Computation α<VAR>cb : Computation β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>ab : R a b<GOAL>Computation.LiftRel R ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>H : Computation.LiftRel R ca cb<VAR>a : α<VAR>h : a ∈ ca<GOAL>∃ b, b ∈ cb ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>H : Computation.LiftRel R ca cb<VAR>b : β<VAR>h : b ∈ cb<GOAL>∃ a, a ∈ ca ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>Computation.LiftRel R ca cb ↔ (ca.Terminates ↔ cb.Terminates) ∧ ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → Computation γ<VAR>f2 : β → Computation δ<VAR>h1 : Computation.LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → Computation.LiftRel S (f1 a) (f2 b)<GOAL>Computation.LiftRel S (s1.bind f1) (s2.bind f2)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>a : α<VAR>cb : Computation β<GOAL>Computation.LiftRel R (Computation.pure a) cb ↔ ∃ b, b ∈ cb ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>b : β<GOAL>Computation.LiftRel R ca (Computation.pure b) ↔ ∃ a, a ∈ ca ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<GOAL>Computation.LiftRel R (Computation.pure a) (Computation.pure b) ↔ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>Computation.LiftRel R ca.think cb ↔ Computation.LiftRel R ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>Computation.LiftRel R ca cb.think ↔ Computation.LiftRel R ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>Ha : ∀ (a : α), a ∈ ca → Computation.LiftRel R ca cb<VAR>Hb : ∀ (b : β), b ∈ cb → Computation.LiftRel R ca cb<GOAL>Computation.LiftRel R ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>ca ca' : Computation α<VAR>cb cb' : Computation β<VAR>ha : ca.Equiv ca'<VAR>hb : cb.Equiv cb'<GOAL>Computation.LiftRel R ca cb ↔ Computation.LiftRel R ca' cb'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : Computation.LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<GOAL>Computation.LiftRel S (Computation.map f1 s1) (Computation.map f2 s2)
<VAR>α : Type u<VAR>β : Type v<VAR>s1 s2 : Computation α<VAR>f : α → β<VAR>h1 : s1.Equiv s2<GOAL>(Computation.map f s1).Equiv (Computation.map f s2)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>a : α<VAR>b : β<GOAL>Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>a : α<VAR>cb : Computation β<GOAL>Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b, b ∈ cb ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>b : β<VAR>ca : Computation α<GOAL>Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a, a ∈ ca ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>a : α<VAR>cb : Computation β<GOAL>Computation.LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b, b ∈ cb ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>a : α ⊕ Computation α<VAR>b : β ⊕ Computation β<GOAL>Computation.LiftRelAux (Function.swap R) (Function.swap C) b a = Computation.LiftRelAux R C a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>b : β<VAR>ca : Computation α<GOAL>Computation.LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ a, a ∈ ca ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct<VAR>ca : Computation α<VAR>cb : Computation β<VAR>Hc : C ca cb<VAR>a : α<VAR>ha : a ∈ ca<GOAL>Computation.LiftRel R ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct<VAR>ca : Computation α<VAR>cb : Computation β<VAR>Hc : C ca cb<GOAL>Computation.LiftRel R ca cb
<VAR>a : ℚ<GOAL>a.floor = a.num / ↑a.den
<VAR>z : ℤ<VAR>r : ℚ<GOAL>z ≤ r.floor ↔ ↑z ≤ r
<VAR>q : ℚ<GOAL>⌊q⌋ = q.num / ↑q.den
<VAR>n : ℤ<VAR>d : ℕ<GOAL>⌊↑n / ↑d⌋ = n / ↑d
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : ℚ<GOAL>⌊↑x⌋ = ⌊x⌋
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : ℚ<GOAL>⌈↑x⌉ = ⌈x⌉
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : ℚ<GOAL>round ↑x = round x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : ℚ<GOAL>↑(Int.fract x) = Int.fract ↑x
<VAR>q : ℚ<GOAL>q.num < (⌊q⌋ + 1) * ↑q.den
<VAR>q : ℚ<VAR>q_pos : 0 < q<GOAL>(Int.fract q⁻¹).num < q.num
<VAR>fuel : ℕ<VAR>n k : PosNum<VAR>h : (↑n).sqrt < fuel + ↑k.bit1<GOAL>↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
<VAR>n : PosNum<GOAL>↑n.minFac = (↑n).minFac
<VAR>n : Num<GOAL>↑n.minFac = (↑n).minFac
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℂ<GOAL>(∑ i ∈ s, f i).re = ∑ i ∈ s, (f i).re
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℂ<GOAL>(∑ i ∈ s, f i).im = ∑ i ∈ s, (f i).im
<VAR>p q : PosNum<GOAL>p.lor q = p ||| q
<VAR>p q : PosNum<GOAL>p.land q = p &&& q
<VAR>p q : PosNum<GOAL>p.lxor q = p ^^^ q
<VAR>p : PosNum<VAR>n : ℕ<GOAL>p.shiftl n = p <<< n
<VAR>p : PosNum<VAR>n : ℕ<GOAL>p <<< n.succ = (p <<< n).bit0
<VAR>p : PosNum<VAR>n : ℕ<GOAL>p.shiftr n = p >>> n
<VAR>p q : Num<GOAL>p.lor q = p ||| q
<VAR>p q : Num<GOAL>p.land q = p &&& q
<VAR>p q : Num<GOAL>p.lxor q = p ^^^ q
<VAR>p : Num<VAR>n : ℕ<GOAL>p.shiftl n = p <<< n
<VAR>p : Num<VAR>n : ℕ<GOAL>p.shiftr n = p >>> n
<VAR>b : Bool<GOAL>SNum.bit b (SNum.zero b) = SNum.zero b
<VAR>b : Bool<GOAL>SNum.bit b (SNum.zero (decide ¬b = true)) = SNum.nz (NzsNum.msb b)
<GOAL>FiniteDimensional.finrank ℝ ℂ = 2
<GOAL>Fact (FiniteDimensional.finrank ℝ ℂ = 2)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℂ E<GOAL>Module.rank ℝ E = 2 * Module.rank ℂ E
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℂ E<GOAL>FiniteDimensional.finrank ℝ E = 2 * FiniteDimensional.finrank ℂ E
<GOAL>Nonempty (ℂ ≃ₗ[ℚ] ℝ)
<GOAL>LinearMap.det Complex.conjAe.toLinearMap = -1
<GOAL>LinearEquiv.det Complex.conjAe.toLinearEquiv = -1
<VAR>z w : ℂ<GOAL>z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im
<VAR>z w : ℂ<GOAL>z < w ↔ z.re < w.re ∧ z.im = w.im
<VAR>z : ℂ<GOAL>0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im
<VAR>z : ℂ<GOAL>0 < z ↔ 0 < z.re ∧ 0 = z.im
<VAR>z : ℂ<GOAL>¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0
<VAR>z : ℂ<GOAL>¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0
<VAR>z : ℂ<GOAL>z.re = Complex.abs z ↔ 0 ≤ z
<VAR>z : ℂ<GOAL>-z.re = Complex.abs z ↔ z ≤ 0
<VAR>z : ℂ<GOAL>z.re = -Complex.abs z ↔ z ≤ 0
<VAR>a : ℤ<VAR>b : ℤ<VAR>b0 : b ≠ 0<GOAL>(Rat.divInt a b).num ∣ a
<VAR>a b : ℤ<GOAL>↑(Rat.divInt a b).den ∣ b
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hd : d ≠ 0<VAR>qdf : q = Rat.divInt n d<GOAL>∃ c, n = c * q.num ∧ d = c * ↑q.den
<VAR>n d : ℤ<GOAL>(Rat.divInt n d).num = d.sign * n / ↑(n.gcd d)
<VAR>n d : ℤ<GOAL>(Rat.divInt n d).den = if d = 0 then 1 else d.natAbs / n.gcd d
<VAR>q r : ℚ<GOAL>q + r = Rat.divInt (q.num * ↑r.den + ↑q.den * r.num) (↑q.den * ↑r.den)
<VAR>q : ℚ<GOAL>IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den
<VAR>n : ℤ<VAR>d : ℤ<VAR>d_ne_zero : d ≠ 0<GOAL>∃ c, n = c * (↑n / ↑d).num ∧ d = c * ↑(↑n / ↑d).den
<VAR>q r : ℚ<GOAL>(q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
<VAR>q r : ℚ<GOAL>(q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
<VAR>a b c d : ℤ<VAR>hb0 : 0 < b<VAR>hd0 : 0 < d<VAR>h1 : a.natAbs.Coprime b.natAbs<VAR>h2 : c.natAbs.Coprime d.natAbs<VAR>h : ↑a / ↑b = ↑c / ↑d<GOAL>a = c ∧ b = d
<VAR>n : ℤ<GOAL>↑(n / n) = ↑n / ↑n
<VAR>n : ℕ<GOAL>↑(n / n) = ↑n / ↑n
<VAR>a b : ℤ<VAR>h : b ∣ a<GOAL>↑(a / b) = ↑a / ↑b
<VAR>a b : ℕ<VAR>h : b ∣ a<GOAL>↑(a / b) = ↑a / ↑b
<VAR>m n : ℤ<VAR>hn : n ≠ 0<GOAL>(↑m / ↑n).den = 1 ↔ n ∣ m
<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>(↑m / ↑n).den = 1 ↔ n ∣ m
<VAR>a : ℕ<VAR>ha0 : 0 < a<GOAL>(↑a)⁻¹.num = 1
<VAR>a : ℤ<VAR>ha0 : 0 < a<GOAL>↑(↑a)⁻¹.den = a
<VAR>a : ℕ<GOAL>(↑a)⁻¹.num = (↑a).sign
<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>(OfNat.ofNat a)⁻¹.num = 1
<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>(OfNat.ofNat a)⁻¹.den = OfNat.ofNat a
<VAR>p : ℚ → Prop<GOAL>(∀ (r : ℚ), p r) ↔ ∀ (a b : ℤ), p (↑a / ↑b)
<VAR>p : ℚ → Prop<GOAL>(∃ r, p r) ↔ ∃ a b, p (↑a / ↑b)
<VAR>x : ℚ<GOAL>↑x.pnatDen = x.den
<VAR>x : ℚ<VAR>n : ℕ+<GOAL>x.pnatDen = n ↔ x.den = ↑n
<VAR>q : ℚ<GOAL>{ num := q.num, den := q.den, den_nz := ⋯, reduced := ⋯ } = q
<VAR>n : ℤ<GOAL>Rat.ofInt n = ↑n
<VAR>n : ℕ<GOAL>(OfNat.ofNat n).num = OfNat.ofNat n
<VAR>n : ℕ<GOAL>(OfNat.ofNat n).den = 1
<VAR>n : ℕ<GOAL>(↑n).num = ↑n
<VAR>n : ℤ<GOAL>(↑n).num = n
<VAR>n : ℤ<GOAL>(↑n).den = 1
<VAR>n : ℤ<GOAL>↑n = 0 ↔ n = 0
<VAR>n : ℤ<GOAL>↑n = 1 ↔ n = 1
<VAR>n : ℕ<GOAL>↑n = 1 ↔ n = 1
<VAR>n : ℤ<VAR>d : ℕ<GOAL>mkRat n d = Rat.divInt n ↑d
<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>w : (Int.natAbs 0).Coprime d<GOAL>{ num := 0, den := d, den_nz := h, reduced := w } = 0
<VAR>q : ℚ<GOAL>q.num = 0 ↔ q = 0
<VAR>q : ℚ<GOAL>q.num ≠ 0 ↔ q ≠ 0
<VAR>q : ℚ<GOAL>q.den ≠ 0
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<GOAL>Rat.divInt a b = 0 ↔ a = 0
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<GOAL>Rat.divInt a b ≠ 0 ↔ a ≠ 0
<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.gcd d = 1<GOAL>Rat.normalize n d h = { num := n, den := d, den_nz := h, reduced := c }
<VAR>q : ℚ<GOAL>Rat.divInt q.num ↑q.den = q
<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<GOAL>{ num := n, den := d, den_nz := h, reduced := c } = Rat.divInt n ↑d
<VAR>z : ℤ<GOAL>↑z = Rat.divInt z 1
<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>Rat.divInt n n = 1