ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.17320, u_1} C<VAR>X : C<GOAL>𝟙 X ≫ 𝟙 X = 𝟙 X
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.17320, u_1} C<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>f = ((fun X => { X := X, p := 𝟙 X, idem := ⋯ }) X✝).p ≫ f ≫ ((fun X => { X := X, p := 𝟙 X, idem := ⋯ }) Y✝).p
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ht : t ∈ 𝓝 x<GOAL>DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>inst✝ : IsSymm α r<GOAL>maximals r s = minimals r s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffAt 𝕜 n f x<VAR>hg : f₁ =ᶠ[𝓝 x] f<GOAL>f₁ =ᶠ[𝓝[univ] x] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M✝ : Type u_3<VAR>inst✝⁵ : AddCommMonoid M✝<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : T2Space M✝<VAR>v✝ : VectorMeasure α M✝<VAR>f : ℕ → Set α<VAR>M : Type u_4<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>A B : Set α<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<VAR>h : A ⊆ B<GOAL>↑v (B \ A) = ↑v B - ↑v A
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<GOAL>closedBall x ε =ᶠ[ae volume] ball x ε
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hε : ε ≤ 0<GOAL>closedBall x ε =ᶠ[ae volume] ball x ε
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>closedBall x ε =ᶠ[ae volume] ball x ε
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>β : ι → Type u_3<VAR>m : (i : ι) → α i → β i<GOAL>map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>β : ι → Type u_3<VAR>m : (i : ι) → α i → β i<GOAL>∀ (x : Set ((i : ι) → β i)), (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) → ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>(x \ y)ᶜ = x ⇨ y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<VAR>a✝ : Nontrivial R<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<VAR>a✝ : Nontrivial R<VAR>s : Finset ↥(M ⊓ N)<VAR>h : LinearIndependent R fun i => ↑i<GOAL>s.card ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<VAR>a✝ : Nontrivial R<VAR>s : Finset ↥(M ⊓ N)<VAR>h : LinearIndependent R fun i => ↑i<VAR>hs : ¬s.card ≤ 1<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<VAR>a✝ : Nontrivial R<VAR>s : Finset ↥(M ⊓ N)<VAR>h : LinearIndependent R fun i => ↑i<VAR>hs : Nontrivial { x // x ∈ s }<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<VAR>a✝ : Nontrivial R<VAR>s : Finset ↥(M ⊓ N)<VAR>h : LinearIndependent R fun i => ↑i<VAR>hs : Nontrivial { x // x ∈ s }<VAR>a b : { x // x ∈ s }<VAR>hab : a ≠ b<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<VAR>a✝ : Nontrivial R<VAR>s : Finset ↥(M ⊓ N)<VAR>h : LinearIndependent R fun i => ↑i<VAR>hs : Nontrivial { x // x ∈ s }<VAR>a b : { x // x ∈ s }<VAR>hab : a ≠ b<GOAL>LinearIndependent R ![↑a, ↑b]
<VAR>a b : Ordinal.{u_1}<GOAL>a < b → beth a < beth b
<VAR>b : Ordinal.{u_1}<VAR>IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k<VAR>a : Ordinal.{u_1}<GOAL>a < b → beth a < beth b
<VAR>b : Ordinal.{u_1}<VAR>IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k<VAR>a : Ordinal.{u_1}<VAR>h : a < b<GOAL>beth a < beth b
<VAR>a : Ordinal.{u_1}<VAR>IH : ∀ k < 0, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k<VAR>h : a < 0<GOAL>beth a < beth 0
<VAR>a c : Ordinal.{u_1}<VAR>IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k<VAR>h : a < succ c<GOAL>beth a < beth (succ c)
<VAR>b : Ordinal.{u_1}<VAR>IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k<VAR>a : Ordinal.{u_1}<VAR>h : a < b<VAR>hb : b.IsLimit<GOAL>beth a < beth b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonUnitalCommSemiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>A : Matrix m n α<VAR>B : Matrix m o α<VAR>x : n → α<GOAL>(A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x : L<GOAL>(traceForm K L M) x ∈ span K (range (Weight.toLinear K L M))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x : L<GOAL>∑ c : Weight K L M, (finrank K ↥↑(weightSpace M ⇑c) • (Weight.toLinear K L M c).smulRight (Weight.toLinear K L M c)) x ∈ span K (range (Weight.toLinear K L M))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x : L<VAR>χ : Weight K L M<VAR>x✝ : χ ∈ Finset.univ<GOAL>(finrank K ↥↑(weightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)) x ∈ span K (range (Weight.toLinear K L M))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x : L<VAR>χ : Weight K L M<VAR>x✝ : χ ∈ Finset.univ<GOAL>↑(finrank K ↥↑(weightSpace M ⇑χ)) • χ x • Weight.toLinear K L M χ ∈ span K (range (Weight.toLinear K L M))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜✝ : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜✝<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜✝ E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜✝ E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>𝕜 : Type u_8<VAR>inst✝¹ : _root_.RCLike 𝕜<VAR>n : Type u_9<VAR>inst✝ : Fintype n<VAR>x : EuclideanSpace 𝕜 n<GOAL>‖x‖ = √(∑ i : n, ‖x i‖ ^ 2)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>h : upperCrossingTime a b f N (n + 1) ω ≠ N<GOAL>b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>h : upperCrossingTime a b f N (n + 1) ω ≠ N<VAR>j : ℕ<VAR>hj₁ : j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω)<VAR>hj₂ : f j ω ∈ Set.Ici b<GOAL>b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>𝒢 : Set C<VAR>h𝒢 : IsSeparating 𝒢<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0<GOAL>∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>𝒢 : Set C<VAR>h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g<GOAL>∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ (f - g) = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>s : Cone D<VAR>j : J<GOAL>(T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c)) ≫ c.π.app j = (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>s : Cone D<VAR>j : J<GOAL>T.map (T.forget.map (s.π.app j)) ≫ (D.obj j).a = s.pt.a ≫ T.forget.map (s.π.app j)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J✝ : Type u<VAR>inst✝ : Category.{v, u} J✝<VAR>D : J✝ ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>s : Cone D<VAR>m : s.pt ⟶ (liftedCone D c t).pt<VAR>J : ∀ (j : J✝), m ≫ (liftedCone D c t).π.app j = s.π.app j<GOAL>m.f = ((fun s => { f := t.lift (T.forget.mapCone s), h := ⋯ }) s).f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J✝ : Type u<VAR>inst✝ : Category.{v, u} J✝<VAR>D : J✝ ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>s : Cone D<VAR>m : s.pt ⟶ (liftedCone D c t).pt<VAR>J : ∀ (j : J✝), m ≫ (liftedCone D c t).π.app j = s.π.app j<GOAL>∀ (j : J✝), m.f ≫ c.π.app j = ((fun s => { f := t.lift (T.forget.mapCone s), h := ⋯ }) s).f ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J✝ : Type u<VAR>inst✝ : Category.{v, u} J✝<VAR>D : J✝ ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>s : Cone D<VAR>m : s.pt ⟶ (liftedCone D c t).pt<VAR>J : ∀ (j : J✝), m ≫ (liftedCone D c t).π.app j = s.π.app j<VAR>j : J✝<GOAL>m.f ≫ c.π.app j = ((fun s => { f := t.lift (T.forget.mapCone s), h := ⋯ }) s).f ≫ c.π.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ : Filter α<VAR>f : α × α → β<VAR>x : Filter α<VAR>y : Filter β<GOAL>Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>x : F (Fix F)<GOAL>rec g (mk x) = g (rec g <$> x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>x : F (Fix F)<VAR>this : recF g ∘ fixToW = rec g<GOAL>rec g (mk x) = g (rec g <$> x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>x : F (Fix F)<VAR>this : recF g ∘ fixToW = rec g<VAR>a : (P F).A<VAR>f : (P F).B a → Fix F<VAR>h : repr x = ⟨a, f⟩<GOAL>recF g (PFunctor.W.mk ((P F).map fixToW ⟨a, f⟩)) = g (rec g <$> x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Lattice α<VAR>a b c a₁ a₂ b₁ b₂ : α<GOAL>Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Lattice α<VAR>a b c a₁ a₂ b₁ b₂ : α<GOAL>Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : Unique ι<VAR>t : (i : ι) → Set (α i)<VAR>x✝ : α default<GOAL>x✝ ∈ uniqueElim ⁻¹' univ.pi t ↔ x✝ ∈ t default
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>s : σ<GOAL>(coeff R 0) (X s) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t<VAR>h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<GOAL>Computation.LiftRel (LiftRelO R fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s.destruct t.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t<VAR>h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t<VAR>h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<GOAL>LiftRelO R (LiftRel R) a b → LiftRelO R (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t<VAR>h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<GOAL>∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>n : ℕ<VAR>a : α<GOAL>↑(eapprox f n) a < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>n : ℕ<VAR>a : α<GOAL>((Finset.range n).sup fun c => ↑(if hs : MeasurableSet {a | ennrealRatEmbed c ≤ f a} then piecewise {a | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0 else 0) a) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>n : ℕ<VAR>a : α<GOAL>∀ b ∈ Finset.range n, ↑(if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0 else 0) a < ⊤
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>i : ι<GOAL>Continuous ⇑(p i)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>i : ι<VAR>this : TopologicalAddGroup E<GOAL>Continuous ⇑(p i)
<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>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ≥0∞<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm f p μ ≤ c • eLpNorm g 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>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ≥0∞<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>z : K<GOAL>spanSingleton R₁⁰ z * ↑I = ↑J ↔ Ideal.span {(sec R₁⁰ z).1} * I = Ideal.span {↑(sec R₁⁰ z).2} * J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (-n) = -U R (n - 2)
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁵ : Field 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<GOAL>((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst = (expSeries 𝕜 R n) fun x_1 => x.fst
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>a0 : 0 < a<VAR>d0 : 0 < d<VAR>h : a * c = b * d<GOAL>a = b ∧ c = d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>a0 : 0 < a<VAR>d0 : 0 < d<VAR>h : a * c = b * d<GOAL>¬a < b ∧ ¬c < d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab✝ : a ≤ b<VAR>hcd : c ≤ d<VAR>a0 : 0 < a<VAR>d0 : 0 < d<VAR>h : a * c = b * d<VAR>hab : a < b<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd✝ : c ≤ d<VAR>a0 : 0 < a<VAR>d0 : 0 < d<VAR>h : a * c = b * d<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f : ι → E<GOAL>‖∏ a ∈ s, f a‖ ≤ ∑ x ∈ s, ‖f x‖
<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 : Finset α<VAR>x : α<VAR>h : x ∈ t<GOAL>insert x s \ t = s \ t
<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 : Finset α<VAR>x : α<VAR>h : x ∈ t<GOAL>insert x ↑s \ ↑t = ↑s \ ↑t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>𝔖_covers : ⋃₀ 𝔖 = univ<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<VAR>φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)<GOAL>Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
<VAR>A : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝² : Category.{?u.20583, u_1} A'<VAR>inst✝¹ : Category.{?u.20587, u_2} B'<VAR>inst✝ : Category.{?u.20591, u_3} T'<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>L₁ L₂ L₃ : A ⥤ T<VAR>R₁ R₂ R₃ : B ⥤ T<VAR>X Y : Comma L₁ R₁<VAR>l : X.left ≅ Y.left<VAR>r : X.right ≅ Y.right<VAR>h : autoParam (L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) _auto✝<GOAL>L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv