ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<VAR>M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }<VAR>hM' : ↑M' ⊆ ↑U' \ ↑L'<VAR>this : ↑(L' ⊔ M') ⊆ ↑U'<GOAL>(fun s => ↑(μ.toFun s)) L' + (fun s => ↑(μ.toFun s)) M' ≤ μ.innerContent { carrier := ↑U', is_open' := ⋯ }
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<VAR>M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }<VAR>hM' : ↑M' ⊆ ↑U' \ ↑L'<VAR>this : ↑(L' ⊔ M') ⊆ ↑U'<GOAL>(fun s => ↑(μ.toFun s)) (L' ⊔ M') = (fun s => ↑(μ.toFun s)) L' + (fun s => ↑(μ.toFun s)) M'
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝² : P.toProperty.RespectsIso<VAR>H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)<VAR>Z X Y S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : Z ⟶ Y<VAR>g' : Z ⟶ X<VAR>h : IsPullback g' f' f g<VAR>hg : P g<GOAL>P g'
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝² : P.toProperty.RespectsIso<VAR>H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)<VAR>Z X Y S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : Z ⟶ Y<VAR>g' : Z ⟶ X<VAR>h : IsPullback g' f' f g<VAR>hg : P g<GOAL>P (pullback.fst f g)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : 𝕜<VAR>x y : E<GOAL>inner_ 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : 𝕜<VAR>x y : E<GOAL>↑(re r) * inner_ 𝕜 x y + ↑(im r) * (-I * inner_ 𝕜 x y) = (↑(re r) + ↑(im r) * -I) * inner_ 𝕜 x y
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>i : xr<VAR>xR : xr → PGame<VAR>j : (xR i).LeftMoves<GOAL>((xR i).moveLeft j).Subsequent (mk xl xr xL xR)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : NonUnitalSubring R<VAR>x : R × S<GOAL>x ∈ s.prod ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>degreeLT R n = Submodule.span R ↑(image (fun n => X ^ n) (range n))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>degreeLT R n ≤ Submodule.span R ↑(image (fun n => X ^ n) (range n))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>Submodule.span R ↑(image (fun n => X ^ n) (range n)) ≤ degreeLT R n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>↑(range n) ⊆ (fun n => X ^ n) ⁻¹' ↑(degreeLT R n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n k : ℕ<VAR>hk : k ∈ ↑(range n)<GOAL>k ∈ (fun n => X ^ n) ⁻¹' ↑(degreeLT R n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n k : ℕ<VAR>hk : k ∈ ↑(range n)<GOAL>((fun n => X ^ n) k).degree < ↑n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (CostructuredArrow F.op (op d))ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(unop X✝).hom.unop ≫ F.map f.unop.left.unop = (unop Y✝).hom.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (CostructuredArrow F.op (op d))ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>((unop Y✝).hom ≫ 𝟙 (op d)).unop = (unop Y✝).hom.unop
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>s * ball 1 δ = thickening δ s
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>s * ball 1 δ = ⋃ x ∈ s, ball x δ
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>s = ⋃ i ∈ s, {i}
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y x✝¹ : E<VAR>x✝ : x✝¹ ∈ s<GOAL>ball x✝¹ δ = {x✝¹} * ball 1 δ
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝² y x✝¹ : E<VAR>x✝ : x✝¹ ∈ s<VAR>x : E<GOAL>x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ
<VAR>k n : ℕ<GOAL>Pairwise (Pi.Lex (fun x x_1 => x < x_1) fun x x x_1 => x < x_1) (antidiagonalTuple (k + 1) n)
<VAR>k n : ℕ<GOAL>(∀ a ∈ antidiagonal n, Pairwise (fun a_2 b => Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a.1 a_2) (Fin.cons a.1 b)) (antidiagonalTuple k a.2)) ∧ Pairwise (fun a₁ a₂ => ∀ a ∈ antidiagonalTuple k a₁.2, ∀ a_2 ∈ antidiagonalTuple k a₂.2, Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a₁.1 a) (Fin.cons a₂.1 a_2)) (antidiagonal n)
<VAR>k n : ℕ<GOAL>(∀ (a b : ℕ), a + b = n → Pairwise (fun a_2 b => Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a a_2) (Fin.cons a b)) (antidiagonalTuple k b)) ∧ Pairwise (fun a₁ a₂ => ∀ a ∈ antidiagonalTuple k a₁.2, ∀ a_2 ∈ antidiagonalTuple k a₂.2, Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a₁.1 a) (Fin.cons a₂.1 a_2)) (antidiagonal n)
<VAR>k n : ℕ<GOAL>(∀ (a b : ℕ), a + b = n → Pairwise (fun a b => Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a b) (antidiagonalTuple k b)) ∧ Pairwise (fun a₁ a₂ => ∀ a ∈ antidiagonalTuple k a₁.2, ∀ a_2 ∈ antidiagonalTuple k a₂.2, a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2) (antidiagonal n)
<GOAL>Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)
<GOAL>Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)
<GOAL>∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Ioc a b) = Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Ioc a b) ⊆ Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>Icc a b ⊆ closure (Ioc a b)
<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>u✝ v✝ w x y : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).darts ~r c.darts
<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>u✝ v✝ w x y : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>((c.dropUntil u h).darts ++ (c.takeUntil u h).darts) ~r c.darts
<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>u✝ v✝ w x y : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>((c.takeUntil u h).darts ++ (c.dropUntil u h).darts) ~r c.darts
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>∀ (i : ι × κ), (dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N) ((b.dualBasis.tensorProduct c.dualBasis) i) = LinearMap.id ((b.dualBasis.tensorProduct c.dualBasis) i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>(dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N) ((b.dualBasis.tensorProduct c.dualBasis) (i, j)) = LinearMap.id ((b.dualBasis.tensorProduct c.dualBasis) (i, j))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>∑ x : ι, ∑ x_1 : κ, ((Finsupp.single x 1) i * (Finsupp.single x_1 1) j) • b.coord x ⊗ₜ[R] c.coord x_1 = b.coord i ⊗ₜ[R] c.coord j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = b.coord i ⊗ₜ[R] c.coord j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>∀ b_1 ∈ Finset.univ, b_1 ≠ j → ((Finsupp.single i 1) i * (Finsupp.single b_1 1) j) • b.coord i ⊗ₜ[R] c.coord b_1 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>j ∉ Finset.univ → ((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>∀ b_1 ∈ Finset.univ, b_1 ≠ i → ∑ x : κ, ((Finsupp.single b_1 1) i * (Finsupp.single x 1) j) • b.coord b_1 ⊗ₜ[R] c.coord x = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>i ∉ Finset.univ → ∑ x : κ, ((Finsupp.single i 1) i * (Finsupp.single x 1) j) • b.coord i ⊗ₜ[R] c.coord x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<VAR>i : α<VAR>h : b ≠ 0<GOAL>(single i b).support ≠ ⊥
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s✝ t : Set α<VAR>ℬ : Set (Set α)<VAR>h : 𝒜 ⊆ ℬ<VAR>s : Set α<VAR>hs : s ∈ generateSetAlgebra 𝒜<GOAL>s ∈ generateSetAlgebra ℬ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>h_eq : (fun n => f n x) = fun n => aeSeq hf p n x<GOAL>p x fun n => f n x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>h_eq : (fun n => f n x) = fun n => aeSeq hf p n x<GOAL>p x fun n => aeSeq hf p n x
<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>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>inst✝¹ : Countable ι'<VAR>m : ι → Measure α<VAR>m' : ι' → Measure β<VAR>inst✝ : ∀ (n : ι'), SFinite (m' n)<GOAL>(sum m).prod (sum m') = sum fun p => (m p.1).prod (m' p.2)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝¹ : CommRing B<VAR>inst✝ : IsDedekindDomain B<VAR>L : Ideal B<VAR>f : R ⧸ I →+* A ⧸ J<VAR>g : A ⧸ J →+* B ⧸ L<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>(idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) = idealFactorsFunOfQuotHom ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝¹ : CommRing B<VAR>inst✝ : IsDedekindDomain B<VAR>L : Ideal B<VAR>f : R ⧸ I →+* A ⧸ J<VAR>g : A ⧸ J →+* B ⧸ L<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : { p // p ∣ I }<GOAL>((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf)) x = (idealFactorsFunOfQuotHom ⋯) x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : Mul β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass β β (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<GOAL>f₁ * g₁ ≤ᶠ[l] f₂ * g₂
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : Nonempty X<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hgm : AEStronglyMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>∃ c, g =ᶠ[ae μ] const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : Nonempty X<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hgm : AEStronglyMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<VAR>t : Set X<VAR>ht : IsSeparable t<VAR>hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t<GOAL>∃ c, g =ᶠ[ae μ] const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : Nonempty X<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hgm : AEStronglyMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<VAR>t : Set X<VAR>ht : IsSeparable t<VAR>hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t<VAR>this : SecondCountableTopology ↑t<GOAL>∃ c, g =ᶠ[ae μ] const α c
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<VAR>hG : Presieve.IsSheaf J G.toPresheaf<GOAL>G = sheafify J G
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<VAR>hG : Presieve.IsSheaf J G.toPresheaf<GOAL>sheafify J G ≤ G
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<VAR>hG : Presieve.IsSheaf J G.toPresheaf<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ (sheafify J G).obj U<GOAL>s ∈ G.obj U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<VAR>hG : Presieve.IsSheaf J G.toPresheaf<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ (sheafify J G).obj U<GOAL>↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<VAR>hG : Presieve.IsSheaf J G.toPresheaf<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ (sheafify J G).obj U<GOAL>∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄, (G.sieveOfSection s).arrows f → F.map f.op ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = F.map f.op s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<VAR>hG : Presieve.IsSheaf J G.toPresheaf<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ (sheafify J G).obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection s).arrows i<GOAL>F.map i.op ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = F.map i.op s
<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✝¹ : DecidableEq ι<VAR>inst✝ : CancelCommMonoid α<VAR>s t : Finset ι<VAR>f : ι → α<GOAL>(∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i = (∏ i ∈ s \ t, f i) * ∏ i ∈ t, f i
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>i : σ<VAR>c : R<GOAL>Multiset.count i (p * C c).degrees ≤ Multiset.count i p.degrees
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>i : σ<VAR>c : R<GOAL>p.degrees = p.degrees + (C c).degrees
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>r : R<GOAL>(contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r) = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>r : R<GOAL>∀ (m : M) (x fx : CliffordAlgebra Q), ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx
<VAR>s : List Char<VAR>i p n : Nat<GOAL>utf8GetAux s { byteIdx := i + n } { byteIdx := p + n } = utf8GetAux s { byteIdx := i } { byteIdx := p }
<VAR>s : List Char<VAR>i p n : Nat<GOAL>∀ (c : Char) (cs : List Char) (i : Pos), ¬i = { byteIdx := p } → utf8GetAux cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := p + n } = utf8GetAux cs (i + c) { byteIdx := p } → (if { byteIdx := i.byteIdx + n } = { byteIdx := p + n } then c else utf8GetAux cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := p + n }) = if i = { byteIdx := p } then c else utf8GetAux cs (i + c) { byteIdx := p }
<VAR>s : List Char<VAR>i✝ p n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>h : ¬{ byteIdx := i } = { byteIdx := p }<VAR>ih : utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } = utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }<GOAL>(if { byteIdx := { byteIdx := i }.byteIdx + n } = { byteIdx := p + n } then c else utf8GetAux cs ({ byteIdx := { byteIdx := i }.byteIdx + n } + c) { byteIdx := p + n }) = if { byteIdx := i } = { byteIdx := p } then c else utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
<VAR>s : List Char<VAR>i✝ p n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>ih : utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } = utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }<VAR>h : ¬i = p<GOAL>(if i + n = p + n then c else utf8GetAux cs { byteIdx := i + n + c.utf8Size } { byteIdx := p + n }) = if i = p then c else utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }
<VAR>s : List Char<VAR>i✝ p n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>ih : utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } = utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }<VAR>h : ¬i = p<GOAL>utf8GetAux cs { byteIdx := i + n + c.utf8Size } { byteIdx := p + n } = utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }
<VAR>s : List Char<VAR>i✝ p n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>ih : utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } = utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }<VAR>h : ¬i = p<GOAL>utf8GetAux cs { byteIdx := i + c.utf8Size + n } { byteIdx := p + n } = utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>All p (match l, v, r with | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d) | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d) | a, x, b => node black a x b) ↔ p v ∧ All p l ∧ All p r
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = X ^ q ^ n - C y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : Category.{u_7, u_1} C<VAR>inst✝⁸ : Category.{u_6, u_2} D<VAR>inst✝⁷ : Category.{u_5, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>inst✝⁶ : AddMonoid M<VAR>inst✝⁵ : HasShift C M<VAR>inst✝⁴ : HasShift D M<VAR>inst✝³ : L.CommShift M<VAR>inst✝² : G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>inst✝¹ : ((whiskeringLeft C D A).obj L).Full<VAR>inst✝ : ((whiskeringLeft C D A).obj L).Faithful<VAR>X : C<GOAL>(F.isoShiftZero M).hom.app (L.obj X) = (e' 0).hom.app X ≫ (G.isoShiftZero M).hom.app X ≫ e.inv.app X