ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : MulZeroOneClass β<VAR>inst✝ : Nontrivial β<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>i : ι<GOAL>∀ t ∈ {t | ∃ j ≤ i, s j = t}, MeasurableSet t
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : MulZeroOneClass β<VAR>inst✝ : Nontrivial β<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>i : ι<GOAL>∀ t ∈ {s_1 | ∃ n, MeasurableSet s_1}, MeasurableSet t
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁷ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : AddCommGroup G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : μ.IsNegInvariant<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>hg : LocallyIntegrable g μ<GOAL>Continuous (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁷ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : AddCommGroup G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : μ.IsNegInvariant<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>hg : LocallyIntegrable g μ<GOAL>Continuous (g ⋆[L.flip, μ] f)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>B : C<VAR>X Y : Subobject B<VAR>f : underlying.obj X ⟶ underlying.obj Y<VAR>w : f ≫ Y.arrow = X.arrow<GOAL>X ≤ Y
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>h₁ : N ≤ maxTrivSubmodule R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L (M ⧸ N) k = ⊥<GOAL>IsNilpotent R L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>h₁ : N ≤ maxTrivSubmodule R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L (M ⧸ N) k = ⊥<GOAL>lowerCentralSeries R L M (k + 1) = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>h₁ : N ≤ maxTrivSubmodule R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L (M ⧸ N) k = ⊥<GOAL>⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>h₁ : N ≤ maxTrivSubmodule R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L (M ⧸ N) k = ⊥<GOAL>lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>h₁ : N ≤ maxTrivSubmodule R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L (M ⧸ N) k = ⊥<GOAL>LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L (M ⧸ N) k
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>d : Dir<VAR>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>i : ℕ<VAR>IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)<VAR>T : Tape Bool<GOAL>stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>d : Dir<VAR>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>i : ℕ<VAR>IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)<VAR>T : Tape Bool<GOAL>stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>d : Dir<VAR>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>i : ℕ<VAR>IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)<VAR>T : Tape Bool<GOAL>stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b✝ : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>a b : M<VAR>ab : (fun x => 1 • x) a = (fun x => 1 • x) b<GOAL>a = b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b✝ : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>a b : M<VAR>ab : 1 • a = 1 • b<GOAL>a = b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b✝ : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>a b : M<VAR>ab : a = b<GOAL>a = b
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>hv₀ : 0 < ↑v<VAR>hv₀' : 0 < 2 * ↑v - 1<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>hv₀ : 0 < ↑v<VAR>hv₀' : 0 < 2 * ↑v - 1<VAR>hv₁ : 0 < 2 * v - 1<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))<VAR>hv₀ : 0 < ↑v<VAR>hv₀' : 0 < 2 * ↑v - 1<VAR>hv₁ : 0 < 2 * v - 1<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))<VAR>hv₀ : 0 < ↑v<VAR>hv₀' : 0 < 2 * ↑v - 1<VAR>hv₁ : 0 < 2 * v - 1<VAR>hu₀ : 0 ≤ u - ⌊ξ⌋ * v<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))<VAR>hv₀ : 0 < ↑v<VAR>hv₀' : 0 < 2 * ↑v - 1<VAR>hv₁ : 0 < 2 * v - 1<VAR>hu₀ : 0 ≤ u - ⌊ξ⌋ * v<VAR>hu₁ : u - ⌊ξ⌋ * v ≤ v<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))<VAR>hv₀ : 0 < ↑v<VAR>hv₀' : 0 < 2 * ↑v - 1<VAR>hv₁ : 0 < 2 * v - 1<VAR>hu₀ : 0 ≤ u - ⌊ξ⌋ * v<VAR>hu₁ : u - ⌊ξ⌋ * v ≤ v<VAR>huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>a b m n✝ p✝ p n : ℕ<VAR>hn : (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)).card = n / p<GOAL>(Finset.filter (fun e => p ∣ e + 1) (Finset.range (n + 1))).card = (n + 1) / p
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<GOAL>toLaurent (Polynomial.C r) = C r
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<GOAL>C r = C r * T ↑0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q = 0<GOAL>norm (const (padicNorm p) q) = padicNorm p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q = 0<VAR>this : const (padicNorm p) q ≈ 0<GOAL>norm (const (padicNorm p) q) = padicNorm p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : ¬q = 0<GOAL>norm (const (padicNorm p) q) = padicNorm p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : ¬q = 0<VAR>this : ¬const (padicNorm p) q ≈ 0<GOAL>norm (const (padicNorm p) q) = padicNorm p q
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y : Mon_ C<GOAL>(X ⊗ Y).one ≫ (β_ X.X Y.X).hom = (Y ⊗ X).one
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y : Mon_ C<GOAL>(ρ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).inv ≫ (Y.one ⊗ X.one) = Y.one ⊗ X.one
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<VAR>t : Set β<VAR>x✝ : α<VAR>y : β<VAR>h : e.IsImage s t<VAR>x : α<VAR>hx : x ∈ e.source<GOAL>↑e.symm (↑e x) ∈ s ↔ ↑e x ∈ t
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>p ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>p = 0 → p.leadingCoeff * q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<GOAL>q ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<GOAL>q = 0 → p.leadingCoeff * q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>p.degree + q.degree ≤ (p * q).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>↑p.natDegree + ↑q.natDegree ≤ (p * q).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).coeff (p.natDegree + q.natDegree) ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>j k : M' →ₗ[R] M''<VAR>h : j ∘ₗ f = k ∘ₗ f<GOAL>j = k
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>j k : M' →ₗ[R] M''<VAR>h : j ∘ₗ f = k ∘ₗ f<GOAL>k ∘ₗ f = k ∘ₗ f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⊓ (a ⇨ b) ≤ b
<VAR>m n : ℕ<GOAL>m.Coprime (n + m) ↔ m.Coprime n
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>(⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ i, ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a⁻¹ ≤ b ↔ b⁻¹ ≤ a
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>p : ℕ<GOAL>p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>p : ℕ<GOAL>Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
<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>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>ν : Measure β<VAR>μ : Measure α<VAR>e : α ≃ᵐ β<GOAL>Measure.map (⇑e.symm) (Measure.map (⇑e) μ) ≪ μ
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>x✝ : Invertible a<GOAL>a * (⅟a * b) = b
<VAR>Ω : Type u_1<VAR>inst✝¹ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝ : TopologicalSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
<VAR>Ω : Type u_1<VAR>inst✝¹ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝ : TopologicalSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>(μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
<VAR>K : Type u_1<VAR>R : 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✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>χ : L → R<VAR>x : L<GOAL>(trace R ↥↑(weightSpace M χ)) ((toEnd R L ↥↑(weightSpace M χ)) x) = finrank R ↥↑(weightSpace M χ) • χ x
<VAR>K : Type u_1<VAR>R : 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✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>χ : L → R<VAR>x : L<GOAL>_root_.IsNilpotent ((toEnd R L ↥↑(weightSpace M χ)) x - χ x • LinearMap.id)
<VAR>K : Type u_1<VAR>R : 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✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>χ : L → R<VAR>x : L<GOAL>_root_.IsNilpotent ((toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x))
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.π.app ((sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>S.proj n = (Profinite.asLimitCone (CompHausLike.of (fun X => TotallyDisconnectedSpace ↑X) ↑S.toTop)).π.app ((sequentialFunctor (DiscreteQuotient ↑S.toTop)).obj (Opposite.op n))
<VAR>S : LightProfinite<VAR>n : ℕ<VAR>c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone<VAR>hc : IsLimit c := S.toLightDiagram.isLimit<GOAL>S.proj n = (Profinite.asLimitCone (CompHausLike.of (fun X => TotallyDisconnectedSpace ↑X) ↑S.toTop)).π.app ((sequentialFunctor (DiscreteQuotient ↑S.toTop)).obj (Opposite.op n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>s : Set α<GOAL>MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<GOAL>Irrational (- -x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<GOAL>limsup u atTop = ⨅ n, ⨆ i, u (i + n)
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>fs : α →ₛ ℝ≥0<VAR>fs_le_f : ∀ (x : α), ↑fs x ≤ f x<VAR>int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(↑fs x) ∂μ + ε / 2<GOAL>∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>fs : α →ₛ ℝ≥0<VAR>fs_le_f : ∀ (x : α), ↑fs x ≤ f x<VAR>int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(↑fs x) ∂μ + ε / 2<VAR>int_fs_lt_top : ∫⁻ (x : α), ↑(↑fs x) ∂μ ≠ ⊤<GOAL>∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>fs : α →ₛ ℝ≥0<VAR>fs_le_f : ∀ (x : α), ↑fs x ≤ f x<VAR>int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(↑fs x) ∂μ + ε / 2<VAR>int_fs_lt_top : ∫⁻ (x : α), ↑(↑fs x) ∂μ ≠ ⊤<VAR>g : α → ℝ≥0<VAR>g_le_fs : ∀ (x : α), g x ≤ ↑fs x<VAR>gcont : UpperSemicontinuous g<VAR>gint : ∫⁻ (x : α), ↑(↑fs x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2<GOAL>∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>fs : α →ₛ ℝ≥0<VAR>fs_le_f : ∀ (x : α), ↑fs x ≤ f x<VAR>int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(↑fs x) ∂μ + ε / 2<VAR>int_fs_lt_top : ∫⁻ (x : α), ↑(↑fs x) ∂μ ≠ ⊤<VAR>g : α → ℝ≥0<VAR>g_le_fs : ∀ (x : α), g x ≤ ↑fs x<VAR>gcont : UpperSemicontinuous g<VAR>gint : ∫⁻ (x : α), ↑(↑fs x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2<GOAL>∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasTerminal C<VAR>ι : Type w<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Finite ι<VAR>X : C<VAR>j : ι<GOAL>(limitIsoPi ι X).hom ≫ Pi.π (fun x => X) j = WidePullback.π (fun x => terminal.from X) j
<VAR>n n✝ : ℕ<VAR>h : n✝ + 1 ∈ n.divisors<GOAL>0 < n✝ + 1
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type u_11<VAR>N : Type u_12<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : SMul M N<VAR>inst✝ : IsScalarTower M N N<VAR>x : M<VAR>y : N<GOAL>x • 1 * y = x • y
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<GOAL>(trace R (M ⊗[R] N)) (TensorProduct.map f g) = (trace R M) f * (trace R N) g
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<VAR>h : (((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))) f) g = (((lsmul R R).compl₁₂ (trace R M) (trace R N)) f) g<GOAL>(trace R (M ⊗[R] N)) (TensorProduct.map f g) = (trace R M) f * (trace R N) g
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<VAR>h : (trace R (M ⊗[R] N)) (TensorProduct.map f g) = (trace R M) f * (trace R N) g<GOAL>(trace R (M ⊗[R] N)) (TensorProduct.map f g) = (trace R M) f * (trace R N) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a * b < b ↔ a * b < 1 * b