ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h : {x | p x}.Finite<VAR>a✝ : α<GOAL>a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.filter p Finset.univ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ι → α × α<VAR>p : Filter ι<GOAL>Tendsto f p (𝓤 α) ↔ Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<GOAL>s < {a} ↔ s = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<GOAL>s = 0 → ¬s = {a}
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>t : Multiset α<VAR>a : α<GOAL>¬0 = {a}
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n ℝ<VAR>hM : M.IsSymm<VAR>hMq : M.toQuadraticMap'.PosDef<VAR>x : n → ℝ<VAR>hx : x ≠ 0<GOAL>0 < star x ⬝ᵥ M *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n ℝ<VAR>hM : M.IsSymm<VAR>x : n → ℝ<VAR>hx : x ≠ 0<VAR>hMq : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M *ᵥ x<GOAL>0 < star x ⬝ᵥ M *ᵥ x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<VAR>t : Set α<GOAL>t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (r.comp s) l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<VAR>t : Set α<GOAL>(∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<VAR>t✝ : Set α<VAR>t : Set γ<VAR>tsets : t ∈ l<VAR>ht : r.preimage (s.preimage t) ⊆ t✝<GOAL>∃ t, (∃ t_1 ∈ l, s.preimage t_1 ⊆ t) ∧ r.preimage t ⊆ t✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : S.Finite<VAR>h : ∀ s ∈ S, IsGδ s<GOAL>IsGδ (⋃₀ S)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup N<GOAL>↑(map f (comap f H)) = ↑(f.range ⊓ H)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<VAR>hz : z = 0<GOAL>padicNorm p ↑z ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<VAR>hz : ¬z = 0<GOAL>(if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<VAR>hz : ¬z = 0<GOAL>↑p ^ (-padicValRat p ↑z) ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<VAR>hz : ¬z = 0<GOAL>¬↑z = 0
<VAR>α : Type u_1<GOAL>⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)
<VAR>α : Type u_1<GOAL>⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>H1 : f.Disjoint g<VAR>H2 : f.Disjoint h<GOAL>f.Disjoint (g * h)
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>H1 : f.Disjoint g<VAR>H2 : f.Disjoint h<GOAL>(g * h).Disjoint f
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>hp : AffineIndependent k p<GOAL>Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>hp : AffineIndependent k p<VAR>h✝ : IsEmpty ι<GOAL>Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>hp : AffineIndependent k p<VAR>h✝ : Nonempty ι<GOAL>Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>hp : AffineIndependent k p<VAR>h✝ : Nonempty ι<GOAL>Fintype.card ι - 1 ≤ finrank k ↥(vectorSpan k (Set.range p))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Fact (1 ≤ p)<GOAL>Lp.boundedContinuousFunction E p μ = (toLpHom p μ).range
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<GOAL>CompleteSpace F
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<VAR>φ : E →L[𝕜] 𝕜<VAR>hφ : φ v = 1<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<VAR>φ : E →L[𝕜] 𝕜<VAR>hφ : φ v = 1<VAR>g : ℕ → E →L[𝕜] F := fun n => ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<VAR>φ : E →L[𝕜] 𝕜<VAR>hφ : φ v = 1<VAR>g : ℕ → E →L[𝕜] F := fun n => ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)<VAR>this : CauchySeq g<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<VAR>φ : E →L[𝕜] 𝕜<VAR>hφ : φ v = 1<VAR>g : ℕ → E →L[𝕜] F := fun n => ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)<VAR>this : CauchySeq g<VAR>a : E →L[𝕜] F<VAR>ha : Tendsto g atTop (𝓝 a)<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<VAR>φ : E →L[𝕜] 𝕜<VAR>hφ : φ v = 1<VAR>g : ℕ → E →L[𝕜] F := fun n => ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)<VAR>this : CauchySeq g<VAR>a : E →L[𝕜] F<VAR>ha : Tendsto g atTop (𝓝 a)<GOAL>Tendsto f atTop (𝓝 (a v))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁵ : Field R<VAR>inst✝¹⁴ : AddCommGroup V<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace V<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : TopologicalAddGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : SeparatingDual 𝕜 E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : CompleteSpace (E →L[𝕜] F)<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>v : E<VAR>hv : v ≠ 0<VAR>φ : E →L[𝕜] 𝕜<VAR>hφ : φ v = 1<VAR>g : ℕ → E →L[𝕜] F := fun n => ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)<VAR>this✝ : CauchySeq g<VAR>a : E →L[𝕜] F<VAR>ha : Tendsto g atTop (𝓝 a)<VAR>this : Tendsto (fun n => (g n) v) atTop (𝓝 (a v))<GOAL>Tendsto f atTop (𝓝 (a v))
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalPreadditive C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g h : Y ⟶ Z<GOAL>f ⊗ (g + h) = f ⊗ g + f ⊗ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ v : Finset α<VAR>a b : α<VAR>s t u : Finset α<VAR>x : α<GOAL>x ∈ (s ∩ t) \ u ↔ x ∈ s ∩ (t \ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : One M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<GOAL>g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left c✝ parent x b)) a<GOAL>RBNode.Ordered cmp (parent.del (node red a x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left c✝ parent x b)) a<VAR>ax : All (fun a => cmpLT cmp a x) a<VAR>ap : All (RootOrdered cmp parent) a<GOAL>RBNode.Ordered cmp (parent.del (node red a x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right c✝ a x parent)) b<GOAL>RBNode.Ordered cmp (parent.del (node red a x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right c✝ a x parent)) b<VAR>xb : All (cmpLT cmp x) b<VAR>bp : All (RootOrdered cmp parent) b<GOAL>RBNode.Ordered cmp (parent.del (node red a x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left c✝ parent x b)) a<GOAL>RBNode.Ordered cmp (parent.del (a.balLeft x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left c✝ parent x b)) a<VAR>ax : All (fun a => cmpLT cmp a x) a<VAR>ap : All (RootOrdered cmp parent) a<GOAL>RBNode.Ordered cmp (parent.del (a.balLeft x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right c✝ a x parent)) b<GOAL>RBNode.Ordered cmp (parent.del (a.balRight x b) c✝)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right c✝ a x parent)) b<VAR>xb : All (cmpLT cmp x) b<VAR>bp : All (RootOrdered cmp parent) b<GOAL>RBNode.Ordered cmp (parent.del (a.balRight x b) c✝)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>Nat.card ↥H.normalizer ≡ Nat.card G [MOD p ^ (n + 1)]
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>this : ↥(H.subgroupOf H.normalizer) ≃ ↥H<GOAL>Nat.card ↥H.normalizer ≡ Nat.card G [MOD p ^ (n + 1)]
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>this : ↥(H.subgroupOf H.normalizer) ≃ ↥H<GOAL>Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) * p ^ n ≡ Nat.card (G ⧸ H) * p ^ n [MOD p * p ^ n]
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ C<VAR>adj : F ⊣ G<VAR>A₁ A₂ : Algebra F<VAR>f : A₁ ⟶ A₂<GOAL>(adj.homEquiv A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ (adj.homEquiv A₂.a A₂.a) A₂.str
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : AnalyticAt 𝕜 f x<GOAL>⋯.order = WithTop.map Nat.cast hf.order
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : AnalyticAt 𝕜 f x<VAR>ho : hf.order = ⊤<GOAL>⋯.order = WithTop.map Nat.cast hf.order
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : AnalyticAt 𝕜 f x<VAR>ho : hf.order ≠ ⊤<GOAL>⋯.order = WithTop.map Nat.cast hf.order
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.66927, u_1} C₁<VAR>inst✝⁵ : Category.{?u.66931, u_2} C₂<VAR>inst✝⁴ : Category.{?u.66935, u_3} C₃<VAR>inst✝³ : Category.{?u.66939, u_4} C₄<VAR>inst✝² : Category.{?u.66943, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.66947, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>inst✝ : ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃) j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.66927, u_1} C₁<VAR>inst✝⁵ : Category.{?u.66931, u_2} C₂<VAR>inst✝⁴ : Category.{?u.66935, u_3} C₃<VAR>inst✝³ : Category.{?u.66939, u_4} C₄<VAR>inst✝² : Category.{?u.66943, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.66947, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>inst✝ : ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ Y₃ Z₃ : GradedObject I₃ C₃<VAR>φ : X₃ ⟶ Y₃<VAR>ψ : Y₃ ⟶ Z₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (φ ≫ ψ) j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ) j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.66927, u_1} C₁<VAR>inst✝⁵ : Category.{?u.66931, u_2} C₂<VAR>inst✝⁴ : Category.{?u.66935, u_3} C₃<VAR>inst✝³ : Category.{?u.66939, u_4} C₄<VAR>inst✝² : Category.{?u.66943, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.66947, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>inst✝ : ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>φ : X₂ ⟶ Y₂<VAR>X₃ Y₃ : GradedObject I₃ C₃<VAR>ψ : X₃ ⟶ Y₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ j ≫ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 Y₃) j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) ψ j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.66927, u_1} C₁<VAR>inst✝⁵ : Category.{?u.66931, u_2} C₂<VAR>inst✝⁴ : Category.{?u.66935, u_3} C₃<VAR>inst✝³ : Category.{?u.66939, u_4} C₄<VAR>inst✝² : Category.{?u.66943, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.66947, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>inst✝ : ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ { app := fun X₃ => mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃), naturality := ⋯ }.app X₃ j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (𝟙 { obj := fun X₃ => mapTrifunctorMapObj F p X₁ X₂ X₃, map := fun {X₃ Y₃} φ => mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯, map_comp := ⋯ }).app X₃ j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.66927, u_1} C₁<VAR>inst✝⁵ : Category.{?u.66931, u_2} C₂<VAR>inst✝⁴ : Category.{?u.66935, u_3} C₃<VAR>inst✝³ : Category.{?u.66939, u_4} C₄<VAR>inst✝² : Category.{?u.66943, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.66947, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>inst✝ : ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ Y₂ Z₂ : GradedObject I₂ C₂<VAR>φ : X₂ ⟶ Y₂<VAR>ψ : Y₂ ⟶ Z₂<VAR>X₃ : GradedObject I₃ C₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h✝ : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h✝ ≫ { app := fun X₃ => mapTrifunctorMapMap F p (𝟙 X₁) (φ ≫ ψ) (𝟙 X₃), naturality := ⋯ }.app X₃ j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h✝ ≫ ({ app := fun X₃ => mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃), naturality := ⋯ } ≫ { app := fun X₃ => mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃), naturality := ⋯ }).app X₃ j
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>s : Stream'.Seq (Pair K)<VAR>inst✝ : DivisionRing K<VAR>m : ℕ<VAR>m_lt_n : m < n<GOAL>(squashSeq s n).get? m = s.get? m
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>1 = 1 % (p.length + 1)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>1 < p.length + 1