ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧ ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty<VAR>h : IsOpen {a}<VAR>b : Ordinal.{u}<VAR>hb : b ∈ {a}<VAR>hb' : b ∈ s<GOAL>False
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧ ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty<VAR>h : IsOpen {a}<VAR>b : Ordinal.{u}<VAR>hb : b ∈ {a}<VAR>hb' : b ∈ s<VAR>c : Ordinal.{u}<VAR>hc : c ∈ {a}<VAR>hc' : c ∈ sᶜ<GOAL>False
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧ ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty<VAR>h : IsOpen {a}<VAR>b : Ordinal.{u}<VAR>hb : b = a<VAR>hb' : b ∈ s<VAR>c : Ordinal.{u}<VAR>hc : c = a<VAR>hc' : c ∈ sᶜ<GOAL>False
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Subsingleton α<VAR>f : α → β<VAR>x y : α<GOAL>f x = f y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>-(x₁ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ = -(x₁ - (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) - W.a₂)) - x₂ - (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂) ^ 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ - x₁ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂) * (x₁ - x₂) ^ 2) = (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ - x₁ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)))) * ((x₁ - x₂) ^ 2 * (x₁ - x₂))
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>g : α ≃ β<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<VAR>v : β → M<VAR>xs : Fin k → M<GOAL>((relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>g : α ≃ β<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<VAR>v : β → M<VAR>xs : Fin k → M<GOAL>(mapTermRel (fun n => ⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))))) (fun n => id) (fun x => id) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝¹ : Fin l → M<VAR>g : α ≃ β<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<VAR>v : β → M<VAR>xs✝ : Fin k → M<VAR>n : ℕ<VAR>t : L.Term (α ⊕ Fin n)<VAR>xs : Fin n → M<GOAL>realize (Sum.elim v xs) ((Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n)))) t) = realize (Sum.elim (v ∘ ⇑g) xs) t
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝¹ : Fin l → M<VAR>g : α ≃ β<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<VAR>v : β → M<VAR>xs✝ : Fin k → M<VAR>n : ℕ<VAR>t : L.Term (α ⊕ Fin n)<VAR>xs : Fin n → M<GOAL>realize (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) t = realize (Sum.elim (v ∘ ⇑g) xs) t
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝¹ : Fin l → M<VAR>g : α ≃ β<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<VAR>v : β → M<VAR>xs✝ : Fin k → M<VAR>n : ℕ<VAR>t : L.Term (α ⊕ Fin n)<VAR>xs : Fin n → M<GOAL>Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) = Sum.elim (v ∘ ⇑g) xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝² : AddCommGroup β✝<VAR>f✝ : α✝ → β✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : AddCommGroup β<VAR>inst✝ : AddCommGroup γ<VAR>a : FreeAbelianGroup α<VAR>f : α → β<VAR>g : β →+ γ<GOAL>(g.comp (lift f)) a = (lift (⇑g ∘ f)) a
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝² : AddCommGroup β✝<VAR>f✝ : α✝ → β✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : AddCommGroup β<VAR>inst✝ : AddCommGroup γ<VAR>a : FreeAbelianGroup α<VAR>f : α → β<VAR>g : β →+ γ<GOAL>∀ (x : α), (g.comp (lift f)) (of x) = (⇑g ∘ f) x
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => x < c<VAR>hca : c ≤ a<GOAL>filter (fun x => x < c) (Ico a b) = ∅
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => x < c<VAR>hca : c ≤ a<GOAL>∅.val = ∅
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ : Seminorm 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ≥0<GOAL>(s.sup p).closedBall x ↑r = ⋂ i ∈ s, (p i).closedBall x ↑r
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abs' (↑f j - ↑f i) < ε<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>|(fun n => (↑f n).re) j - (fun n => (↑f n).re) i| ≤ abs' (↑f j - ↑f i)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u✝ v✝ u' v' : V<VAR>p✝ : G.Walk u✝ v✝<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>∀ e ∈ p.reverse.edges, e ∈ H.edgeSet
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u✝ v✝ u' v' : V<VAR>p✝ : G.Walk u✝ v✝<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>∀ e ∈ p.edges, e ∈ H.edgeSet
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u✝ v✝ u' v' : V<VAR>p✝ : G.Walk u✝ v✝<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>(p.transfer H hp).reverse = p.reverse.transfer H ⋯
<VAR>m s n : Nat<GOAL>m ∈ range' s n ↔ s ≤ m ∧ m < s + n
<VAR>m s n : Nat<GOAL>(∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>bernoulliFourierCoeff k 0 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>xy : A × A<GOAL>xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>x₀ : G<VAR>ε : ℝ<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε<GOAL>0 ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → β × σ → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>a : α<GOAL>List.foldl (fun s b => h (a, s, b).1 ((a, s, b).2.2, (a, s, b).2.1)) (g a) (f a).reverse = List.foldr (fun b s => h a (b, s)) (g a) (f a)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<VAR>hw : w ≠ 0<GOAL>(trinomial k m n u v w).mirror = trinomial k (n - m + k) n w v u
<VAR>α : Type u<VAR>ι : Sort v<VAR>t : ι → TopologicalSpace α<VAR>s : Set α<GOAL>s ∈ {s | IsOpen s} ↔ s ∈ {x | ∀ (i : ι), IsOpen x}
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (LinearMap.fst R M M₂) (fst R M M₂) = ⊤
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>⊤ ≤ map (LinearMap.fst R M M₂) (fst R M M₂)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<GOAL>x ∈ map (LinearMap.fst R M M₂) (fst R M M₂)
<VAR>α : Type u_1<VAR>inst✝⁹ : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝³ : TopologicalSpace A₂<VAR>inst✝² : Semiring A₂<VAR>inst✝¹ : Algebra R A₂<VAR>inst✝ : TopologicalSemiring A₂<VAR>k : R<VAR>a : α<GOAL>((algebraMap R C(α, A)) k) a = k • 1
<VAR>α : Type u_1<VAR>inst✝⁹ : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝³ : TopologicalSpace A₂<VAR>inst✝² : Semiring A₂<VAR>inst✝¹ : Algebra R A₂<VAR>inst✝ : TopologicalSemiring A₂<VAR>k : R<VAR>a : α<GOAL>(k • 1) a = k • 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M✝ : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M✝<VAR>a b : α<VAR>s t : Set α<VAR>M : Type u_7<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>h : ∀ (i : ι), 1 ≤ f i<VAR>hf : (mulSupport f).Finite<VAR>i : ι<VAR>hi : 1 < f i<GOAL>1 < ∏ᶠ (i : ι), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M✝ : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M✝<VAR>a b : α<VAR>s t : Set α<VAR>M : Type u_7<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>h : ∀ (i : ι), 1 ≤ f i<VAR>hf : (mulSupport f).Finite<VAR>i : ι<VAR>hi : 1 < f i<GOAL>1 < ∏ i ∈ hf.toFinset, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M✝ : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M✝<VAR>a b : α<VAR>s t : Set α<VAR>M : Type u_7<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>h : ∀ (i : ι), 1 ≤ f i<VAR>hf : (mulSupport f).Finite<VAR>i : ι<VAR>hi : 1 < f i<GOAL>i ∈ hf.toFinset
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_3<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : φ.IsCovering<VAR>hφψ : (φ ⋙q ψ).IsCovering<VAR>φsur : Surjective φ.obj<VAR>u : U<GOAL>Bijective (ψ.star (φ.obj u))
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_3<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : φ.IsCovering<VAR>hφψ : (φ ⋙q ψ).IsCovering<VAR>φsur : Surjective φ.obj<VAR>u : U<GOAL>Bijective (ψ.costar (φ.obj u))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t✝ : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_1<VAR>k : Heap α → Heap α<VAR>n : Nat<VAR>le : α → α → Bool<VAR>res : FindMin α<VAR>s✝ : Heap α<VAR>m : Nat<VAR>hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize<VAR>hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n<VAR>r : Nat<VAR>a : α<VAR>c : HeapNode α<VAR>s : Heap α<VAR>eq : n = m + (cons r a c s).realSize<GOAL>Batteries.BinomialHeap.Imp.FindMin.HasSize (findMin le (k ∘ cons r a c) s (if le res.val a = true then res else { before := k, val := a, node := c, next := s })) n
<VAR>α : Type u_1<VAR>k : Heap α → Heap α<VAR>n : Nat<VAR>le : α → α → Bool<VAR>res : FindMin α<VAR>s✝ : Heap α<VAR>m : Nat<VAR>hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize<VAR>hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n<VAR>r : Nat<VAR>a : α<VAR>c : HeapNode α<VAR>s : Heap α<VAR>eq : n = m + (cons r a c s).realSize<GOAL>Batteries.BinomialHeap.Imp.FindMin.HasSize (if le res.val a = true then res else { before := k, val := a, node := c, next := s }) n
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>H : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>Splits (algebraMap K L) (X ^ ↑n - 1)
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>H : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>Splits (RingHom.id L) (X ^ ↑n - 1)
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>H : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<VAR>z : L<VAR>hz : IsPrimitiveRoot z ↑n<GOAL>Splits (RingHom.id L) (X ^ ↑n - 1)
<VAR>R : Type u_2<VAR>K : Type ?u.58132<VAR>L : Type ?u.58135<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<GOAL>(minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree
<VAR>R : Type u_2<VAR>K : Type ?u.58132<VAR>L : Type ?u.58135<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<GOAL>(minpolyDiv R x).natDegree + 1 = (minpolyDiv R x).natDegree + (X - C x).natDegree
<VAR>R : Type u_2<VAR>K : Type ?u.58132<VAR>L : Type ?u.58135<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<GOAL>(minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>f g : α → β<GOAL>∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>a : R<GOAL>(X + C a).Separable
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>a : R<GOAL>IsCoprime (X + C a) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Icc a b \ Ico a b = {b}
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<GOAL>M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<GOAL>(∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<GOAL>(∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<GOAL>(∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : e ∈ ⋂ J ∈ Js, M.closure J<VAR>he' : e ∉ M.closure (⋂₀ Js)<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : e ∉ M.closure (⋂₀ Js)<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : e ∉ M.closure (⋂₀ Js)<VAR>heEI : e ∈ M.E \ I<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>heEI : e ∈ M.E \ I<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J✝ B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>heEI : e ∈ M.E \ I<VAR>J : Set α<VAR>hJI : M.Basis J (insert e I)<VAR>heJ : insert e (⋂₀ Js) ⊆ J<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J✝ B : Set α<VAR>f x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>heEI : e ∈ M.E \ I<VAR>J : Set α<VAR>hJI : M.Basis J (insert e I)<VAR>heJ : insert e (⋂₀ Js) ⊆ J<VAR>hIb : M.Basis I (insert e I)<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J✝ B : Set α<VAR>f✝ x y : α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<VAR>hiX : ⋂₀ Js ⊆ I<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>heEI : e ∈ M.E \ I<VAR>J : Set α<VAR>hJI : M.Basis J (insert e I)<VAR>heJ : insert e (⋂₀ Js) ⊆ J<VAR>hIb : M.Basis I (insert e I)<VAR>f : α<VAR>hfIJ : f ∈ I \ J<VAR>hfb : M.Basis (insert f (J \ {e})) (insert e I)<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>J✝ B : Set α<VAR>f✝ x y : α<VAR>Js : Set (Set α)<VAR>hne : Js.Nonempty<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>J : Set α<VAR>heJ : insert e (⋂₀ Js) ⊆ J<VAR>f : α<VAR>hI : M.Indep (insert f (J \ {e}))<VAR>hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})<VAR>hiX : ⋂₀ Js ⊆ insert f (J \ {e})<VAR>heEI : e ∈ M.E \ insert f (J \ {e})<VAR>hJI : M.Basis J (insert e (insert f (J \ {e})))<VAR>hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>hfIJ : f ∈ insert f (J \ {e}) \ J<VAR>hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<GOAL>False